The Coq mailing list

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

Dear list,

I have the following module types

Module Type MONAD.

  Parameter t: Type -> Type.

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

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

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

End 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.

and the module functor

Module Monad_of (M:MONAD0).

  Definition t := M.t.

  Definition bind := M.bind.

  Definition make := M.make.

  Arguments bind {A} {B} _ _.

  Arguments make {A} _.

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

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

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

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

End Monad_of.

I wanted to use the following module as a module argument for the previous functor

Module Option.

  Inductive t (A:Type) :=

  | None: t A

  | Some: A -> t A.

  Check t.

  Arguments None {A}.

  Arguments Some {A} _.

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

    Some a.

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

    match m with

    | None =>

      None

    | Some v =>

      f v

    end.

  Check make.

End Option.

Module Option1 := Monad_of(Option).

With the last line the compiler complains with the message "The kernel does not recognize yet that a parameter can be instantiated by an inductive type. Hint: you can rename the inductive type and give a definition to map the old name to the new name."

Can anybody help me to understand this error message and give me a hint on how to fix this problem?

Thanks

Helmut