The Coq mailing list

[Casteran Pierre <pierre.casteran AT labri.fr>]

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

(* from Cedric AUGER in Cocorico *)

Class Monad (m : Type -> Type) : Type :=
{return_ : forall A, A -> m A;
 bind : forall A, m A -> forall B, (A -> m B) -> m B
 (* some place for laws *)}.


Section monadic_functions.
Variable m : Type -> Type.
Context ( M : Monad m).

Definition join {A:Type} (mma: m (m A)) : m A :=
  bind _ mma _ (fun ma: m A => ma).

End monadic_functions.
About join.
Arguments join { m M A} mma.

Inductive MM (B:Type):  Type :=
  MM_Return (b:B)
| MM_Bind {A :Type}(a:MM  A)(f : A -> MM B) 
| MM_Random (n:nat)(f : nat -> MM B) .

Instance MMM  : Monad MM. 
split;[exact MM_Return | intros A ma B f ; exact (MM_Bind  _ ma f) ].  
Defined.
(*
Check (fun n : MM (MM nat) => join  n): MM (MM nat) -> MM nat.

Error: Universe inconsistency. 

*)