Syntax for explicit universe levels

[JasonGross]

If we provide a syntax for explicit universe levels, @mattam82 has said that he will provide it.

I propose something like the following:

Definition foo {universes i <= j, Set < k < i, ℓ = max(m, n), p}
  (A B : Type i) (C : Type j) (D : Type k) (E : Type m) (F : Type n) (G : Type) (H : Type p)
 : Type ℓ

The semantics are: If you take the transitive closure of the final universe graph, and drop any constraints involving a universe not in the list of explicit "universes", then that graph should be exactly the transitive closure of the given graph. (Coq may add any constraints to the definition it needs to in order to achieve this; for example, it may augment the initial constraint list with the ones mentioned explicitly) This means, for example, that if you mention a universe without giving any constraints, it should be unconstrained by the other universes you mention.

[JasonGross]

I forgot to add, I've opened this issue to request agreement on this syntax, and/or suggestions for other syntax or improvements of this syntax.

[JasonGross]

Here is a way to implement a weaker version of the semantics with slightly uglier notation (I haven't checked too carefully that it works):

Require Import Coq.Init.Datatypes Coq.Init.Specif Coq.Init.Notations Coq.Init.Logic.
Set Universe Polymorphism.

Delimit Scope universe_constraints with univs.

Definition universes (_ : Type) : Set := forall P : Prop, P.

Arguments universes _%univs.

Notation "( x , y , .. , z )" := (prod .. (prod x%univs y%univs) .. z%univs) : universe_constraints.

Notation typeof x := ($(let t := type of x in exact t)$) (only parsing).
Notation "i <= j" := ($(let enforce := constr:(fun x : i%univs => (x : j%univs)) in exact j%univs)$) (only parsing) : universe_constraints.
Notation "i < j" := ($(let enforce := constr:(i%univs : j%univs) in exact j%univs)$) (only parsing) : universe_constraints.
Notation "i >= j" := ($(let enforce := constr:(fun x : j%univs => (x : i%univs)) in exact j%univs)$) (only parsing) : universe_constraints.
Notation "i > j" := ($(let enforce := constr:(j%univs : i%univs) in exact j%univs)$) (only parsing) : universe_constraints.
Notation "i = j" := ($(let enforce := constr:((i%univs <= j%univs, j%univs <= i%univs)%univs) in exact j%univs)$) (only parsing) : universe_constraints.
Notation "max[ i , j ]" := ($(let ret := constr:(Type) in let enforce := constr:((i%univs <= ret, j%univs <= ret)%univs) in exact ret)$) (only parsing) : universe_constraints.

Definition foo
  (A B : Type) (C : Type) (D : Type) (E : Type) (F : Type) (G : Type) (H : Type) (U := Type)
  (cs : Set := universes (typeof A = typeof B, typeof B <= typeof C, Set < typeof D, typeof D < typeof A, U = max[typeof E, typeof F]%univs, typeof H))
 : U.
Admitted.
Set Printing Universes.
Print foo.