[Agda] A type for positive type functors?

[Dominique Devriese]

Andreas,

2010/11/18 Andreas Abel <andreas.abel at ifi.lmu.de>:
> in your case, I am afraid, you have to turn off the positivity checker.
>  Agda checks positivity by unfolding definitions, this is why the concrete
> version with Maybe works.  However, if you abstract Maybe to a variable M,
> positivity hold only if M is positive itself.
>
> Currently Agda cannot handle this.  In my toy language MiniAgda it works,
> because you can declare M to be strictly positive as follows:
>
>  data EventHandlerMonad ++(M : Set -> Set) (E : Set) (A : Set) : Set ...
>
> telling the positivity checker that M is assumed to be strictly positive and
> can only be instantiated with strictly positive type functions.

This is indeed the sort of thing I was hoping to find. Too bad it
doesn't exist in Agda. I will try to find a different solution for my
problem.

Dominique