The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Coq accepts the following snippet, which declares a universe-polymorphic type that lives in a successor universe: 

Polymorphic Inductive pack@{i} : Type@{i+1} :=

  Pack { sort : Type@{i}; elt : sort }.

However, if I try to take the successor of a universe level elsewhere, I get a parse error:

Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) : pack@{i+1} :=

  Pack pack@{i} (Pack@{i} T x).

(* Toplevel input, characters 65-66: *)

(* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) : pack@{i+1} :=   Pack pack@{i} (Pack@{i} T x). *)

(* >                                                                  ^ *)

(* Error: Syntax error: [constr:universe_level] or '}' expected (in [instance]). *)

If I omit the annotation, Coq complains that I haven't declared the universe where the definition should live:

Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=

  Pack pack@{i} (Pack@{i} T x).

(* Toplevel input, characters 61-65: *)

(* > Polymorphic Definition pack2@{i} (T : Type@{i}) (x : T) :=   Pack pack@{i} (Pack@{i} T x). *)

(* >                                                              ^^^^ *)

(* Error: Universe {Top.72} is unbound. *)

Is there any way of convincing Coq that pack2's codomain is pack@{i+1}?

Thanks!

Best,

Arthur