[Agda] implicit argument equality weirdness

[Ulf Norell]

On Wed, Oct 29, 2008 at 9:06 AM, Noam Zeilberger
<noam+agda at cs.cmu.edu<noam%2Bagda at cs.cmu.edu>
> wrote:

> Consider two code snippets, which only differ by (a : A) vs {a : A},
> i.e. explicit vs implicit arguments:
> -------
> module Test1  (A B : Set) where
>
>  data fnAB : Set where
>    lam : ((a : A) -> B) -> fnAB
>
>  data R : fnAB -> fnAB -> Set where
>    r : {f g : (a : A) -> B} -> A -> R (lam f) (lam g)
>
>  invert : {f g : (a : A) -> B} -> R (lam f) (lam g) -> A
>  invert (r a) = a
> -------
> module Test2  (A B : Set) where
>
>  data fnAB : Set where
>    lam : ({a : A} -> B) -> fnAB
>
>  data R : fnAB -> fnAB -> Set where
>    r : {f g : {a : A} -> B} -> A -> R (lam f) (lam g)
>
>  invert : {f g : {a : A} -> B} -> R (lam f) (lam g) -> A
>  invert (r a) = a
> -------

Test1 typechecks, while Test2 fails with error...
>
> Is this a bug?


There are two problems, one of which is a bug. When you say "lam f" the
mechanism for inserting implicit arguments turns this into

  lam (\{a} -> f {_})

The implicit argument to f cannot be inferred and you're left with an
unsolved 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.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: https://lists.chalmers.se/mailman/private/agda/attachments/20081029/22b02a66/attachment.html