[Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'

[Andreas Abel]

On 11/15/10 9:35 PM, Dirk Ullrich wrote:
> Hi all,
>   when I try to generate all `agdai' files for the Agda standard lib at
> once with the current Agda version from darcs repository I get an
> error for `Data.Star.Decoration.agda':
> ...
> .../Data/Star/Decoration.agda:54,15-16
> xs != ε of type Star (λ .i' .j → T .i' .j) j j
> when checking that the pattern ε has type
> Star (DecoratedWith (λ {.i} {.j} → P)) (nonEmpty xs) (nonEmpty ε)
>
> Here it is caused by Andreas' patch that removes eta-contraction of
> function bodies in `Def.hs'.

Seems plausible.

> Can anyone reproduce this?

If I had more main memory, probably...

Andreas


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/