[Agda] Instance resolution question

[Apostolis Xekoukoulotakis]

This might work.

(I do want cob and not bob).

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

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