The Coq mailing list

[Arnaud Spiwack <aspiwack AT lix.polytechnique.fr>]

Indeed, the problem is the universe of A in the constructor MM_bind: it has to be a lower universe than that of MM. As a consequence [@MM_bind (MM nat) n] only typechecks thanks to universe polymorphism. It has type [(MM nat -> MM' nat) -> MM' nat] (where MM' means MM but one universe higher). It cannot be passed the identity function.

It may not work in general, but in this particular case, the definition of the free monad over Random is:

Inductive MM (B:Type):  Type :=
  MM_Return (b:B)
| MM_Random (n:nat)(f : nat -> MM B) .

MM_Bind can be defined by recursion. And I think (not tested) that join will work as expected.

On 21 June 2013 21:59, AUGER Cédric <sedrikov AT gmail.com> wrote:

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.