The Coq mailing list

[Gregory Malecha <gmalecha AT gmail.com>]

Hello --

I've been tracking down universe issues the last few days and I keep running into issues surrounding standard library code that is not universe polymorphic but template universe polymorphic. My naive understanding of template universe polymorphism is that the type is "refreshed" every time that it is used. It is kind of like universe polymorphism, but not quite. This is what lets you have [list nat] and [list { x : nat & ... }]. Given this understanding, it seems not inconceivable that you could write the term `list :: nil` by setting up the universes appropriately. However, this seems impossible to write in Coq. Is there a description of template universe polymorphism somewhere that I could read?

Thanks.

Set Printing Universes.

Universe A.

Definition x : list (Type@{A} -> Type@{A}).

  refine (cons (@list) nil). (** fails **)

Abort.

With polymorphic lists (a.la. ExtLib) everything works out well.

Polymorphic Inductive plist@{A} (T : Type@{A}) : Type@{A} :=

| pnil

| pcons (_ : T) (_ : plist T).

Definition x : plist (Type@{A} -> Type@{A}).

  refine (@pcons (Type@{A} -> Type@{A}) (@plist@{A}) (@pnil _)).

Defined.

--

- gregory malecha
  gmalecha.github.io