Merge PR #11348: Discharge inductive types without rechecking them

Ack-by: maximedenes
Reviewed-by: ppedrot

15 files changed, 254 insertions, 142 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 261a3510d6..cebbfe4986 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -144,11 +144,11 @@ let abstract_context hyps =
   in
   Context.Named.fold_outside fold hyps ~init:([], [])
 
-let abstract_constant_type t (hyps, subst) =
+let abstract_as_type t (hyps, subst) =
   let t = Vars.subst_vars subst t in
   List.fold_left (fun c d -> mkProd_wo_LetIn d c) t hyps
 
-let abstract_constant_body c (hyps, subst) =
+let abstract_as_body c (hyps, subst) =
   let c = Vars.subst_vars subst c in
   it_mkLambda_or_LetIn c hyps
 
@@ -192,8 +192,7 @@ let discharge_abstract_universe_context subst abs_ctx auctx =
     let auctx = Univ.subst_univs_level_abstract_universe_context substf auctx in
     subst, (AUContext.union abs_ctx auctx)
 
-let lift_univs cb subst auctx0 =
-  match cb.const_universes with
+let lift_univs subst auctx0 = function
   | Monomorphic ctx ->
     assert (AUContext.is_empty auctx0);
     subst, (Monomorphic ctx)
@@ -219,7 +218,7 @@ let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) =
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps in
-  let c = abstract_constant_body (expmod c) hyps in
+  let c = abstract_as_body (expmod c) hyps in
   (c, priv)
 
 let cook_constr infos c =
@@ -230,11 +229,11 @@ let cook_constant { from = cb; info } =
   let { Opaqueproof.modlist; abstract } = info in
   let cache = RefTable.create 13 in
   let abstract, usubst, abs_ctx = abstract in
-  let usubst, univs = lift_univs cb usubst abs_ctx in
+  let usubst, univs = lift_univs usubst abs_ctx cb.const_universes in
   let expmod = expmod_constr_subst cache modlist usubst in
   let hyps0 = Context.Named.map expmod abstract in
   let hyps = abstract_context hyps0 in
-  let map c = abstract_constant_body (expmod c) hyps in
+  let map c = abstract_as_body (expmod c) hyps in
   let body = match cb.const_body with
   | Undef _ as x -> x
   | Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
@@ -243,7 +242,7 @@ let cook_constant { from = cb; info } =
   | Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
   in
   let const_hyps = Id.Set.diff (Context.Named.to_vars cb.const_hyps) (Context.Named.to_vars hyps0) in
-  let typ = abstract_constant_type (expmod cb.const_type) hyps in
+  let typ = abstract_as_type (expmod cb.const_type) hyps in
   {
     cook_body = body;
     cook_type = typ;
@@ -259,104 +258,160 @@ let cook_constant { from = cb; info } =
 (********************************)
 (* Discharging mutual inductive *)
 
-(* Replace
-
-     Var(y1)..Var(yq):C1..Cq |- Ij:Bj
-     Var(y1)..Var(yq):C1..Cq; I1..Ip:B1..Bp |- ci : Ti
-
-   by
-
-     |- Ij: (y1..yq:C1..Cq)Bj
-     I1..Ip:(B1 y1..yq)..(Bp y1..yq) |- ci : (y1..yq:C1..Cq)Ti[Ij:=(Ij y1..yq)]
-*)
-
-let it_mkNamedProd_wo_LetIn b d =
-  List.fold_left (fun c d -> mkNamedProd_wo_LetIn d c) b d
-
-let abstract_inductive decls nparamdecls inds =
-  let open Entries in
-  let ntyp = List.length inds in
-  let ndecls = Context.Named.length decls in
-  let args = Context.Named.to_instance mkVar (List.rev decls) in
-  let args = Array.of_list args in
-  let subs = List.init ntyp (fun k -> lift ndecls (mkApp(mkRel (k+1),args))) in
-  let inds' =
-    List.map
-      (function (tname,arity,template,cnames,lc) ->
-        let lc' = List.map (Vars.substl subs) lc in
-        let lc'' = List.map (fun b -> it_mkNamedProd_wo_LetIn b decls) lc' in
-        let arity' = it_mkNamedProd_wo_LetIn arity decls in
-        (tname,arity',template,cnames,lc''))
-        inds in
-  let nparamdecls' = nparamdecls + Array.length args in
-(* To be sure to be the same as before, should probably be moved to cook_inductive *)
-  let params' = let (_,arity,_,_,_) = List.hd inds' in
-                let (params,_) = decompose_prod_n_assum nparamdecls' arity in
-    params
+let template_level_of_var ~template_check d =
+  (* When [template_check], a universe from a section variable may not
+     be in the universes from the inductive (it must be pre-declared)
+     so always [None]. *)
+  if template_check then None
+  else
+    let c = Term.strip_prod_assum (RelDecl.get_type d) in
+    match kind c with
+    | Sort (Type u) -> Univ.Universe.level u
+    | _ -> None
+
+let it_mkProd_wo_LetIn = List.fold_left (fun c d -> mkProd_wo_LetIn d c)
+
+let abstract_rel_ctx (section_decls,subst) ctx =
+  (* Dealing with substitutions between contexts is too annoying, so
+     we reify [ctx] into a big [forall] term and work on that. *)
+  let t = it_mkProd_or_LetIn mkProp ctx in
+  let t = Vars.subst_vars subst t in
+  let t = it_mkProd_wo_LetIn t section_decls in
+  let ctx, t = decompose_prod_assum t in
+  assert (Constr.equal t mkProp);
+  ctx
+
+let abstract_lc ~ntypes expmod (newparams,subst) c =
+  let args = Array.rev_of_list (CList.map_filter (fun d ->
+      if RelDecl.is_local_def d then None
+      else match RelDecl.get_name d with
+        | Anonymous -> assert false
+        | Name id -> Some (mkVar id))
+      newparams)
   in
-  let ind'' =
-  List.map
-    (fun (a,arity,template,c,lc) ->
-      let _, short_arity = decompose_prod_n_assum nparamdecls' arity in
-      let shortlc =
-        List.map (fun c -> snd (decompose_prod_n_assum nparamdecls' c)) lc in
-      { mind_entry_typename = a;
-        mind_entry_arity = short_arity;
-        mind_entry_template = template;
-        mind_entry_consnames = c;
-        mind_entry_lc = shortlc })
-    inds'
-  in (params',ind'')
-
-let refresh_polymorphic_type_of_inductive (_,mip) =
-  match mip.mind_arity with
-  | RegularArity s -> s.mind_user_arity, false
-  | TemplateArity ar ->
-    let ctx = List.rev mip.mind_arity_ctxt in
-      mkArity (List.rev ctx, Sorts.sort_of_univ ar.template_level), true
+  let diff = List.length newparams in
+  let subs = List.init ntypes (fun k ->
+      lift diff (mkApp (mkRel (k+1), args)))
+  in
+  let c = Vars.substl subs c in
+  let c = Vars.subst_vars subst (expmod c) in
+  let c = it_mkProd_wo_LetIn c newparams in
+  c
+
+let abstract_projection ~params expmod hyps t =
+  let t = it_mkProd_or_LetIn t params in
+  let t = mkArrowR mkProp t in (* dummy type standing in for the inductive *)
+  let t = abstract_as_type (expmod t) hyps in
+  let _, t = decompose_prod_n_assum (List.length params + 1 + Context.Rel.nhyps (fst hyps)) t in
+  t
+
+let cook_one_ind ~template_check ~ntypes
+    (section_decls,_ as hyps) expmod mip =
+  let mind_arity = match mip.mind_arity with
+    | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
+      let arity = abstract_as_type (expmod arity) hyps in
+      let sort = destSort (expmod (mkSort sort)) in
+      RegularArity {mind_user_arity=arity; mind_sort=sort}
+    | TemplateArity {template_param_levels=levels;template_level} ->
+      let sec_levels = CList.map_filter (fun d ->
+          if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
+          else None)
+          section_decls
+      in
+      let levels = List.rev_append sec_levels levels in
+      TemplateArity {template_param_levels=levels;template_level}
+  in
+  let mind_arity_ctxt =
+    let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
+    abstract_rel_ctx hyps ctx
+  in
+  let mind_user_lc =
+    Array.map (abstract_lc ~ntypes expmod hyps)
+      mip.mind_user_lc
+  in
+  let mind_nf_lc = Array.map (fun (ctx,t) ->
+      let lc = it_mkProd_or_LetIn t ctx in
+      let lc = abstract_lc ~ntypes expmod hyps lc in
+      decompose_prod_assum lc)
+      mip.mind_nf_lc
+  in
+  { mind_typename = mip.mind_typename;
+    mind_arity_ctxt;
+    mind_arity;
+    mind_consnames = mip.mind_consnames;
+    mind_user_lc;
+    mind_nrealargs = mip.mind_nrealargs;
+    mind_nrealdecls = mip.mind_nrealdecls;
+    mind_kelim = mip.mind_kelim;
+    mind_nf_lc;
+    mind_consnrealargs = mip.mind_consnrealargs;
+    mind_consnrealdecls = mip.mind_consnrealdecls;
+    mind_recargs = mip.mind_recargs; (* TODO is this correct? checker should tell us. *)
+    mind_relevance = mip.mind_relevance;
+    mind_nb_constant = mip.mind_nb_constant;
+    mind_nb_args = mip.mind_nb_args;
+    mind_reloc_tbl = mip.mind_reloc_tbl;
+  }
 
 let cook_inductive { Opaqueproof.modlist; abstract } mib =
-  let open Entries in
   let (section_decls, subst, abs_uctx) = abstract in
-  let nparamdecls = Context.Rel.length mib.mind_params_ctxt in
-  let subst, ind_univs =
-    match mib.mind_universes with
-    | Monomorphic ctx -> Univ.empty_level_subst, Monomorphic_entry ctx
-    | Polymorphic auctx ->
-      let subst, auctx = discharge_abstract_universe_context subst abs_uctx auctx in
-      let subst = Univ.make_instance_subst subst in
-      let nas = Univ.AUContext.names auctx in
-      let auctx = Univ.AUContext.repr auctx in
-      subst, Polymorphic_entry (nas, auctx)
-  in
+  let subst, mind_universes = lift_univs subst abs_uctx mib.mind_universes in
   let cache = RefTable.create 13 in
-  let discharge c = Vars.subst_univs_level_constr subst (expmod_constr cache modlist c) in
-  let inds =
-    Array.map_to_list
-      (fun mip ->
-        let ty, template = refresh_polymorphic_type_of_inductive (mib,mip) in
-        let arity = discharge ty in
-        let lc = Array.map discharge mip.mind_user_lc  in
-          (mip.mind_typename,
-           arity, template,
-           Array.to_list mip.mind_consnames,
-           Array.to_list lc))
-      mib.mind_packets in
-  let section_decls' = Context.Named.map discharge section_decls in
-  let (params',inds') = abstract_inductive section_decls' nparamdecls inds in
-  let record = match mib.mind_record with
-    | PrimRecord info ->
-      Some (Some (Array.map (fun (x,_,_,_) -> x) info))
-    | FakeRecord -> Some None
-    | NotRecord -> None
+  let expmod = expmod_constr_subst cache modlist subst in
+  let section_decls = Context.Named.map expmod section_decls in
+  let removed_vars = Context.Named.to_vars section_decls in
+  let section_decls, _ as hyps = abstract_context section_decls in
+  let nnewparams = Context.Rel.nhyps section_decls in
+  let template_check = mib.mind_typing_flags.check_template in
+  let mind_params_ctxt =
+    let ctx = Context.Rel.map expmod mib.mind_params_ctxt in
+    abstract_rel_ctx hyps ctx
+  in
+  let ntypes = mib.mind_ntypes in
+  let mind_packets =
+    Array.map (cook_one_ind ~template_check ~ntypes hyps expmod)
+      mib.mind_packets
   in
-  { mind_entry_record = record;
-    mind_entry_finite = mib.mind_finite;
-    mind_entry_params = params';
-    mind_entry_inds = inds';
-    mind_entry_private = mib.mind_private;
-    mind_entry_cumulative = Option.has_some mib.mind_variance;
-    mind_entry_universes = ind_univs
+  let mind_record = match mib.mind_record with
+    | NotRecord -> NotRecord
+    | FakeRecord -> FakeRecord
+    | PrimRecord data ->
+      let data = Array.map (fun (id,projs,relevances,tys) ->
+          let tys = Array.map (abstract_projection ~params:mib.mind_params_ctxt expmod hyps) tys in
+          (id,projs,relevances,tys))
+          data
+      in
+      PrimRecord data
+  in
+  let mind_hyps =
+    List.filter (fun d -> not (Id.Set.mem (NamedDecl.get_id d) removed_vars))
+      mib.mind_hyps
+  in
+  let mind_variance, mind_sec_variance =
+    match mib.mind_variance, mib.mind_sec_variance with
+    | None, None -> None, None
+    | None, Some _ | Some _, None -> assert false
+    | Some variance, Some sec_variance ->
+      let sec_variance, newvariance =
+        Array.chop (Array.length sec_variance - AUContext.size abs_uctx)
+          sec_variance
+      in
+      Some (Array.append newvariance variance), Some sec_variance
+  in
+  {
+    mind_packets;
+    mind_record;
+    mind_finite = mib.mind_finite;
+    mind_ntypes = mib.mind_ntypes;
+    mind_hyps;
+    mind_nparams = mib.mind_nparams + nnewparams;
+    mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
+    mind_params_ctxt;
+    mind_universes;
+    mind_variance;
+    mind_sec_variance;
+    mind_private = mib.mind_private;
+    mind_typing_flags = mib.mind_typing_flags;
   }
 
 let expmod_constr modlist c = expmod_constr (RefTable.create 13) modlist c
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 83a8b9edfc..c2d47735ec 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -31,7 +31,7 @@ val cook_constr : Opaqueproof.cooking_info list ->
   (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
 
 val cook_inductive :
-  Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
+  Opaqueproof.cooking_info -> mutual_inductive_body -> mutual_inductive_body
 
 (** {6 Utility functions used in module [Discharge]. } *)
 
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9fd10b32e6..0b6e59bd5e 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -223,6 +223,11 @@ type mutual_inductive_body = {
 
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
+    mind_sec_variance : Univ.Variance.t array option;
+    (** Variance info for section polymorphic universes. [None]
+       outside sections. The final variance once all sections are
+       discharged is [mind_sec_variance ++ mind_variance]. *)
+
     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 *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 35185b6a5e..27e3f84464 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -248,6 +248,7 @@ let subst_mind_body sub mib =
     mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
     mind_variance = mib.mind_variance;
+    mind_sec_variance = mib.mind_sec_variance;
     mind_private = mib.mind_private;
     mind_typing_flags = mib.mind_typing_flags;
   }
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index b19472dc99..591cd050a5 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -276,7 +276,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
   let kelim = allowed_sorts univ_info in
   (arity,lc), (indices,splayed_lc), kelim
 
-let typecheck_inductive env (mie:mutual_inductive_entry) =
+let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   let () = match mie.mind_entry_inds with
   | [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
   | _ -> ()
@@ -335,8 +335,19 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
         data, Some None
   in
 
-  (* TODO pass only the needed bits *)
-  let variance = InferCumulativity.infer_inductive env mie in
+  let variance = if not mie.mind_entry_cumulative then None
+    else match mie.mind_entry_universes with
+      | Monomorphic_entry _ ->
+        CErrors.user_err Pp.(str "Inductive cannot be both monomorphic and universe cumulative.")
+      | Polymorphic_entry (_,uctx) ->
+        let univs = Instance.to_array @@ UContext.instance uctx in
+        let univs = match sec_univs with
+          | None -> univs
+          | Some sec_univs -> Array.append sec_univs univs
+        in
+        let variances = InferCumulativity.infer_inductive ~env_params univs mie.mind_entry_inds in
+        Some variances
+  in
 
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 5c04e860a2..8dea8f046d 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -17,6 +17,7 @@ open Declarations
     - environment with inductives + parameters in rel context
     - abstracted universes
     - checked variance info
+      (variance for section universes is at the beginning of the array)
     - record entry (checked to be OK)
     - parameters
     - for each inductive,
@@ -24,9 +25,11 @@ open Declarations
       * (indices * splayed constructor types) (both without params)
       * top allowed elimination
  *)
-val typecheck_inductive : env -> mutual_inductive_entry ->
-  env
-  * universes * Univ.Variance.t array option
+val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
+  -> mutual_inductive_entry
+  -> env
+  * universes
+  * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
   * ((inductive_arity * Constr.types array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 0d900c2ec9..3771454db5 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -466,7 +466,8 @@ let compute_projections (kn, i as ind) mib =
   Array.of_list (List.rev rs),
   Array.of_list (List.rev pbs)
 
-let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env ~sec_univs names prv univs variance
+    paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env paramsctxt inds in
@@ -517,6 +518,15 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
         mind_reloc_tbl = rtbl;
       } in
   let packets = Array.map3 build_one_packet names inds recargs in
+  let variance, sec_variance = match variance with
+    | None -> None, None
+    | Some variance -> match sec_univs with
+      | None -> Some variance, None
+      | Some sec_univs ->
+        let nsec = Array.length sec_univs in
+        Some (Array.sub variance nsec (Array.length variance - nsec)),
+        Some (Array.sub variance 0 nsec)
+  in
   let mib =
       (* Build the mutual inductive *)
     { mind_record = NotRecord;
@@ -529,6 +539,7 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
       mind_packets = packets;
       mind_universes = univs;
       mind_variance = variance;
+      mind_sec_variance = sec_variance;
       mind_private = prv;
       mind_typing_flags = Environ.typing_flags env;
     }
@@ -549,9 +560,11 @@ let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite
 (************************************************************************)
 (************************************************************************)
 
-let check_inductive env kn mie =
+let check_inductive env ~sec_univs kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+  let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+    IndTyping.typecheck_inductive env ~sec_univs mie
+  in
   (* Then check positivity conditions *)
   let chkpos = (Environ.typing_flags env).check_positive in
   let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -562,6 +575,6 @@ let check_inductive env kn mie =
       (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
   in
   (* Build the inductive packets *)
-    build_inductive env names mie.mind_entry_private univs variance
+    build_inductive env ~sec_univs names mie.mind_entry_private univs variance
       paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 240ba4e2bb..9b54e8b878 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -14,4 +14,5 @@ open Environ
 open Entries
 
 (** Check an inductive. *)
-val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
+val check_inductive : env -> sec_univs:Univ.Level.t array option
+  -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml
index 77abe6b410..211c909241 100644
--- a/kernel/inferCumulativity.ml
+++ b/kernel/inferCumulativity.ml
@@ -188,15 +188,12 @@ let infer_arity_constructor is_arity env variances arcn =
 
 open Entries
 
-let infer_inductive_core env params entries uctx =
-  let uarray = Instance.to_array @@ UContext.instance uctx in
-  if Array.is_empty uarray then raise TrivialVariance;
-  let env = Environ.push_context uctx env in
+let infer_inductive_core env univs entries =
+  if Array.is_empty univs then raise TrivialVariance;
   let variances =
     Array.fold_left (fun variances u -> LMap.add u IrrelevantI variances)
-      LMap.empty uarray
+      LMap.empty univs
   in
-  let env, _ = Typeops.check_context env params in
   let variances = List.fold_left (fun variances entry ->
       let variances = infer_arity_constructor true
           env variances entry.mind_entry_arity
@@ -210,17 +207,8 @@ let infer_inductive_core env params entries uctx =
       | exception Not_found -> Invariant
       | IrrelevantI -> Irrelevant
       | CovariantI -> Covariant)
-    uarray
-
-let infer_inductive env mie =
-  let open Entries in
-  let params = mie.mind_entry_params in
-  let entries = mie.mind_entry_inds in
-  if not mie.mind_entry_cumulative then None
-  else
-    let uctx = match mie.mind_entry_universes with
-      | Monomorphic_entry _ -> assert false
-      | Polymorphic_entry (_,uctx) -> uctx
-    in
-    try Some (infer_inductive_core env params entries uctx)
-    with TrivialVariance -> Some (Array.make (UContext.size uctx) Invariant)
+    univs
+
+let infer_inductive ~env_params univs entries =
+  try infer_inductive_core env_params univs entries
+  with TrivialVariance -> Array.make (Array.length univs) Invariant
diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli
index 2bddfe21e2..a8f593c7f9 100644
--- a/kernel/inferCumulativity.mli
+++ b/kernel/inferCumulativity.mli
@@ -8,5 +8,14 @@
 (*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
-val infer_inductive : Environ.env -> Entries.mutual_inductive_entry ->
-  Univ.Variance.t array option
+val infer_inductive
+  : env_params:Environ.env
+  (** Environment containing the polymorphic universes and the
+     parameters. *)
+  -> Univ.Level.t array
+  (** Universes whose cumulativity we want to infer. *)
+  -> Entries.one_inductive_entry list
+  (** The inductive block data we want to infer cumulativity for.
+      NB: we ignore the template bool and the names, only the terms
+      are used. *)
+  -> Univ.Variance.t array
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index ee101400d6..f6f2058c13 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -908,14 +908,19 @@ let check_mind mie lab =
     (* The label and the first inductive type name should match *)
     assert (Id.equal (Label.to_id lab) oie.mind_entry_typename)
 
+let add_checked_mind kn mib senv =
+  let mib =
+    match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
+  in
+  add_field (MutInd.label kn,SFBmind mib) (I kn) senv
+
 let add_mind l mie senv =
   let () = check_mind mie l in
   let kn = MutInd.make2 senv.modpath l in
-  let mib = Indtypes.check_inductive senv.env kn mie in
-  let mib =
-    match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
+  let sec_univs = Option.map Section.all_poly_univs  senv.sections
   in
-  kn, add_field (l,SFBmind mib) (I kn) senv
+  let mib = Indtypes.check_inductive senv.env ~sec_univs kn mie in
+  kn, add_checked_mind kn mib senv
 
 (** Insertion of module types *)
 
@@ -1014,9 +1019,8 @@ let close_section senv =
     add_constant_aux senv (kn, cb)
   | `Inductive (ind, mib) ->
     let info = cooking_info (Section.segment_of_inductive env0 ind sections0) in
-    let mie = Cooking.cook_inductive info mib in
-    let _, senv = add_mind (MutInd.label ind) mie senv in
-    senv
+    let mib = Cooking.cook_inductive info mib in
+    add_checked_mind ind mib senv
   in
   List.fold_left fold senv redo
 
diff --git a/kernel/section.ml b/kernel/section.ml
index 603ef5d006..6fa0543b23 100644
--- a/kernel/section.ml
+++ b/kernel/section.ml
@@ -28,6 +28,8 @@ type 'a t = {
   sec_mono_universes : ContextSet.t;
   sec_poly_universes : Name.t array * UContext.t;
   (** Universes local to the section *)
+  all_poly_univs : Univ.Level.t array;
+  (** All polymorphic universes, including from previous sections. *)
   has_poly_univs : bool;
   (** Are there polymorphic universes or constraints, including in previous sections. *)
   sec_entries : section_entry list;
@@ -41,6 +43,8 @@ let rec depth sec = 1 + match sec.sec_prev with None -> 0 | Some prev -> depth p
 
 let has_poly_univs sec = sec.has_poly_univs
 
+let all_poly_univs sec = sec.all_poly_univs
+
 let find_emap e (cmap, imap) = match e with
 | SecDefinition con -> Cmap.find con cmap
 | SecInductive ind -> Mindmap.find ind imap
@@ -57,7 +61,10 @@ let push_context (nas, ctx) sec =
   else
     let (snas, sctx) = sec.sec_poly_universes in
     let sec_poly_universes = (Array.append snas nas, UContext.union sctx ctx) in
-    { sec with sec_poly_universes; has_poly_univs = true }
+    let all_poly_univs =
+      Array.append sec.all_poly_univs (Instance.to_array @@ UContext.instance ctx)
+    in
+    { sec with sec_poly_universes; all_poly_univs; has_poly_univs = true }
 
 let rec is_polymorphic_univ u sec =
   let (_, uctx) = sec.sec_poly_universes in
@@ -81,6 +88,7 @@ let open_section ~custom sec_prev =
     sec_context = 0;
     sec_mono_universes = ContextSet.empty;
     sec_poly_universes = ([||], UContext.empty);
+    all_poly_univs = Option.cata (fun sec -> sec.all_poly_univs) [| |] sec_prev;
     has_poly_univs = Option.cata has_poly_univs false sec_prev;
     sec_entries = [];
     sec_data = (Cmap.empty, Mindmap.empty);
diff --git a/kernel/section.mli b/kernel/section.mli
index fbd3d8254e..37d0dab317 100644
--- a/kernel/section.mli
+++ b/kernel/section.mli
@@ -57,6 +57,14 @@ val push_inductive : poly:bool -> MutInd.t -> 'a t -> 'a t
 
 (** {6 Retrieving section data} *)
 
+val all_poly_univs : 'a t -> Univ.Level.t array
+(** Returns all polymorphic universes, including those from previous
+   sections. Earlier sections are earlier in the array.
+
+    NB: even if the array is empty there may be polymorphic
+   constraints about monomorphic universes, which prevent declaring
+   monomorphic globals. *)
+
 type abstr_info = private {
   abstr_ctx : Constr.named_context;
   (** Section variables of this prefix *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0029ff96d5..51440147ad 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -755,6 +755,10 @@ struct
     | Invariant, _ | _, Invariant -> Invariant
     | Covariant, Covariant -> Covariant
 
+  let equal a b = match a,b with
+    | Irrelevant, Irrelevant | Covariant, Covariant | Invariant, Invariant -> true
+    | (Irrelevant | Covariant | Invariant), _ -> false
+
   let check_subtype x y = match x, y with
   | (Irrelevant | Covariant | Invariant), Irrelevant -> true
   | Irrelevant, Covariant -> false
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ccb5c80cbf..1914ce5e34 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -263,6 +263,8 @@ sig
 
   val pr : t -> Pp.t
 
+  val equal : t -> t -> bool
+
 end
 
 (** {6 Universe instances} *)