[Agda] A type for positive type functors?

[Dominique Devriese]

Hi,

Is there anyway to represent a positive type functor in the Agda type
system? I'm thinking of the following situation. I can encode a simple
"event handler monad" over Maybe as the base monad as follows:

   data EventHandlerMonad E A : Set where
      mkM : Maybe (A × Maybe (E → EventHandlerMonad E ⊤)) →
EventHandlerMonad E A

   v : EventHandlerMonad ⊤ ⊤
   v = mkM (just (tt , nothing ))
   v2 : EventHandlerMonad ⊤ ⊤
   v2 = mkM (just (tt , just (\_ → v) ))

However, when I try to abstract from Maybe as the base monad like this:

   data EventHandlerMonad M E A : Set where
      mkM : M (A × Maybe (E → EventHandlerMonad M E ⊤)) →
EventHandlerMonad M E A

   v : EventHandlerMonad Maybe ⊤ ⊤
   v = mkM (just (tt , nothing ))
   v2 : EventHandlerMonad Maybe ⊤ ⊤
   v2 = mkM (just (tt , just (\_ → v) ))

I get an error saying that "EventHandlerMonad is not strictly
positive, because it occurs in the second argument to Maybe in the 4th
argument to Σ in an argument to a bound variable in the type of the
constructor mkM in the definition of EventHandlerMonad."

In my use case, M should be a monad, and I have the intuition that
since M is a functor, then in its definition, the argument type cannot
be used in "contravariant" positions, so M must be a positive functor?
However, if this intuition is correct, then there does not seem any
way to communicate this fact to Agda? Even if I require an argument of
type (RawFunctor M), Agda will not notice that M is therefore
positive?

Are my intuitions wrong, or is there some way to achieve what I'm
trying to do in Agda? Any interesting references perhaps?

Thanks for your help,
Dominique