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

[Jesper Cockx]

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:

it : ⊤
it = record {}

IsZero : Nat → Set
IsZero zero = ⊤
IsZero _    = ⊥

test : IsZero _
test = it

is-zero : (n : Nat) {_ : IsZero n} → n ≡ zero
is-zero zero = refl
is-zero (suc _) {()}

IsSuc : Nat → Set
IsSuc (suc _) = ⊤
IsSuc _ = ⊥

pred : (n : Nat) {_ : IsSuc n} → Nat
pred zero {()}
pred (suc n) = n

So in conclusion: I think instance arguments work just fine, I was just
using them wrong.

Cheers,
Jesper

On Wed, Oct 29, 2014 at 11:37 AM, Guillaume Brunerie <
guillaume.brunerie at gmail.com> wrote:

> 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
> >
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20141029/04511f97/attachment.html