[Agda] Instance resolution question

[Ulf Norell]

You can wrap CPF in data type/record:

record CPF : Set where
  constructor mkCPF
  field unCPF : {{a : A}} → A

postulate
  fun : CPF → CPF
  e   : CPF

rob : CPF
rob = fun e

But note that if it's really `bob` you want, not inserting the {{ctx}} will
give you `cob`, which
is not the same as `bob`:

cob : CPF
cob {{ctx}} = fun (λ {{ctx'}} → e {{ctx'}}) {{ctx}}

/ Ulf

On Wed, Mar 28, 2018 at 7:36 AM, Apostolis Xekoukoulotakis <
apostolis.xekoukoulotakis at gmail.com> wrote:

> 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/7bb3abf9/attachment.html>