<div dir="ltr"><div><div><div>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:<br><br> works2 : (e : E) (g : G) (e∈g : e ∈ g) →<br> _≡_ {A = V}<br> (value e∈g)<br> (value e∈g)<br> works2 e g e∈g = refl<br><br></div>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.<br><br></div>Cheers,<br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 5, 2016 at 8:23 AM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><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" target="_blank">http://agda.readthedocs.<wbr>io/en/latest/language/<wbr>instance-arguments.html#<wbr>instance-resolution</a> for the details.<span class="HOEnZb"><font color="#888888"><div><br></div><div>/ Ulf</div></font></span></div><div class="HOEnZb"><div class="h5"><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>
</div></div><br>______________________________<wbr>_________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/<wbr>mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>