[Agda] Instance resolution question

[Apostolis Xekoukoulotakis]

https://lists.chalmers.se/pipermail/agda/2017/009802.html

>From a previous discussion with Andreas, hidden/instance arguments are
inserted eagerly.
I wonder  if I can disable this specifically for "{{ctx}}".

On Wed, Mar 28, 2018 at 8:14 AM, Ulf Norell <ulf.norell at gmail.com> wrote:

> The candidates are not equal. This is what `rob` expands to:
>
> rob : CPF
> rob {{ctx}} = fun (λ {{ctx'}} → e)
>
> ctx and ctx' are distinct variables.
>
> / Ulf
>
> On Wed, Mar 28, 2018 at 6:39 AM, Apostolis Xekoukoulotakis <
> apostolis.xekoukoulotakis at gmail.com> wrote:
>
>> ```
>> module Test2 where
>>
>>
>> data A : Set where
>>
>>
>> CPF : Set
>> CPF = {{a : A}} → A
>>
>> postulate
>>   fun : CPF → CPF
>>   e : CPF
>>
>>
>> bob : CPF
>> bob {{ctx}} = fun (e {{ctx}})
>>
>>
>> rob : CPF
>> rob = fun e
>>
>> ```
>>
>> I wonder if there is a way to write "rob" instead of "bob".
>>
>> Keep in mind that the candidates are definitionally equal. (it seems)
>>
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20180328/685043b0/attachment.html>