The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Indeed, in the template case partial applications do not give you a fresh instance (because there's no way to know what the fresh levels are in that case, when retyping) , but an eta-expanded version will work I think, e.g fun X => list X, as then we can look at the type of X to determine the type of list X.

On Sat, 22 Oct 2016 at 06:56, Jason Gross <jasongross9 AT gmail.com> wrote:

Template universes are "refreshed" every time you use a fully instantiated version of the inductive, together with a constraint that the new universes are not larger than the original ones, I believe.  So you should be able to write [(list Type) :: nil] but not [list :: nil].

Tangentially, note that template polymorphic universes can be instantiated with [Prop], but universe polymorphic universes can not be so instantiated.

On Fri, Oct 21, 2016, 9:17 PM Gregory Malecha <gmalecha AT gmail.com> wrote:

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