[Agda] A problem with instance arguments and function application.

[effectfully]

Thanks for the explanations, Ulf Norell.

2015-04-07 17:02 GMT+04:00, Ulf Norell <ulf.norell at gmail.com>:
> You would think that Agda could infer that f x should have function type
> when it's applied to y,
> but the problem is it doesn't know if it should be an implicit or explicit
> function space. The handling
> of implicit argument insertion and implicit function spaces is quite
> unsatisfactory at the moment,
> which shows up in cases like yours. We are thinking about possible fixes,
> but don't hold your breath.
>
> / Ulf
>
> On Tue, Apr 7, 2015 at 2:07 PM, effectfully <effectfully at gmail.com> wrote:
>
>> Sorry, I described a problem, but didn't include an illustrative
>> example in the code. Fixed now: it's at the bottom of the module and
>> called "yellow".
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>