The Coq mailing list

[Helmut Brandl <helmut.brandl AT gmx.net>]

I want to define a module with some basic functionality and then define a functor to augment the functionality. I have the problem that all works fine if I put all definitions in one file and I get a universe violation error if I put them in different files.

E.g. I define an option module with the two monadic functions 'make' and 'bind'.

Module Option.

  Inductive t0 (A:Type) :=

  | None: t0 A

  | Some: A -> t0 A.

  Definition t := t0.

  Arguments None {A}.

  Arguments Some {A} _.

  Definition make {A:Type} (a:A): t A :=

    Some a.

  Definition bind {A B:Type} (m:t A) (f:A->t B): t B :=

    match m with

    | None =>

      None

    | Some v =>

      f v

    end.

End Option.

The I define the functor which augments the functionality of the basic monad.

Module Type MONAD0.

  Parameter t: Type -> Type.

  Parameter make:  forall A:Type, A -> t A.

  Parameter bind:  forall A B:Type, t A -> (A -> t B) -> t B.

End MONAD0.

Module Monad_of (M:MONAD0).

  Import M.

  Arguments bind {A} {B} _ _.

  Arguments make {A} _.

  Polymorphic Definition map {A B:Type} (f:A->B) (m:t A): t B :=

    bind m (fun a => make (f a)).

  Polymorphic Definition apply {A B:Type} (f: t (A->B)) (m: t A): t B :=

    bind f (fun f0 => map f0 m).

End Monad_of.

With that I can define

Module Option1 := Monad_of(Option).

If I put the module type MONAD0 and the functor 'Monad_of' into a different file (let's say 'Monad.v') then the following fails with a universe violation

Require Monad.

Module Option2 := Monad.Monad_of(Option).

For me it should be exactly the same. Can anybody give a hint on what is wrong and on how to remedy the situation. I want to build a library where I can stack many monads arbitrarily on top of each other. If I cannot make the definitions in different files then the situation gets unmanageable.

Thanks for any hint.

Regards

Helmut