Add sort cumulativity for polymorphic inductive types

checker/checkInductive.ml

@@ -97,13 +97,15 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
       mb.mind_packets
   in
   let mind_entry_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_variance in
+  let mind_entry_sort_variance = Option.map (Array.map (fun v -> Some v)) mb.mind_sort_variance in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
     mind_entry_params;
     mind_entry_inds;
     mind_entry_universes;
     mind_entry_variance;
+    mind_entry_sort_variance;
     mind_entry_private = mb.mind_private;
   }
 
@@ -210,6 +212,7 @@ let check_inductive env mind mb =
   let { mind_packets; mind_finite; mind_hyps; mind_univ_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
         mind_universes; mind_template; mind_variance; mind_sec_variance;
+        mind_sort_variance; mind_sec_sort_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
@@ -236,6 +239,9 @@ let check_inductive env mind mb =
   check "mind_variance" (Option.equal (Array.equal UVars.Variance.equal)
                            mb.mind_variance mind_variance);
   check "mind_sec_variance" (Option.is_empty mind_sec_variance);
+  check "mind_sort_variance" (Option.equal (Array.equal UVars.Variance.equal)
+                           mb.mind_sort_variance mind_sort_variance);
+  check "mind_sec_sort_variance" (Option.is_empty mind_sec_sort_variance);
   ignore mind_private; (* passed through Indtypes *)
 
   ignore mind_typing_flags;

checker/values.ml

@@ -482,6 +482,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_opt v_template_universes;
     v_opt (v_array v_variance);
     v_opt (v_array v_variance);
+    v_opt (v_array v_variance);
+    v_opt (v_array v_variance);
     v_opt v_bool;
     v_typing_flags|]
 

doc/changelog/01-kernel/21770-sort-cumulativity-Added.rst

@@ -0,0 +1,6 @@
+- **Added:**
+  :flag:`Polymorphic Inductive Sort Cumulativity` to allow sorts in the same
+  connected component ({Prop, Type/Set} or {SProp}) to be treated as equivalent
+  at quality positions with non-Invariant inferred variance in cumulative inductives
+  (`#21770 <https://github.com/rocq-prover/rocq/pull/21770>`_,
+  by Jason Gross).

doc/sphinx/addendum/universe-polymorphism.rst

@@ -433,6 +433,27 @@ Insufficiently restrictive variance annotations lead to errors:
           Defined.
       End down.
 
+Sort Cumulativity
+~~~~~~~~~~~~~~~~~
+
+.. flag:: Polymorphic Inductive Sort Cumulativity
+
+   When this :term:`flag` is on (it is off by default), it enables sort
+   cumulativity for cumulative polymorphic inductive types. This means that
+   sort/quality positions with non-Invariant inferred variance allow sorts in
+   the same connected component to be treated as equivalent. The connected
+   components are:
+
+   - ``{Prop, Type/Set}`` (both "relevant" sorts)
+   - ``{SProp}`` (alone)
+
+   For example, with sort cumulativity enabled, a cumulative polymorphic
+   inductive ``Iso@{s s'; u u'}`` declared at ``Iso@{Prop Prop; Set Set}``
+   can be used where ``Iso@{Type Prop; Set Set}`` is expected, because
+   ``Prop`` and ``Type`` are in the same connected component.
+
+   This flag requires :flag:`Polymorphic Inductive Cumulativity` to be on.
+
 Cumulativity Weak Constraints
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 

engine/eConstr.ml

@@ -757,7 +757,8 @@ let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
   | Some variances ->
     let num_param_arity = Conversion.inductive_cumulativity_arguments spec in
     if not (Int.equal num_param_arity nargs) then enforce_eq_instances_univs false u1 u2 cstrs
-    else compare_cumulative_instances cv_pb  variances u1 u2 cstrs
+    else
+      compare_cumulative_instances cv_pb variances ?sort_variance:mind.Declarations.mind_sort_variance u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
@@ -768,6 +769,7 @@ let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs
     else
+      let u1, u2 = UVars.normalize_sort_cumul_instances mind.Declarations.mind_sort_variance u1 u2 in
       let qs1, us1 = UVars.Instance.to_array u1
       and qs2, us2 = UVars.Instance.to_array u2 in
       let cstrs = enforce_eq_qualities qs1 qs2 cstrs in

engine/evarutil.ml

@@ -764,7 +764,8 @@ let subterm_source evk ?where (loc,k) =
 
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
-let compare_cumulative_instances cv_pb variances u u' sigma =
+let compare_cumulative_instances cv_pb variances ?sort_variance u u' sigma =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let open UnivProblem in
   let cstrs = Univ.UnivConstraints.empty in
   let soft = Set.empty in
@@ -788,7 +789,8 @@ let compare_cumulative_instances cv_pb variances u u' sigma =
     Inl (Evd.add_constraints sigma soft)
   | exception UGraph.UniverseInconsistency p -> Inr p
 
-let compare_constructor_instances evd u u' =
+let compare_constructor_instances ?sort_variance evd u u' =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let open UnivProblem in
   let qs, us = UVars.Instance.to_array u
   and qs', us' = UVars.Instance.to_array u' in

engine/evarutil.mli

@@ -180,6 +180,7 @@ val eq_constr_univs_test :
    Additionally flexible universes in irrelevant positions are unified
    if possible. Returns [Inr p] when the former is impossible. *)
 val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array ->
+  ?sort_variance:UVars.Variance.t array ->
   UVars.Instance.t -> UVars.Instance.t -> evar_map ->
   (evar_map, UGraph.univ_inconsistency) Util.union
 
@@ -188,7 +189,7 @@ val compare_cumulative_instances : Conversion.conv_pb -> UVars.Variance.t array
 
     But what about qualities?
 *)
-val compare_constructor_instances : evar_map ->
+val compare_constructor_instances : ?sort_variance:UVars.Variance.t array -> evar_map ->
   UVars.Instance.t -> UVars.Instance.t -> (evar_map, UGraph.univ_inconsistency) Util.union
 
 (** {6 Unification problems} *)

engine/polyFlags.ml

@@ -12,26 +12,31 @@ type t = {
   univ_poly : bool;
   collapse_sort_variables : bool;
   cumulative : bool;
+  sort_cumulative : bool;
 }
 
-let make ~univ_poly ~collapse_sort_variables ~cumulative =
+let make ~univ_poly ~collapse_sort_variables ~cumulative ~sort_cumulative =
   if cumulative && not univ_poly then
     CErrors.user_err Pp.(str "Cannot have cumulative but not universe polymorphic constructions");
+  if sort_cumulative && not cumulative then
+    CErrors.user_err Pp.(str "Sort cumulativity requires universe cumulativity.");
   if not collapse_sort_variables && not univ_poly then
     CErrors.user_err Pp.(str "Sort metavariables must be collapsed to Type in universe monomorphic constructions");
-  { collapse_sort_variables; univ_poly; cumulative }
+  { collapse_sort_variables; univ_poly; cumulative; sort_cumulative }
 
-let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false }
+let default = { collapse_sort_variables = true; univ_poly = false; cumulative = false; sort_cumulative = false }
 let of_univ_poly b = { default with univ_poly = b }
 
 let collapse_sort_variables x = x.collapse_sort_variables
 let univ_poly x = x.univ_poly
 let cumulative x = x.cumulative
+let sort_cumulative x = x.sort_cumulative
 
 let pr f =
   let open Pp in
   str "{ univ_poly = " ++ bool f.univ_poly ++ spc () ++
   str "; cumulative = " ++ bool f.cumulative ++ spc () ++
+  str "; sort_cumulative = " ++ bool f.sort_cumulative ++ spc () ++
   str "; collapse_sort_variables = " ++ bool f.collapse_sort_variables ++ spc () ++
   str "}"
 

engine/polyFlags.mli

@@ -16,7 +16,7 @@ type t
  *)
 
 (** Raises a user error if [univ_poly = false] and either [collapse_sort_variables = false] or [cumulative = true]. *)
-val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> t
+val make : univ_poly:bool -> collapse_sort_variables:bool -> cumulative:bool -> sort_cumulative:bool -> t
 
 (** The [default] is monomorphic:
     [univ_poly] and [cumulative] are [false], [collapse_sort_variables] is [true] *)
@@ -32,6 +32,7 @@ val of_univ_poly : bool -> t
 val univ_poly : t -> bool
 val collapse_sort_variables : t -> bool
 val cumulative : t -> bool
+val sort_cumulative : t -> bool
 
 (** Pretty print *)
 val pr : t -> Pp.t

engine/univProblem.ml

@@ -127,7 +127,8 @@ let enforce_eq_qualities qs qs' cstrs =
       if Sorts.Quality.equal a b then c else Set.add (QEq (a, b)) c)
     cstrs qs qs'
 
-let compare_cumulative_instances  cv_pb variances u u' cstrs =
+let compare_cumulative_instances  cv_pb variances ?sort_variance u u' cstrs =
+  let u, u' = UVars.normalize_sort_cumul_instances sort_variance u u' in
   let make u = Sorts.sort_of_univ @@ Univ.Universe.make u in
   let qs, us = UVars.Instance.to_array u
   and qs', us' = UVars.Instance.to_array u' in

engine/univProblem.mli

@@ -49,4 +49,4 @@ val enforce_eq_instances_univs : bool -> Instance.t constraint_function
 
 val enforce_eq_qualities : Sorts.Quality.t array constraint_function
 
-val compare_cumulative_instances : Conversion.conv_pb -> Variance.t array -> Instance.t constraint_function
+val compare_cumulative_instances : Conversion.conv_pb -> Variance.t array -> ?sort_variance:Variance.t array -> Instance.t constraint_function

kernel/conversion.ml

@@ -151,7 +151,7 @@ type conv_pb =
 type ('a, 'err) universe_compare = {
   compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
   compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
-  compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
+  compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
     UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
@@ -169,15 +169,15 @@ let convert_instances ~flex u u' (s, check) =
 
 exception MustExpand
 
-let convert_instances_cumul pb var u u' (s, check) =
-  (check.compare_cumul_instances pb var u u' s, check)
+let convert_instances_cumul pb var sort_var u u' (s, check) =
+  (check.compare_cumul_instances pb var sort_var u u' s, check)
 
-let get_cumulativity_constraints cv_pb variance u u' =
+let get_cumulativity_constraints cv_pb variance sort_variance u u' =
   match cv_pb with
   | CONV ->
-    UVars.enforce_eq_variance_instances variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
+    UVars.enforce_eq_variance_instances variance ?sort_variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
   | CUMUL ->
-    UVars.enforce_leq_variance_instances variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
+    UVars.enforce_leq_variance_instances variance ?sort_variance u u' (UVars.QPairSet.empty, Univ.UnivConstraints.empty)
 
 let inductive_cumulativity_arguments (mind,ind) =
   mind.Declarations.mind_nparams +
@@ -192,7 +192,7 @@ let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2
       (* shortcut, not sure if worth doing, could use perf data *)
       if UVars.Instance.equal u1 u2 then Result.Ok s else raise MustExpand
     else
-      cmp_cumul cv_pb variances u1 u2 s
+      cmp_cumul cv_pb variances mind.Declarations.mind_sort_variance u1 u2 s
 
 type 'e conv_tab = {
   cnv_inf : clos_infos;
@@ -227,9 +227,8 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u
     else
       (** By invariant, both constructors have a common supertype,
           so they are convertible _at that type_. *)
-      (* NB: no variance for qualities *)
       let variance = Array.make (snd (UVars.Instance.length u1)) UVars.Variance.Irrelevant in
-      cmp_cumul CONV variance u1 u2 s
+      cmp_cumul CONV variance mind.Declarations.mind_sort_variance u1 u2 s
 
 let convert_constructors ctor nargs u1 u2 (s, check) =
   convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -780,7 +779,7 @@ and eqwhnf cv_pb l2r infos (lft1, (hd1, v1) as appr1) (lft2, (hd2, v2) as appr2)
     | FArray (u1,t1,ty1), FArray (u2,t2,ty2) ->
       let len = Parray.length_int t1 in
       if not (Int.equal len (Parray.length_int t2)) then raise NotConvertible;
-      let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] u1 u2 cuniv in
+      let cuniv = fail_check infos @@ convert_instances_cumul CONV [|UVars.Variance.Irrelevant|] None u1 u2 cuniv in
       let el1 = el_stack lft1 v1 in
       let el2 = el_stack lft2 v2 in
       let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
@@ -862,7 +861,7 @@ and convert_stacks ?(mask = [||]) l2r infos lft1 lft2 stk1 stk2 cuniv =
                     let u2 = CClosure.usubst_instance e2 u2 in
                     match mind.Declarations.mind_variance with
                     | None -> convert_instances ~flex:false u1 u2 cu
-                    | Some variances -> convert_instances_cumul CONV variances u1 u2 cu
+                    | Some variances -> convert_instances_cumul CONV variances mind.Declarations.mind_sort_variance u1 u2 cu
                 in
                 let cu = fail_check infos cu in
                 let pms1 = mk_clos_vect e1 pms1 in
@@ -993,8 +992,8 @@ let check_convert_instances qeq = (); fun ~flex:_ u u' state ->
   else Result.Error None
 
 (* general conversion and inference functions *)
-let check_inductive_instances qeq = (); fun cv_pb variance u1 u2 state ->
-  let qcsts, ucsts = get_cumulativity_constraints cv_pb variance u1 u2 in
+let check_inductive_instances qeq = (); fun cv_pb variance sort_variance u1 u2 state ->
+  let qcsts, ucsts = get_cumulativity_constraints cv_pb variance sort_variance u1 u2 in
   let check_quality (q1, q2) = qeq q1 q2 in
   if UVars.QPairSet.for_all check_quality qcsts && UGraph.check_constraints ucsts state
   then Result.Ok state

kernel/conversion.mli

@@ -25,15 +25,15 @@ type conv_pb = CONV | CUMUL
 type ('a, 'err) universe_compare = {
   compare_sorts : conv_pb -> Sorts.t -> Sorts.t -> 'a -> ('a, 'err option) result;
   compare_instances: flex:bool -> UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
-  compare_cumul_instances : conv_pb -> UVars.Variance.t array ->
+  compare_cumul_instances : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
     UVars.Instance.t -> UVars.Instance.t -> 'a -> ('a, 'err option) result;
 }
 
 type ('a, 'err) universe_state = 'a * ('a, 'err) universe_compare
 
 type ('a, 'err) generic_conversion_function = ('a, 'err) universe_state -> constr -> constr -> ('a, 'err option) result
 
-val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array ->
+val get_cumulativity_constraints : conv_pb -> UVars.Variance.t array -> UVars.Variance.t array option ->
   UVars.Instance.t -> UVars.Instance.t -> UVars.QPairSet.t * Univ.UnivConstraints.t
 
 val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int

kernel/declarations.mli

@@ -298,6 +298,13 @@ type mutual_inductive_body = {
        outside sections. The final variance once all sections are
        discharged is [mind_sec_variance ++ mind_variance]. *)
 
+    mind_sort_variance : UVars.Variance.t array option;
+    (** Sort/quality variance info, [None] when no sort cumulativity. *)
+
+    mind_sec_sort_variance : UVars.Variance.t array option;
+    (** Sort variance info for section polymorphic qualities. [None]
+       outside sections. *)
+
     mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
 
     mind_typing_flags : typing_flags; (** typing flags at the time of the inductive creation *)

kernel/declareops.ml

@@ -270,6 +270,8 @@ let subst_mind_body subst mib =
     mind_template = mib.mind_template;
     mind_variance = mib.mind_variance;
     mind_sec_variance = mib.mind_sec_variance;
+    mind_sort_variance = mib.mind_sort_variance;
+    mind_sec_sort_variance = mib.mind_sec_sort_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }

kernel/discharge.ml

@@ -187,6 +187,17 @@ let cook_inductive info mib =
       in
       Some (Array.append newvariance variance), Some sec_variance
   in
+  let mind_sort_variance, mind_sec_sort_variance =
+    match mib.mind_sort_variance, mib.mind_sec_sort_variance with
+    | None, None -> None, None
+    | None, Some _ | Some _, None -> assert false
+    | Some variance, Some sec_variance ->
+      let qlen = fst (AbstractContext.size (universe_context_of_cooking_info info)) in
+      let sec_variance, newvariance =
+        Array.chop (Array.length sec_variance - qlen) sec_variance
+      in
+      Some (Array.append newvariance variance), Some sec_variance
+  in
   let mind_template = match mib.mind_template with
   | None -> None
   | Some {template_param_arguments=levels; template_context; template_concl; template_defaults;} ->
@@ -206,6 +217,8 @@ let cook_inductive info mib =
     mind_template;
     mind_variance;
     mind_sec_variance;
+    mind_sort_variance;
+    mind_sec_sort_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }

kernel/entries.mli

@@ -65,6 +65,10 @@ type mutual_inductive_entry = {
   (* [None] if non-cumulative, otherwise associates each universe of
      the entry to [None] if to be inferred or [Some v] if to be
      checked. *)
+  mind_entry_sort_variance : variance_entry option;
+  (* [None] if no sort cumulativity, otherwise associates each quality
+     of the entry to [None] if to be inferred or [Some v] if to be
+     checked. *)
   mind_entry_private : bool option;
 }