[Agda] Puzzled about how instance arguments work in the presence of metas

[Guillaume Brunerie]

It’s indeed rejected because instance search will now refuse to look
for an instance when one of the arguments of the typeclass is an
unsolved meta (unless this meta is determined by other arguments, e.g.
universe levels).

For instance if you define the decidable equality typeclass and only
the instance for Nat and write  ? == ?, should Agda say "I only know
of one way to have decidable equality on some type and it’s on the
type Nat, hence the two question marks have to be natural numbers and
I will use decidable equality of natural numbers." ?
Right now we don’t do that and we just don’t solve the constraint,
both to prevent loopings (what if you had only defined the instance
for List instead?) and because it doesn’t seem right, instance search
should look at the head constructor of the type and do something
appropriate, not deduce the arguments of the typeclass just because we
happen to have defined only one instance.

In your case, if you replace the underscore in the type of test by 0,
then instance search will find is-zero as expected.

Of course we can still discuss what instance search should do, the
current criterium is what we agreed on in Tallinn with Ulf, but it can
probably be improved.

Cheers,
Guillaume

2014-10-29 10:44 GMT+01:00 Jesper Cockx <Jesper at sikanda.be>:
> Can someone tell me if the code fragment below is supposed to work? It gives
> me yellow, but it works fine when I replace `it` by the (unique) solution
> `is-zero`.
>
> it : {A : Set} {{_ : A}} → A
> it {{x}} = x
>
> data IsZero : Nat → Set where
>   instance
>     is-zero : IsZero 0
>
> test : IsZero _
> test = it
>
> Cheers,
> Jesper
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>