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

[Ulf Norell]

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
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20150407/01bf8cf3/attachment.html