The Coq mailing list

[Andrej Bauer <andrej.bauer AT andrej.com>]

On Wed, Apr 18, 2012 at 11:03 PM, AUGER Cédric 
<sedrikov AT gmail.com>
 wrote:
> 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.

First, casting to "Type" is not a type annotation because Type is not
a type... Coq gets to choose which one it is, and it can choose Prop.
Second, what about intermediate expressions, how do I type those?

Frederic makes a similar observation:

> I agree with Andrej that this is not a desirable property to do type 
> inference when a type is explicitly given.

Again, and I was confused about this yesterday, Type is not a real
type, so annotating with Type is not a real type annotation. Coq still
has to infer something, namely the level, and as Hugo explained to me,
the levels go
Prop < Set < ... < Type(k) < ... Coq picks the lowest available.

With kind regards,

Andrej