[Agda] Agda crash caused by excessive unfolding

[Thomas Hallgren]

Hello,

Thanks for your replies!

Marcin Benke wrote:

> ... "new" aka "Summer School" syntax ... If you want the "classic" 
> syntax, you can either recompile the Midsummer source yourself, or get 
> the Jun 1 binary  ...

I see, the new syntax looks nice...

takeyama wrote:

>...
>In the example, the type of the meta in proofA1 is something like
>  (PredT#86 {}) ((f#88 {}) (B#85 {}) (i#90 {}) p#108)
>...  i#90, as opposed to i#103
>defined in P3, is not in scope.  So Agda unfolds it, trying not to
>print out-of-scope i#90.  This is not the matter of how not to unfold i#103.
>  
>
But i#103 is defined by a simple "open P2 use i", so it doesn't look 
like it would be too hard to keep track of the fact that i#103 can be 
used refer to i#90. Any chance that Agda could be improved to do that?

The example was distilled from code produced by my Haskell-to-Alfa 
translator, which translates Haskell modules to Agda packages, so the 
above problem is quite common. In this context, I don't need the full 
power of Agda packages, just name space control, so an improvement for 
this special case would be very useful!

-- 
Thomas H

Our productivity is directly proportional to our ability to relax;
only when our minds are clear and our thoughts are organized can we
achieve results and unleash our creative potential.  -- David Allen