The Coq mailing list

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

Thanks for trying to reproduce the error. However I have found that it has to do something with my installation.

I removed the coq installation completely and reinstalled it via opam. Now I cannot reproduce the problem either. The indicated code works fine in the same file and in a separate file.

Regards

Helmut

2017-09-18 5:18 GMT-05:00 Matthieu Sozeau <mattam AT mattam.org>:

Hi Helmut,

  I can't reproduce your problem with either Coq 8.5(pl2) or Coq 8.6. Could you please report this at http://coq.inria.fr/bugs indicating your version?

Best regards,

-- Matthieu

On Mon, Sep 18, 2017 at 11:00 AM Helmut Brandl <helmut.brandl AT gmx.net> wrote:

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