The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Hi,

I have the following example:

Set Printing Universes.

Set Printing All.

Definition bar (A : Type) := { _ : A | True }.

Record baz (A : Type) := { qux : A }.

Definition foo (A : Type) := baz A.

Definition foo' (A : Set) := baz A.

Check bar nat. (* Type (* Top.238 *) *)

Check baz nat. (* Set *)

Check foo nat. (* Type (* Top.258 *) *)

Check foo' nat. (* Set *)

I was wondering if someone could explain to me why [Check baz nat] gives [Set], but the other two don't, or, more precisely, why it should be this way?  Adam conjectured that fake universe polymorphism only happens for inductive definitions, and that seems to mostly explain these results, and http://coq.inria.fr/refman/Reference-Manual006.html#@default346 supports that.  But it seems rather unfortunate that I can't, for example, define an alternate version of an inductive polymorphic type that switches parameter order, and, worse, that if I want an inductive type to be polymorphic, I have to expand out all my [Definition]s that I use inside of it manually.

Does anyone know a good way to get around this, or if there are plans to make [Definition]s support sort-polymorphism?  (Should I submit a feature request on the coq bug-list page?)

Thanks.

-Jason