Stream: Coq users

Topic: Understanding universe variance rules for cumulativity

Sébastien Michelland (Aug 14 2023 at 16:39):

Consider a basic wrapper for a type with some arbitrary extra requirement:

``````Set Printing Universes.
Polymorphic Cumulative Record TypeWrapper@{u} := {
WrapT: Type@{u};
}.
(* TypeWrapper@{u} : Type@{u+1}
(* +u |=  *) *)
``````

When we define it to be universe polymorphic, the universe parameter `u` is covariant, which is no surprise since we can legitimately convert the wrapped type to a Type in a higher universe, but not the other way around.

However, as soon as I use the wrapped type in an inductive:

``````Polymorphic Cumulative Inductive ValueWrapper@{u} (t: TypeWrapper@{u}) :=
| WrapV (v: WrapT t).
(* ValueWrapper@{u} : TypeWrapper@{u} -> Type@{u}
(* =u |=  *) *)
``````

the universe parameter becomes invariant, and I fail to see how having covariant `u` would break the universe hierarchy. By contrast, using a parameter `(t: Type@{u})` with `WrapV (v: t)` makes `u` irrelevant.

• Is there any documentation on how all of this works (I'm pretty sure there isn't but who knows)?
• Where do the covariant/irrelevant outputs for my examples come from?
• Is there a clean way to convert a `ValueWrapper@{u}` to a higher universe `v` when `t` itself can be converted to a `TypeWrapper@{v}`? (Maybe with explicit lifting?)

Gaëtan Gilbert (Aug 14 2023 at 17:03):

the cumulativity of `Ind@{u1 ... un}` is determined by comparing the constructor argument types of `Ind@{u1 ... un}` with the ones at a different instances ie the ones of `Ind@{u1' ... un'}`: `C_i@{u1 ... un} <= C_i@{u1' ... un'}`
additionally the same is done for the indices telescope, and the indices arguments in the return types of the constructors must be convertible (`=` not `<=`) (this doesn't matter for records since there are no indices)
if `uj = uj'` is required then `uj` is invariant
if `uj <= uj'` is required then `uj` is covariant
otherwise `uj` is irrelevant

`WrapT@{u} t` expands to `match t return Type@{u} with Build_TypeWrapper x => x end`
because of the `return Type@{u}`, `WrapT@{u} t <= WrapT@{v} t` implies `u = v` so the universe is invariant

In this case you could use primitive projections, if `TypeWrapper` is primitive then `WrapT t` is normal form and does not mention any universe.

Sébastien Michelland (Aug 18 2023 at 18:05):

Thanks @Gaëtan Gilbert. Primitive projections did solve that issue, avoiding (if I understand correctly) a call to the projection function and thus associated constraints. It took me a while to propagate this change (I've got like 5k lines impacted :sweat_smile: ) but I'm pretty sure now the issues I have left are unrelated.

Last updated: Jun 23 2024 at 05:02 UTC