<div dir="ltr"><div><div><div>Thank you for the explanation, I think I understand now. I was trying to use instance arguments for a closed type family, while they were meant for open type families. I've now found a better way to handle my example, (ab)using eta-equality and injectivity of constructor-headed functions:<br><br><div style="margin-left:40px">it : ⊤<br>it = record {}<br><br>IsZero : Nat → Set<br>IsZero zero = ⊤<br>IsZero _ = ⊥<br><br>test : IsZero _<br>test = it<br><br>is-zero : (n : Nat) {_ : IsZero n} → n ≡ zero<br>is-zero zero = refl<br>is-zero (suc _) {()}<br><br>IsSuc : Nat → Set<br>IsSuc (suc _) = ⊤<br>IsSuc _ = ⊥<br><br>pred : (n : Nat) {_ : IsSuc n} → Nat<br>pred zero {()}<br>pred (suc n) = n<br></div><br></div>So in conclusion: I think instance arguments work just fine, I was just using them wrong.<br><br></div>Cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Oct 29, 2014 at 11:37 AM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">It’s indeed rejected because instance search will now refuse to look<br>
for an instance when one of the arguments of the typeclass is an<br>
unsolved meta (unless this meta is determined by other arguments, e.g.<br>
universe levels).<br>
<br>
For instance if you define the decidable equality typeclass and only<br>
the instance for Nat and write ? == ?, should Agda say "I only know<br>
of one way to have decidable equality on some type and it’s on the<br>
type Nat, hence the two question marks have to be natural numbers and<br>
I will use decidable equality of natural numbers." ?<br>
Right now we don’t do that and we just don’t solve the constraint,<br>
both to prevent loopings (what if you had only defined the instance<br>
for List instead?) and because it doesn’t seem right, instance search<br>
should look at the head constructor of the type and do something<br>
appropriate, not deduce the arguments of the typeclass just because we<br>
happen to have defined only one instance.<br>
<br>
In your case, if you replace the underscore in the type of test by 0,<br>
then instance search will find is-zero as expected.<br>
<br>
Of course we can still discuss what instance search should do, the<br>
current criterium is what we agreed on in Tallinn with Ulf, but it can<br>
probably be improved.<br>
<br>
Cheers,<br>
Guillaume<br>
<div><div class="h5"><br>
2014-10-29 10:44 GMT+01:00 Jesper Cockx <<a href="mailto:Jesper@sikanda.be">Jesper@sikanda.be</a>>:<br>
> Can someone tell me if the code fragment below is supposed to work? It gives<br>
> me yellow, but it works fine when I replace `it` by the (unique) solution<br>
> `is-zero`.<br>
><br>
> it : {A : Set} {{_ : A}} → A<br>
> it {{x}} = x<br>
><br>
> data IsZero : Nat → Set where<br>
> instance<br>
> is-zero : IsZero 0<br>
><br>
> test : IsZero _<br>
> test = it<br>
><br>
> Cheers,<br>
> Jesper<br>
><br>
</div></div>> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
><br>
</blockquote></div><br></div>