<div dir="ltr">You can also define a function<div><br></div><div>infixr 0 _asInst_</div><div><div> _asInst_ : ∀ {a b} {A : Set a} {B : A → Set b} (x : A) → ({{y : A}} → B y) → B x</div><div> x asInst f = f {{x}}</div></div><div><br></div><div>and say</div><div><br></div><div>f : A -> B -> C</div><div>f a b = a asInst b asInst ?</div><div><br></div><div>I think pattern synonyms is the best vehicle to solve this problem. Currently they</div><div>don't support instance arguments, but that's been on my todo list for a while. I</div><div>filed #2829:</div><div><br></div><div><a href="https://github.com/agda/agda/issues/2829">https://github.com/agda/agda/issues/2829</a><br></div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Oct 31, 2017 at 9:10 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">Maybe there could be a way to declare an explicit argument to be<br>
available for instance search (other than my hack above).<br>
For instance<br>
<span class=""><br>
f : A -> B -> C<br>
</span>f (instance a) (instance b) = ?<br>
<span class="HOEnZb"><font color="#888888"><br>
Guillaume<br>
</font></span><div class="HOEnZb"><div class="h5"><br>
On Tue, Oct 31, 2017 at 4:07 PM, Ulf Norell <<a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>> wrote:<br>
> There are a few reasons why only instance arguments are available for<br>
> instance search:<br>
><br>
> - Variables may have big types that are expensive to check against the goal<br>
> type. And you<br>
> typically have quite a lot of variables in the context.<br>
><br>
> - Unrelated variables can interfere with instance search if their types<br>
> contain metas,<br>
> meaning that instance search cannot determine uniqueness. In some cases<br>
> (don't<br>
> have one at hand though), the metas in the types can only be solved once<br>
> the instance<br>
> goal is solved, so you get an unsolved metas.<br>
><br>
> - It's a nice symmetric design: top-level things need to be 'instance' to be<br>
> eligible and<br>
> lambda-bound things need to be '{{ }}'.<br>
><br>
> / Ulf<br>
><br>
> On Tue, Oct 31, 2017 at 7:11 PM, Apostolis Xekoukoulotakis<br>
> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@<wbr>gmail.com</a>> wrote:<br>
>><br>
>> I haven't used Idris for a while but in the documentation, it says that<br>
>> using something in the outer context requires the "%hint" annotation, so<br>
>> this is similar to how we need to annotate functions with instance in Agda.<br>
>><br>
>> I am mostly referring to the lhs variables.<br>
>><br>
>> What you propose is a nice hack that is only useful if the constructed<br>
>> proof is proportionally bigger.<br>
>><br>
>> On Tue, Oct 31, 2017 at 8:01 PM, Guillaume Brunerie<br>
>> <<a href="mailto:guillaume.brunerie@gmail.com">guillaume.brunerie@gmail.com</a>> wrote:<br>
>>><br>
>>> 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<br>
>>> 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>
>>> <<a href="mailto:apostolis.xekoukoulotakis@gmail.com">apostolis.xekoukoulotakis@<wbr>gmail.com</a>> wrote:<br>
>>> ><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.<wbr>html?#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">apostolis.xekoukoulotakis@<wbr>gmail.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<br>
>>> >> in the<br>
>>> >> context.<br>
>>> ><br>
>>> ><br>
>>> ><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>
>><br>
>><br>
>><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>
><br>
</div></div></blockquote></div><br></div>