The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Thanks!

If what you mean by "not actually effective" is the comment at the bottom of  http://www.lix.polytechnique.fr/coq/bugs/show_bug.cgi?id=2298, it seems like it was at least partially effective.  For example, when I build coq at the revision right before that revert, I can do

Set Printing Universes.

Polymorphic Definition foo (a : Type) := a.

Definition foo' (a : Type) := a.

Check foo. (* Type (* Top.1 *) -> Type (* Top.1 *) *)

Check foo'.(* Type (* Top.23 *) -> Type (* Top.23 *) *)

Check foo nat. (* Set *) 

Check foo' nat. (* Set *)

However, in Coq 8.4beta2, I get [Type (* Top.1 *) -> Type (* Top.1 *)] for [foo'], but I get [Type (* Top.1 *)] for [foo' nat].

I can imitate the sort-polymorphic behavior using

Record foo' (a : Type) := { foo'_Member : a }.

(and for definitions where the head of the body is a global class, rather than a passed argument, I can use [:>] instead of [:] and get something closer to the functionality that I want).

It's not clear to me that the test listed in that bug report is a good test of sort-polymorphic definitions that conform to existing sort-polymorphic behavior in Coq; when I translate that example to [Record] syntax, I get

Inductive paths {A:Type} : A -> A -> Type :=

  idpath : forall x : A, (paths  x  x).

Record is_contr (A:Type) := { is_contr_ :> {x : A & forall y : A, (paths y x)} }.

Record is_prop (A:Type):= { is_prop_ :> forall (x y:A), is_contr (paths x  y) }.

Record is_set (A:Type):= { is_set_ :> forall (x y:A), is_prop (paths x  y) }.

Record hProp:={ hProp_ :> (sigT is_prop) }.

Check (is_set hProp).

and the last line of this gives me a universe inconsistency, too.

Was there some other problem with it?

-Jason

On Sat, Jul 21, 2012 at 1:03 AM, Tom Prince <tom.prince AT ualberta.net> wrote:

Jason Gross <jasongross9 AT gmail.com> writes:

> Hi,
> I noticed that Coq seems to have had universe polymorphism at one point,
> but no longer does (see commit message at the bottom of the message).  Is
> there somewhere that I can find an explanation of why this was removed, or
> can someone respond with an explanation?  (If it was discussed on coq-club
> before, are there archives of coq-club@, and can someone point me to them?)

coq has for a long time had a limited support for universe polymorphism
for inductive types. The commit you reference was an attempt at adding
more support, but it wasn't actually effective (hence the revert).

  Tom