The Coq mailing list

[Stéphane Glondu <steph AT glondu.net>]

Le 18/04/2012 13:36, Andrej Bauer a écrit :
> I am not proposing an incompatibility change, I think. I am proposing
> that the type should be honored when explicitly given. Because I
> explicitly defined that Q should map to Type, it should map to Type.
> If I asked Coq to _infer_ the type and it decided it was Prop, then I
> would have no objection. But as far as I am concerned this is a bug.

This is not a bug for me, merely an unfortunate convention.

"Type" in this position means "infer", whereas most of the time it means
"a new universe". As far as I know, there is no syntax for "a new
universe" in this position. The "infer" semantics is needed for universe
polymorphism.

If you want "a new universe", you can (as you've figured out) define a
constant to be "Type" (which will effectively create a new universe),
and use that constant. Yes, it will fix the level, but I don't see how
you can avoid that: inductive types can be polymorphic only in the types
of parameters, not the return sort.


Cheers,

-- 
Stéphane