I tried to model a less naive monadic encoding of non-determinism (less naive than MonadPlus and common lists) in Coq that is often used in Haskell; for example the encoding for lists looks like
data List m a = Nil | Cons (m a) (m (List m a))
whereas the corresponding definition in Coq would like as follows.
Inductive List (M: Type -> Type) (A: Type) :=
Nil: List M A
| Cons : M A -> M (List M A) -> List M A.
However, this kind of definition is not allowed in Coq because of the "strictly positive"-condition for inductive data types.
I'm not sure if I am aiming for a Coq-specific answer or an alternative implementation in Haskell that I can formalise in Coq, but I am happy to read any suggestions on how to overcome this problem.
See Chlipala's "Certified Programming with Dependent Types". If you had Definition Id T := T -> T, then List Id could produce a non-terminating term. I think you might also be able to derive a contradiction by Definition Not T := T -> False, especially if you drop the Nil constructor and accept the law of excluded middle.
It would be nice if there were some way to annotate M as only using its argument in positive locations. I think Andreas Abel may have done some work in this direction.
Anyway, if you're willing to restrict your datatypes just a little bit, you could use:
Fixpoint SizedList M A (n : nat) : Type :=
match n with
| 0 => unit
| S m => option (M A * M (SizedList M A m))
end.
Definition List M A := { n : nat & SizedList M A n }.