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

[Ulf Norell]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20161105/76eed9d4/attachment-0001.html