[Agda] implicit argument equality weirdness

[Noam Zeilberger]

On Wed, Oct 29, 2008 at 11:04:32AM +0100, Ulf Norell wrote:
> metavariable. If you want to use implicit functions in a higher order way you
> have to be explicit about it, in this case write
> 
> � lam (\{a} -> f {a})
> 
> Once we do that it still doesn't work. That's because the typechecker didn't
> perform eta contraction before unifying datatype indices. This is a bug which I
> have now fixed.

Thanks!  Yes, that fixes it.

Noam