<div dir="ltr"><div>Wait, what?!? That seems really counterintuitive to me. But you're right, the following also works on the current github Agda:<br><br> works3 : (e : E) (g : G) (e∈g : e ∈ g) →<br> _≡_ {A = V}<br> (value ⦃ _ ⦄ e∈g)<br> (value ⦃ _ ⦄ e∈g)<br> works3 e g e∈g = refl<br><br>I would expect an underscore to be solved by the constraint solver, if I wanted instance search I'd use 'it'. So now there's no easy way to turn an instance implicit into a regular implicit, that seems like a loss of expressivity to me.<br><br><br></div><div>Jesper</div><div><div class="gmail_extra"><br><div class="gmail_quote">On Sat, Nov 5, 2016 at 11:26 AM, Andreas Abel <span dir="ltr"><<a href="mailto:abela@chalmers.se" target="_blank">abela@chalmers.se</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span>On 05.11.2016 10:32, Jesper Cockx wrote:<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
If you write ⦃ _ ⦄as an argument, then Agda won't use instance search<br>
for this argument but it will use the constraint solver instead.<br>
</blockquote>
<br></span>
I thought I changed that in 2.5.2, see<br>
<a href="https://github.com/agda/agda/issues/2172" rel="noreferrer" target="_blank">https://github.com/agda/agda/i<wbr>ssues/2172</a><br>
<br>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex"><span>
You<br>
should just leave out the argument instead if you want to use the<br>
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>
You do need to give {A = V} because the instance search doesn't work<br>
with unsolved metas in the type, because otherwise it may get stuck in a<br>
loop.<br>
<br>
Cheers,<br>
Jesper<br>
<br>
On Sat, Nov 5, 2016 at 8:23 AM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a><br></span><span>
<mailto:<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</a>>> wrote:<br>
<br>
The problem isn't that there are too many candidates (the error<br>
should be clearer about this) but that there are unsolved metas in<br>
the target (_A_35).<br>
See <a href="http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution" rel="noreferrer" target="_blank">http://agda.readthedocs.io/en/<wbr>latest/language/instance-argum<wbr>ents.html#instance-resolution</a><br>
<<a href="http://agda.readthedocs.io/en/latest/language/instance-arguments.html#instance-resolution" rel="noreferrer" target="_blank">http://agda.readthedocs.io/en<wbr>/latest/language/instance-argu<wbr>ments.html#instance-resolution</a><wbr>><br>
for the details.<br>
<br>
/ Ulf<br>
<br>
On Sat, Nov 5, 2016 at 6:03 AM, Martin Stone Davis<br></span>
<<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gmail.com</a> <mailto:<a href="mailto:martin.stone.davis@gmail.com" target="_blank">martin.stone.davis@gma<wbr>il.com</a>>><div><div class="gmail-m_-8094278342279473h5"><br>
wrote:<br>
<br>
I'm unclear why the below code fails to typecheck and confused<br>
by the error message. First, the code:<br>
<br>
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>
<br>
<br>
Here are the relevant parts of the error message that have me<br>
scratching my head:<br>
<br>
_r_41 : Valueable ((E∈G Membership.∈ e) g) (_A_35 E G V e g e∈g)<br>
<br>
(This is associated with yellow highlighting on the instance<br>
argument to the first call to 'value' in 'fails'.)<br>
<br>
<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₁)<br>
g₁) →<br>
Valueable ((E∈G₁ Membership.∈ e₁) g₁) (_A_35 E₁ G₁<br>
V₁ e₁ g₁ e∈g₁)<br>
Candidates<br>
e∈g→v :<br>
{e = e₁ : E} {g = g₁ : G} → Valueable ((E∈G<br>
Membership.∈ e₁) g₁) V<br>
E∈G : Membership E G<br>
<br>
The above error message seems to indicate that both 'e∈g→v' and<br>
'E∈G' are candidates for the instance argument to 'value'. But<br>
'E∈G' doesn't have a 'Valueable' type! So, how can it be a<br>
candidate?<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br></div></div>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><wbr>><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><span><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a>><br>
<br>
<br>
<br>
______________________________<wbr>_________________<br>
Agda mailing list<br></span>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a> <mailto:<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><wbr>><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><span><br>
<<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mai<wbr>lman/listinfo/agda</a>><br>
<br>
<br>
<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>
<br>
</span></blockquote><span class="gmail-m_-8094278342279473HOEnZb"><font color="#888888">
<br>
<br>
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Department of Computer Science and Engineering<br>
Chalmers and Gothenburg University, Sweden<br>
<br>
<a href="mailto:andreas.abel@gu.se" target="_blank">andreas.abel@gu.se</a><br>
<a href="http://www2.tcs.ifi.lmu.de/%7Eabel/" rel="noreferrer" target="_blank">http://www2.tcs.ifi.lmu.de/~ab<wbr>el/</a><br>
</font></span></blockquote></div><br></div></div></div>