The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Fri, 21 Jun 2013 11:19:56 +0200,
Casteran Pierre 
<pierre.casteran AT labri.fr>
 a écrit :

> Le 21/06/2013 11:03, Casteran Pierre a écrit :
> > Hi,
> >
> >    I met some problems with the "join" function.
> > using Cédric définitions (taken from Cocorico),
> > everything seems OK until I try to apply join to
> > an instance of an inductive family of types.
> >
> > Happily, bind, return are OK, but a simple application
> > of join gives me a universe inconsistency.
> >
> > Perhaps it's the definition of the MM family that is wrong ?
> > Is there some standard way to solve this issue ?
> >
> > Pierre
> >
> 
> 
> It works better if the definition of the Monad class
> takes bind and return_ as parameters:
> 
> Class Monad' (m : Type -> Type) (return_ : forall A, A -> m A)
>   (bind : forall A, m A -> forall B, (A -> m B) -> m B): Prop :=
> {
>   (* some place for laws *)}.
> 
> Sorry for the spam.
> 
> Pierre
> 
> 
> 

In fact the culprit is not really the definition of the Monad itself.
By unfolding all the calls, you get something which does not involve
Monads at all, and still have the universe constraints problem.

Definition test : MM (MM nat) -> MM nat.
intros n.
apply @MM_Bind with (MM nat).
exact n.
exact (fun x => x).
Defined.