Implementation details of Coq universes are pushed onto the user (aka Algebraic universes are a pain)

[kyoDralliam]

Description of the problem

In the following definition, the argument t cannot be instantiated because its type contains an algebraic universe u+1. As a first feature request, it would be great to warn or to error at the point of definition rather than in all subsequent attempts of applying tnat.

Polymorphic (* same error w/o*)
  Definition tnat@{u} (t : Type@{u} -> Type@{u+1}) := t nat.

Fail Check (tnat list).
(* Error: Algebraic universe on the right *)

Inductive indexed_id@{u} : Type@{u} -> Type@{u+1} :=
| diag : forall (A : Type@{u}), indexed_id A.

Fail Check (tnat indexed_id).

The current fix of the above code that I'm aware of is the following

Definition tnat'@{u v | u < v} (t : Type@{u} -> Type@{v}) := t nat.
Check tnat' list.
Check tnat' indexed_id.

This is more general but it doubles the number of universe probably making universe debugging harder in larger context and loses the fact that v can be taken to be the smallest universe greater than u. The main problem however is that it imposes to the user to be aware of the implementation details of the algebraic universe so that they can encode their example in Coq...

So the second feature request is to have a way for Coq to handle such functional constraints between universes (v is determined by u in the previous example) transparently for the user.

Coq Version

8.10.2, master 6f2b88649ec0c1e27befe7bcd2cdbec0ccee95d6

[ppedrot]

cc @mattam82

[kyoDralliam]

Also a bit puzzled by this example

Polymorphic Inductive indexed_id@{u} : Type@{u} -> Type@{u+1} :=
| diag : forall (A : Type@{u}), indexed_id A.

Fail Definition test@{u} : Type@{u+1} := sigT indexed_id.
(* Algebraic universe on the right *)
Definition test@{u} : Type@{u+1} := sigT indexed_id@{u}.

Why does the explicit universe application change anything ?

Continuing my investigation, the second example fails when sigT is made universe polymorphic:

Polymorphic Inductive psigT@{a b} {A : Type@{a}} (B : A -> Type@{b}) :=
  | pexistT : forall a, B a -> psigT B.

Fail Definition ptest@{u} : Type@{u+1} := psigT indexed_id@{u}.

Not sure what I was expecting there...

[ppedrot]

It probably changes the way universe unification is performed. In the first case a fresh universe is generated and is tentatively unified with an algebraic universe, which fails.

[SkySkimmer]

sigT is template poly so you get v+1 <= u+1 (where v is the fresh one) and universe inference doesn't handle that.

[kyoDralliam]

So does that mean that the Algebraic universe on the right error is used for two distinct (but closely related) problems: the first one is a universe inference failure and the second one is an actual limitation due to some restriction to non-algebraic universes in some places ?

Understanding this partially solves one of the issues I had at the beginning (in the polymorphic case):

Section Foo.
  Universe u.
  Fail Check (tnat@{u} list). (* list is template poly, can't be applied to any universes *)
  Fail Check (tnat indexed_id@{u}).
  Fail Check (tnat@{u} indexed_id).
  Check (tnat@{u} indexed_id@{u}).
End Foo.

[kyoDralliam]

Yet another quirky case, when a polymorphic universe level is unconstrained:

Polymorphic Inductive strange@{u v} : Type@{u} -> Type@{u+1} :=
  | mkStrange : forall (A : Type@{u}), strange A.

Fail Definition ntest@{v u} : Type@{u+1} := sigT strange@{v u}.

Also fails if sigT is replaced by a universe-polymorphic version, or by a record (with and w/o primitive projections, with and without universe-polymorphism). That annoys me because the concrete case I want to work with actually have this kind of example...

[SkySkimmer]

Not sure what else you would expect from that code.

That annoys me because the concrete case I want to work with actually have this kind of example...

Using explicit algebraic universes is not really supported, if your goal is anything other than trying to understand the implementation I recommend you stop.

[kyoDralliam]

Using explicit algebraic universes is not really supported, if your goal is anything other than trying to understand the implementation I recommend you stop.

Looking at these examples that sounds like a sane advice. I can indeed write my code using the encoding above (but I need 4 universes where I would expect only one in a pen&paper proof). Besides complaining I'm also interested in understanding what's happening inside Coq and what can be improved. Shouldn't coq warn the user by default when it finds algebraic universes in the source for instance ?

[SkySkimmer]

https://github.com/coq/coq/pull/7490 was attempted and abandoned. Maybe I got too ambitious with the kernel check and should have stayed with only the pretyper check.

[kyoDralliam]

That's good to know, I was not aware of this attempt. Preventing the user from writing algebraic universes in places not really supported by coq looks like a good move so that users like me do not get wrong expectations (but warning/documenting more clearly the use of universes in coq may have a more direct effect).

However, it does not help with the universe proliferation and the difficulty to debug a universe inconsistency at the end of your project (if you haven't paid much attention to universes, you suddenly realize that there is a massive amount of them around when something breaks and it is hard to find the faulty constraint). From what I understood, the limitation on algebraic universes is of algorithmic nature: if algebraic universes are accepted anywhere, universe constraint solving can get badly exponential in the number of universes and constraints (correct me if I'm wrong).

In practice, it was observed that in a cumulative, covariant system like coq, there is no real loss (is there ?) to restrict most of the language to universe variables and constraints of the shape u <= v or u < v. In particular +1 and max seem rarely needed for actual development and can be replaced by fresh universe variables with the adequate constraints. But it's still an encoding... Would it be possible to provide the user with facilities to deal with these encoding ? More precisely could we add to the universe term algebra 2 function symbols above (unary) and bound (n-ary) such that u < above u for any universe level u and vi <= bound v1 .. vn for any sequence vi of universe levels ? These two function symbols are clearly definable in the current (restricted) system by adding new universe variables and constraints but providing them would allow the user to concentrate on which universes matters wrt his development.