<div dir="ltr">There are a few reasons why only instance arguments are available for instance search:<div><br></div><div>- Variables may have big types that are expensive to check against the goal type. And you</div><div>  typically have quite a lot of variables in the context.</div><div><br></div><div>- Unrelated variables can interfere with instance search if their types contain metas,</div><div>  meaning that instance search cannot determine uniqueness. In some cases (don't</div><div>  have one at hand though), the metas in the types can only be solved once the instance</div><div>  goal is solved, so you get an unsolved metas.</div><div><br></div><div>- It's a nice symmetric design: top-level things need to be 'instance' to be eligible and</div><div>  lambda-bound things need to be '{{ }}'.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 31, 2017 at 7:11 PM, Apostolis Xekoukoulotakis <span dir="ltr"><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@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"><div><div>I haven't used Idris for a while but in the documentation, it says that using something in the outer context requires the "%hint" annotation, so this is similar to how we need to annotate functions with instance in Agda.<br><br></div> I am mostly referring to the lhs variables.<br><br></div>What you propose is a nice hack that is only useful if the constructed proof is proportionally bigger.<br></div><div class="HOEnZb"><div class="h5"><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 31, 2017 at 8:01 PM, Guillaume Brunerie <span dir="ltr"><<a href="mailto:guillaume.brunerie@gmail.com" target="_blank">guillaume.brunerie@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">By "in the context", you only mean things bound by let and on<br>
left-hand sides, right? Not everything in scope? Allowing everything<br>
in scope would make instance search prohibitively slow when using big<br>
libraries.<br>
<br>
If you do mean variables bound on left-hand sides, I’m not quite sure<br>
either why explicit arguments are not available for instance search<br>
but note that<br>
- instance arguments *are* available for instance search, as you<br>
mention, so even though in<br>
<br>
f : A -> B<br>
f a = ?<br>
<br>
the [a] is not available for instance search in the goal, it is available in<br>
<br>
f : {{_ : A}} -> B<br>
f = ?<br>
<br>
- In case you need explicit arguments to be available for instance<br>
search, you can use the following workaround:<br>
<br>
f : A -> B -> C<br>
f a b = ? where instance _ = a; _ = b<br>
<br>
Now both [a] and [b] are available for instance search.<br>
<br>
On Tue, Oct 31, 2017 at 12:47 PM, Apostolis Xekoukoulotakis<br>
<span><<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>> wrote:<br>
> <a href="http://docs.idris-lang.org/en/latest/tutorial/miscellany.html?#auto-implicit-arguments" rel="noreferrer" target="_blank">http://docs.idris-lang.org/en/<wbr>latest/tutorial/miscellany.htm<wbr>l?#auto-implicit-arguments</a><br>
><br>
> On Tue, Oct 31, 2017 at 6:17 PM, Apostolis Xekoukoulotakis<br>
> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com" target="_blank">apostolis.xekoukoulotakis@gma<wbr>il.com</a>> wrote:<br>
>><br>
>> I am trying to simplify my code by using instance arguments and thus<br>
>> letting agda fill them.<br>
>><br>
>> I am wondering why Agda does not allow to pick variables that are not<br>
>> instance tagged as solutions if there is a unique such solution in the<br>
>> context.<br>
>><br>
>> A similar feature is the 'auto' in Idris. In this case, auto specifies<br>
>> which implicit arguments to automatically fill , with anything found in the<br>
>> context.<br>
><br>
><br>
><br>
</span>> ______________________________<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>
</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>