[Agda] Agda crash caused by excessive unfolding

[Marcin Benke]

Thomas Hallgren wrote:

> Hi,
>
> I enclose an example where Agda's does too much unfolding when it 
> displays types of meta variables.
>
>
Makoto seems to have answered about the bug alreadfy, so  I add only a 
few words about versions of Agda:

>
> The version of Agda that I used is from October 2004, so perhaps this 
> problem has been solved already? I tried to repeat the test with 
> Agda-1.1-Midsummer-i386-Linux.tgz, but after working around some 
> syntax problems, I got a type error that I didn't understand...
>
> ---  ("info" ("* Agda version *" "Agda with idata and implicit 
> arguments\n\n[ghc604; built Jun 24 2005 10:53:00]")) +++
> >> load bug.alfa
> ---  ("error" ("At: \"bug.alfa\", line 10, column 16\nError in the 
> telescope of f because:\nMore function arguments than the function 
> type specifies: E")) +++

The Midsummer Linux binary is compiled with "new" aka "Summer School" 
syntax, where arguments in the telescope are hidden by default. If you 
want the "classic" syntax, you can either recompile the Midsummer source 
yourself, or get the Jun 1 binary  - the main change made in June was 
the addition of the (optional) new syntax.

Marcin