The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Hello.

I agree with Andrej that this is not a desirable property to do type 
inference when a type is explicitly given. Is this documented somewhere? 
Anyway, the minimum would be to output some warning saying that the 
inductive type in fact lives in a different universe than the one given 
by the user.

In a variant of Andrej's example, giving no type has indeed the same effect:

Parameter A : Type.
Inductive Q' (x : A) := horn : Q' x.
Check Q'.
Q'
     : A -> Prop
Inductive Q (x : A) : Type := h : Q x.
Check Q.
Q
     : A -> Prop

Frederic.

Le 19/04/2012 05:03, AUGER Cédric a écrit :
> Le Wed, 18 Apr 2012 13:51:07 +0200,
> Andrej 
> Bauer<andrej.bauer AT andrej.com>
>   a écrit :
>
> > Here is another way to circumvent the problem, I think. First we
> > define the offending type which lands in Prop, then we define an alias
> > for it:
> >
> > Parameter A : Type.
> > Definition cow (P : forall (x : A), A ->  Type) : Type := forall x y :
> > A, P x y. Inductive Q' (x : A) : A ->  Type := horn : Q' x x.
> > Definition Q : A ->  A ->  Type := Q'.
> > Definition q := cow Q.
> > Definition r := forall x y : A, Q x y.
> >
> > Now r is in Type. But this still deserves to be a bug.
> >
> > With kind regards,
> >
> > Andrej
> Parameter A : Type.
> Definition cow (P : forall (x : A), A ->  Type) : Type := forall x y :
> A, P x y. Inductive Q (x : A) : A ->  Type := horn : Q x x.
> Definition q := cow Q.
> Definition r : Type := forall x y : A, Q x y.
>               ^^^^^^
> isn't type casting simpler than defining Q' ?
> I always found that giving explicitely the type of a symbol at top
> level was nicer that making the reader to mentaly perform the type
> inference.
>
> There r is really in Type and no more in Prop.