Separate variance and universe fields in inductives.

I think the usage looks cleaner this way.

checker/checkInductive.ml

@@ -28,11 +28,8 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     | PrimRecord data -> Some (Some (Array.map pi1 data))
   in
   let mind_entry_universes = match mb.mind_universes with
-    | Monomorphic_ind univs -> Monomorphic_ind_entry univs
-    | Polymorphic_ind auctx -> Polymorphic_ind_entry (AUContext.names auctx, AUContext.repr auctx)
-    | Cumulative_ind auctx ->
-      Cumulative_ind_entry (AUContext.names (ACumulativityInfo.univ_context auctx),
-                            ACumulativityInfo.repr auctx)
+    | Monomorphic univs -> Monomorphic_entry univs
+    | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
   in
   let mind_entry_inds = Array.map_to_list (fun ind ->
       let mind_entry_arity, mind_entry_template = match ind.mind_arity with
@@ -64,6 +61,7 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
+    mind_entry_variance = mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }
 
@@ -135,7 +133,8 @@ let check_same_record r1 r2 = match r1, r2 with
 let check_inductive env mind mb =
   let entry = to_entry mb in
   let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
-        mind_nparams; mind_nparams_rec; mind_params_ctxt; mind_universes;
+        mind_nparams; mind_nparams_rec; mind_params_ctxt;
+        mind_universes; mind_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set the oracle for further typechecking *)
@@ -157,6 +156,7 @@ let check_inductive env mind mb =
 
   check "mind_params_ctxt" (Context.Rel.equal Constr.equal mb.mind_params_ctxt mind_params_ctxt);
   ignore mind_universes; (* Indtypes did the necessary checking *)
+  ignore mind_variance; (* Indtypes did the necessary checking *)
   ignore mind_private; (* passed through Indtypes *)
 
   ignore mind_typing_flags;

checker/mod_checking.ml

@@ -16,8 +16,8 @@ let check_constant_declaration env kn cb =
   (* [env'] contains De Bruijn universe variables *)
   let poly, env' =
     match cb.const_universes with
-    | Monomorphic_const ctx -> false, push_context_set ~strict:true ctx env
-    | Polymorphic_const auctx ->
+    | Monomorphic ctx -> false, push_context_set ~strict:true ctx env
+    | Polymorphic auctx ->
       let ctx = Univ.AUContext.repr auctx in
       let env = push_context ~strict:false ctx env in
       true, env

checker/values.ml

@@ -112,7 +112,6 @@ let v_variance = v_enum "variance" 3
 
 let v_instance = Annot ("instance", Array v_level)
 let v_abs_context = v_tuple "abstract_universe_context" [|Array v_name; v_cstrs|]
-let v_abs_cum_info = v_tuple "cumulativity_info" [|v_abs_context; Array v_variance|]
 let v_context_set = v_tuple "universe_context_set" [|v_hset v_level;v_cstrs|]
 
 (** kernel/term *)
@@ -226,14 +225,14 @@ let v_cst_def =
 let v_typing_flags =
   v_tuple "typing_flags" [|v_bool; v_bool; v_oracle; v_bool; v_bool; v_bool; v_bool|]
 
-let v_const_univs = v_sum "constant_universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
+let v_univs = v_sum "universes" 0 [|[|v_context_set|]; [|v_abs_context|]|]
 
 let v_cb = v_tuple "constant_body"
   [|v_section_ctxt;
     v_cst_def;
     v_constr;
     Any;
-    v_const_univs;
+    v_univs;
     Opt v_context_set;
     v_bool;
     v_typing_flags|]
@@ -276,10 +275,6 @@ let v_record_info =
   v_sum "record_info" 2
     [| [| Array (v_tuple "record" [| v_id; Array v_id; Array v_constr |]) |] |]
 
-let v_ind_pack_univs = 
-  v_sum "abstract_inductive_universes" 0
-    [|[|v_context_set|]; [|v_abs_context|]; [|v_abs_cum_info|]|]
-
 let v_ind_pack = v_tuple "mutual_inductive_body"
   [|Array v_one_ind;
     v_record_info;
@@ -289,7 +284,8 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     Int;
     v_rctxt;
-    v_ind_pack_univs; (* universes *)
+    v_univs; (* universes *)
+    Opt (Array v_variance);
     Opt v_bool;
     v_typing_flags|]
 

dev/ci/user-overlays/09439-sep-variance.sh

@@ -0,0 +1,14 @@
+
+if [ "$CI_PULL_REQUEST" = "9439" ] || [ "$CI_BRANCH" = "sep-variance" ]; then
+    elpi_CI_REF=sep-variance
+    elpi_CI_GITURL=https://github.com/SkySkimmer/coq-elpi
+
+    equations_CI_REF=sep-variance
+    equations_CI_GITURL=https://github.com/SkySkimmer/Coq-Equations
+
+    mtac2_CI_REF=sep-variance
+    mtac2_CI_GITURL=https://github.com/SkySkimmer/mtac2
+
+    paramcoq_CI_REF=sep-variance
+    paramcoq_CI_GITURL=https://github.com/SkySkimmer/paramcoq
+fi

dev/include

@@ -41,8 +41,6 @@
 #install_printer  (* univ context *) ppuniverse_context;;
 #install_printer  (* univ context future *) ppuniverse_context_future;;
 #install_printer  (* univ context set *) ppuniverse_context_set;;
-#install_printer  (* cumulativity info *) ppcumulativity_info;;
-#install_printer  (* abstract cumulativity info *) ppabstract_cumulativity_info;;
 #install_printer  (* univ set *) ppuniverse_set;;
 #install_printer  (* univ instance *) ppuniverse_instance;;
 #install_printer  (* univ subst *) ppuniverse_subst;;

dev/top_printers.ml

@@ -222,8 +222,6 @@ let ppuniverseconstraints c = pp (UnivProblem.Set.pr c)
 let ppuniverse_context_future c = 
   let ctx = Future.force c in
     ppuniverse_context ctx
-let ppcumulativity_info c = pp (Univ.pr_cumulativity_info Univ.Level.pr c)
-let ppabstract_cumulativity_info c = pp (Univ.pr_abstract_cumulativity_info Univ.Level.pr c)
 let ppuniverses u = pp (UGraph.pr_universes Level.pr u)
 let ppnamedcontextval e =
   let env = Global.env () in

dev/top_printers.mli

@@ -145,8 +145,6 @@ val ppevar_universe_context : UState.t -> unit
 val ppconstraints : Univ.Constraint.t -> unit
 val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : Univ.UContext.t Future.computation -> unit
-val ppcumulativity_info : Univ.CumulativityInfo.t -> unit
-val ppabstract_cumulativity_info : Univ.ACumulativityInfo.t -> unit
 val ppuniverses : UGraph.t -> unit
 
 val ppnamedcontextval : Environ.named_context_val -> unit

engine/eConstr.ml

@@ -405,25 +405,17 @@ let compare_cumulative_instances cv_pb nargs_ok variances u u' cstrs =
 
 let cmp_inductives cv_pb (mind,ind as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
-    cstrs
-  | Declarations.Polymorphic_ind _ ->
-     enforce_eq_instances_univs false u1 u2 cstrs
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> enforce_eq_instances_univs false u1 u2 cstrs
+  | Some variances ->
     let num_param_arity = Reduction.inductive_cumulativity_arguments spec in
-    let variances = Univ.ACumulativityInfo.variance cumi in
     compare_cumulative_instances cv_pb (Int.equal num_param_arity nargs) variances u1 u2 cstrs
 
 let cmp_constructors (mind, ind, cns as spec) nargs u1 u2 cstrs =
   let open UnivProblem in
-  match mind.Declarations.mind_universes with
-  | Declarations.Monomorphic_ind _ ->
-    cstrs
-  | Declarations.Polymorphic_ind _ ->
-    enforce_eq_instances_univs false u1 u2 cstrs
-  | Declarations.Cumulative_ind cumi ->
+  match mind.Declarations.mind_variance with
+  | None -> enforce_eq_instances_univs false u1 u2 cstrs
+  | Some _ ->
     let num_cnstr_args = Reduction.constructor_cumulativity_arguments spec in
     if not (Int.equal num_cnstr_args nargs)
     then enforce_eq_instances_univs false u1 u2 cstrs

engine/evd.ml

@@ -852,8 +852,9 @@ let universe_context_set d = UState.context_set d.universes
 
 let to_universe_context evd = UState.context evd.universes
 
-let const_univ_entry ~poly evd = UState.const_univ_entry ~poly evd.universes
-let ind_univ_entry ~poly evd = UState.ind_univ_entry ~poly evd.universes
+let univ_entry ~poly evd = UState.univ_entry ~poly evd.universes
+
+let const_univ_entry = univ_entry
 
 let check_univ_decl ~poly evd decl = UState.check_univ_decl ~poly evd.universes decl
 

engine/evd.mli

@@ -597,12 +597,12 @@ val universes : evar_map -> UGraph.t
     [Univ.ContextSet.to_context]. *)
 val to_universe_context : evar_map -> Univ.UContext.t
 
-val const_univ_entry : poly:bool -> evar_map -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> evar_map -> Entries.universes_entry
 
-(** NB: [ind_univ_entry] cannot create cumulative entries. *)
-val ind_univ_entry : poly:bool -> evar_map -> Entries.inductive_universes
+val const_univ_entry : poly:bool -> evar_map -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
 
-val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> evar_map -> UState.universe_decl -> Entries.universes_entry
 
 val merge_universe_context : evar_map -> UState.t -> evar_map
 val set_universe_context : evar_map -> UState.t -> evar_map

engine/uState.ml

@@ -100,24 +100,16 @@ let constraints ctx = snd ctx.uctx_local
 
 let context ctx = ContextSet.to_context ctx.uctx_local
 
-let const_univ_entry ~poly uctx =
+let univ_entry ~poly uctx =
   let open Entries in
   if poly then
     let (binders, _) = uctx.uctx_names in
     let uctx = context uctx in
     let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-    Polymorphic_const_entry (nas, uctx)
-  else Monomorphic_const_entry (context_set uctx)
+    Polymorphic_entry (nas, uctx)
+  else Monomorphic_entry (context_set uctx)
 
-(* does not support cumulativity since you need more info *)
-let ind_univ_entry ~poly uctx =
-  let open Entries in
-  if poly then
-    let (binders, _) = uctx.uctx_names in
-    let uctx = context uctx in
-    let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-    Polymorphic_ind_entry (nas, uctx)
-  else Monomorphic_ind_entry (context_set uctx)
+let const_univ_entry = univ_entry
 
 let of_context_set ctx = { empty with uctx_local = ctx }
 
@@ -422,10 +414,10 @@ let check_univ_decl ~poly uctx decl =
       let (binders, _) = uctx.uctx_names in
       let uctx = universe_context ~names ~extensible uctx in
       let nas = UnivNames.compute_instance_binders (UContext.instance uctx) binders in
-      Entries.Polymorphic_const_entry (nas, uctx)
+      Entries.Polymorphic_entry (nas, uctx)
     else
       let () = check_universe_context_set ~names ~extensible uctx in
-      Entries.Monomorphic_const_entry uctx.uctx_local
+      Entries.Monomorphic_entry uctx.uctx_local
   in
   if not decl.univdecl_extensible_constraints then
     check_implication uctx
@@ -458,8 +450,8 @@ let restrict ctx vars =
 let demote_seff_univs entry uctx =
   let open Entries in
   match entry.const_entry_universes with
-  | Polymorphic_const_entry _ -> uctx
-  | Monomorphic_const_entry (univs, _) ->
+  | Polymorphic_entry _ -> uctx
+  | Monomorphic_entry (univs, _) ->
     let seff = LSet.union uctx.uctx_seff_univs univs in
     { uctx with uctx_seff_univs = seff }
 

engine/uState.mli

@@ -64,12 +64,11 @@ val constraints : t -> Univ.Constraint.t
 val context : t -> Univ.UContext.t
 (** Shorthand for {!context_set} with {!Context_set.to_context}. *)
 
-val const_univ_entry : poly:bool -> t -> Entries.constant_universes_entry
+val univ_entry : poly:bool -> t -> Entries.universes_entry
 (** Pick from {!context} or {!context_set} based on [poly]. *)
 
-val ind_univ_entry : poly:bool -> t -> Entries.inductive_universes
-(** Pick from {!context} or {!context_set} based on [poly].
-    Cannot create cumulative entries. *)
+val const_univ_entry : poly:bool -> t -> Entries.universes_entry
+[@@ocaml.deprecated "Use [univ_entry]."]
 
 (** {5 Constraints handling} *)
 
@@ -177,7 +176,7 @@ val default_univ_decl : universe_decl
    When polymorphic, the universes corresponding to
    [decl.univdecl_instance] come first in the order defined by that
    list. *)
-val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.constant_universes_entry
+val check_univ_decl : poly:bool -> t -> universe_decl -> Entries.universes_entry
 
 val check_mono_univ_decl : t -> universe_decl -> Univ.ContextSet.t
 

interp/declare.ml

@@ -143,7 +143,7 @@ let declare_constant_common id cst =
   update_tables c;
   c
 
-let default_univ_entry = Monomorphic_const_entry Univ.ContextSet.empty
+let default_univ_entry = Monomorphic_entry Univ.ContextSet.empty
 let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
     ?(univs=default_univ_entry) ?(eff=Safe_typing.empty_private_constants) body =
   { const_entry_body = Future.from_val ?fix_exn ((body,Univ.ContextSet.empty), eff);
@@ -156,8 +156,8 @@ let definition_entry ?fix_exn ?(opaque=false) ?(inline=false) ?types
 
 let declare_constant ?(internal = UserIndividualRequest) ?(local = false) id ?(export_seff=false) (cd, kind) =
   let is_poly de = match de.const_entry_universes with
-  | Monomorphic_const_entry _ -> false
-  | Polymorphic_const_entry _ -> true
+  | Monomorphic_entry _ -> false
+  | Polymorphic_entry _ -> true
   in
   let in_section = Lib.sections_are_opened () in
   let export, decl = (* We deal with side effects *)
@@ -217,8 +217,8 @@ let cache_variable ((sp,_),o) =
          section-local definition, but it's not enforced by typing *)
       let (body, uctx), () = Future.force de.const_entry_body in
       let poly, univs = match de.const_entry_universes with
-      | Monomorphic_const_entry uctx -> false, uctx
-      | Polymorphic_const_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
+      | Monomorphic_entry uctx -> false, uctx
+      | Polymorphic_entry (_, uctx) -> true, Univ.ContextSet.of_context uctx
       in
       let univs = Univ.ContextSet.union uctx univs in
       (* We must declare the universe constraints before type-checking the
@@ -328,21 +328,15 @@ let dummy_inductive_entry m = {
   mind_entry_record = None;
   mind_entry_finite = Declarations.BiFinite;
   mind_entry_inds = List.map dummy_one_inductive_entry m.mind_entry_inds;
-  mind_entry_universes = Monomorphic_ind_entry Univ.ContextSet.empty;
+  mind_entry_universes = default_univ_entry;
+  mind_entry_variance = None;
   mind_entry_private = None;
 }
 
 (* reinfer subtyping constraints for inductive after section is dischared. *)
-let infer_inductive_subtyping mind_ent =
-  match mind_ent.mind_entry_universes with
-  | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ ->
-    mind_ent
-  | Cumulative_ind_entry (_, cumi) ->
-    begin
-      let env = Global.env () in
-      (* let (env'', typed_params) = Typeops.infer_local_decls env' (mind_ent.mind_entry_params) in *)
-        InferCumulativity.infer_inductive env mind_ent
-    end
+let rebuild_inductive mind_ent =
+  let env = Global.env () in
+  InferCumulativity.infer_inductive env mind_ent
 
 let inInductive : mutual_inductive_entry -> obj =
   declare_object {(default_object "INDUCTIVE") with
@@ -352,25 +346,19 @@ let inInductive : mutual_inductive_entry -> obj =
     classify_function = (fun a -> Substitute (dummy_inductive_entry a));
     subst_function = ident_subst_function;
     discharge_function = discharge_inductive;
-    rebuild_function = infer_inductive_subtyping }
+    rebuild_function = rebuild_inductive }
 
 let declare_one_projection univs (mind,_ as ind) ~proj_npars proj_arg label (term,types) =
   let id = Label.to_id label in
-  let univs = match univs with
-    | Monomorphic_ind_entry _ ->
+  let univs, u = match univs with
+    | Monomorphic_entry _ ->
       (* Global constraints already defined through the inductive *)
-      Monomorphic_const_entry Univ.ContextSet.empty
-    | Polymorphic_ind_entry (nas, ctx) ->
-      Polymorphic_const_entry (nas, ctx)
-    | Cumulative_ind_entry (nas, ctx) ->
-      Polymorphic_const_entry (nas, Univ.CumulativityInfo.univ_context ctx)
-  in
-  let term, types = match univs with
-    | Monomorphic_const_entry _ -> term, types
-    | Polymorphic_const_entry (_, ctx) ->
-      let u = Univ.UContext.instance ctx in
-      Vars.subst_instance_constr u term, Vars.subst_instance_constr u types
+      default_univ_entry, Univ.Instance.empty
+    | Polymorphic_entry (nas, ctx) ->
+      Polymorphic_entry (nas, ctx), Univ.UContext.instance ctx
   in
+  let term = Vars.subst_instance_constr u term in
+  let types = Vars.subst_instance_constr u types in
   let entry = definition_entry ~types ~univs term in
   let cst = declare_constant id (DefinitionEntry entry, IsDefinition StructureComponent) in
   let p = Projection.Repr.make ind ~proj_npars ~proj_arg label in

interp/declare.mli

@@ -43,7 +43,7 @@ type internal_flag =
 (* Defaut definition entries, transparent with no secctx or proj information *)
 val definition_entry : ?fix_exn:Future.fix_exn ->
   ?opaque:bool -> ?inline:bool -> ?types:types ->
-  ?univs:Entries.constant_universes_entry ->
+  ?univs:Entries.universes_entry ->
   ?eff:Safe_typing.private_constants -> constr -> Safe_typing.private_constants definition_entry
 
 (** [declare_constant id cd] declares a global declaration
@@ -58,7 +58,7 @@ val declare_constant :
 val declare_definition : 
   ?internal:internal_flag -> ?opaque:bool -> ?kind:definition_object_kind ->
   ?local:bool -> Id.t -> ?types:constr ->
-  constr Entries.in_constant_universes_entry -> Constant.t
+  constr Entries.in_universes_entry -> Constant.t
 
 (** Since transparent constants' side effects are globally declared, we
  *  need that *)