The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

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.