The Coq mailing list

[Frédéric Besson <frederic.besson AT inria.fr>]

Hi, 

To avoid this error message, your inductive type should not be named t
but, say, _t.
Then, you can define t as _t.
Definition t := _t.

This error message has been there for ages. Isn't there a FAQ
explaining the workaround ?

Best,
--
Frédéric


On Mon, 2017-09-11 at 14:36 -0500, Helmut Brandl wrote:
> 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
>