Stream: Coq users

Topic: Understanding universe variance rules for cumulativity


view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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