[Agda] Generic programming and pointfree stuff.

[flicky frans]

I forgot to send the mail to Agda mailing list. Andreas Abel, sorry
for the duplicate.
----
Thanks for answering.

>No, but you could try the development version of Agda (get from the
>darcs repo) which has some performance improvements.  (Might be worth
>trying.)
I tried, but got this error:

C:\Documents and Settings\ 4<8=8AB at 0B>@\Application
Data\cabal\Agda-2.3.3\lib\prim\Agda\Primitive.agda: openFile:
invalid argument (Invalid argument)

Locale problems. I searched for a way to unhardcode the path, but
didn't find it. Is there any?

>Conversion checking for Level is certainly incomplete.  Levels are not
>meant for complicated computations.
Previous version of this code typechecks. Last definition in this
messy module: http://lpaste.net/8416145096918958080
It's more complicated however. Just for the statistics: how many such
a bugs with levels have you seen?

>You could file a bug report (google for "agda issues") with a file
>that reproduces the problematic behavior.

I have no idea how to reproduce this bug with a smaller amount of code.

Thanks again.