<div dir="ltr">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 <a href="http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution">http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution</a> for the details.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 5, 2016 at 6:03 AM, Martin Stone Davis <span dir="ltr"><<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I'm unclear why the below code fails to typecheck and confused by the error message. First, the code:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
open import Agda.Builtin.Equality<br>
<br>
record Membership (E G : Set) : Set₁ where<br>
field _∈_ : E → G → Set<br>
<br>
open Membership ⦃ ... ⦄<br>
<br>
record Valueable (A V : Set) : Set where<br>
field value : A → V<br>
<br>
open Valueable ⦃ ... ⦄<br>
<br>
module _<br>
(E G V : Set)<br>
⦃ E∈G : Membership E G ⦄<br>
⦃ e∈g→v : {e : E} {g : G} → Valueable (e ∈ g) V ⦄<br>
where<br>
<br>
works : (e : E) (g : G) (e∈g : e ∈ g) →<br>
_≡_ {A = V}<br>
(value ⦃ e∈g→v ⦄ e∈g)<br>
(value ⦃ e∈g→v ⦄ e∈g)<br>
works e g e∈g = refl<br>
<br>
fails : (e : E) (g : G) (e∈g : e ∈ g) →<br>
_≡_ {A = _}<br>
(value ⦃ _ ⦄ e∈g)<br>
(value ⦃ _ ⦄ e∈g)<br>
fails e g e∈g = refl<br>
</blockquote>
<br>
Here are the relevant parts of the error message that have me scratching my head:<br>
<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
_r_41 : Valueable ((E∈G Membership.∈ e) g) (_A_35 E G V e g e∈g)<br>
<br>
</blockquote>
(This is associated with yellow highlighting on the instance argument to the first call to 'value' in 'fails'.)<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<br>
Failed to solve the following constraints:<br>
[0] Resolve instance argument<br>
_41 :<br>
(E₁ G₁ V₁ : Set) {{E∈G = E∈G₁ : Membership E₁ G₁}}<br>
{{e∈g→v = e∈g→v₁<br>
: {e = e₁ : E₁} {g = g₁ : G₁} →<br>
Valueable ((E∈G₁ Membership.∈ e₁) g₁) V₁}}<br>
(e₁ : E₁) (g₁ : G₁) (e∈g₁ : (E∈G₁ Membership.∈ e₁) g₁) →<br>
Valueable ((E∈G₁ Membership.∈ e₁) g₁) (_A_35 E₁ G₁ V₁ e₁ g₁ e∈g₁)<br>
Candidates<br>
e∈g→v :<br>
{e = e₁ : E} {g = g₁ : G} → Valueable ((E∈G Membership.∈ e₁) g₁) V<br>
E∈G : Membership E G<br>
<br>
</blockquote>
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?<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
</blockquote></div><br></div>