[Agda] newbie instance resolution question: too many candidates?

[Jesper Cockx]

If you write ⦃ _ ⦄as an argument, then Agda won't use instance search for
this argument but it will use the constraint solver instead. You should
just leave out the argument instead if you want to use the instance search.
The following version works:

      works2 : (e : E) (g : G) (e∈g : e ∈ g) →
            _≡_ {A = V}
                (value e∈g)
                (value e∈g)
      works2 e g e∈g = refl

You do need to give {A = V} because the instance search doesn't work with
unsolved metas in the type, because otherwise it may get stuck in a loop.

Cheers,
Jesper

On Sat, Nov 5, 2016 at 8:23 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> The problem isn't that there are too many candidates (the error should be
> clearer about this) but that there are unsolved metas in the target
> (_A_35). See http://agda.readthedocs.io/en/latest/language/
> instance-arguments.html#instance-resolution for the details.
>
> / Ulf
>
> On Sat, Nov 5, 2016 at 6:03 AM, Martin Stone Davis <
> martin.stone.davis at gmail.com> wrote:
>
>> I'm unclear why the below code fails to typecheck and confused by the
>> error message. First, the code:
>>
>> open import Agda.Builtin.Equality
>>>
>>> record Membership (E G : Set) : Set₁ where
>>>   field _∈_ : E → G → Set
>>>
>>> open Membership ⦃ ... ⦄
>>>
>>> record Valueable (A V : Set) : Set where
>>>   field value : A → V
>>>
>>> open Valueable ⦃ ... ⦄
>>>
>>> module _
>>>   (E G V : Set)
>>>   ⦃ E∈G : Membership E G ⦄
>>>   ⦃ e∈g→v : {e : E} {g : G} → Valueable (e ∈ g) V ⦄
>>>   where
>>>
>>>   works : (e : E) (g : G) (e∈g : e ∈ g) →
>>>         _≡_ {A = V}
>>>             (value ⦃ e∈g→v ⦄ e∈g)
>>>             (value ⦃ e∈g→v ⦄ e∈g)
>>>   works e g e∈g = refl
>>>
>>>   fails : (e : E) (g : G) (e∈g : e ∈ g) →
>>>         _≡_ {A = _}
>>>             (value ⦃ _ ⦄ e∈g)
>>>             (value ⦃ _ ⦄ e∈g)
>>>   fails e g e∈g = refl
>>>
>>
>> Here are the relevant parts of the error message that have me scratching
>> my head:
>>
>> _r_41 : Valueable ((E∈G Membership.∈ e) g) (_A_35 E G V e g e∈g)
>>>
>>> (This is associated with yellow highlighting on the instance argument to
>> the first call to 'value' in 'fails'.)
>>
>>>
>>> Failed to solve the following constraints:
>>>   [0] Resolve instance argument
>>>         _41 :
>>>           (E₁ G₁ V₁ : Set) {{E∈G = E∈G₁ : Membership E₁ G₁}}
>>>           {{e∈g→v = e∈g→v₁
>>>             : {e = e₁ : E₁} {g = g₁ : G₁} →
>>>               Valueable ((E∈G₁ Membership.∈ e₁) g₁) V₁}}
>>>           (e₁ : E₁) (g₁ : G₁) (e∈g₁ : (E∈G₁ Membership.∈ e₁) g₁) →
>>>           Valueable ((E∈G₁ Membership.∈ e₁) g₁) (_A_35 E₁ G₁ V₁ e₁ g₁
>>> e∈g₁)
>>>       Candidates
>>>         e∈g→v :
>>>           {e = e₁ : E} {g = g₁ : G} → Valueable ((E∈G Membership.∈ e₁)
>>> g₁) V
>>>         E∈G : Membership E G
>>>
>>> The above error message seems to indicate that both 'e∈g→v' and 'E∈G'
>> are candidates for the instance argument to 'value'. But 'E∈G' doesn't have
>> a 'Valueable' type! So, how can it be a candidate?
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
> _______________________________________________
> 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/20161105/f39fbcc2/attachment.html