Merge PR #11528: Checker does not rely on Monomorphic fields

Reviewed-by: SkySkimmer

6 files changed, 32 insertions, 9 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index a2cf44389e..051f51bbb3 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -20,7 +20,7 @@ exception InductiveMismatch of MutInd.t * string
 
 let check mind field b = if not b then raise (InductiveMismatch (mind,field))
 
-let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
+let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
   let open Entries in
   let nparams = List.length mb.mind_params_ctxt in (* include letins *)
   let mind_entry_record = match mb.mind_record with
@@ -28,7 +28,27 @@ let to_entry (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
     | PrimRecord data -> Some (Some (Array.map (fun (x,_,_,_) -> x) data))
   in
   let mind_entry_universes = match mb.mind_universes with
-    | Monomorphic univs -> Monomorphic_entry univs
+    | Monomorphic _ ->
+      (* We only need to rebuild the set of constraints for template polymorphic
+        inductive types. The set of monomorphic constraints is already part of
+        the graph at that point, but we need to emulate a broken bound variable
+        mechanism for template inductive types. *)
+      let fold accu ind = match ind.mind_arity with
+      | RegularArity _ -> accu
+      | TemplateArity ar ->
+        match accu with
+        | None -> Some ar.template_context
+        | Some ctx ->
+          (* Ensure that all template contexts agree. This is enforced by the
+             kernel. *)
+          let () = check mind "mind_arity" (ContextSet.equal ctx ar.template_context) in
+          Some ctx
+      in
+      let univs = match Array.fold_left fold None mb.mind_packets with
+      | None -> ContextSet.empty
+      | Some ctx -> ctx
+      in
+      Monomorphic_entry univs
     | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
   in
   let mind_entry_inds = Array.map_to_list (fun ind ->
@@ -69,8 +89,9 @@ let check_arity env ar1 ar2 = match ar1, ar2 with
   | RegularArity ar, RegularArity {mind_user_arity;mind_sort} ->
     Constr.equal ar.mind_user_arity mind_user_arity &&
     Sorts.equal ar.mind_sort mind_sort
-  | TemplateArity ar, TemplateArity {template_param_levels;template_level} ->
+  | TemplateArity ar, TemplateArity {template_param_levels;template_level;template_context} ->
     List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
+    ContextSet.equal template_context ar.template_context &&
     UGraph.check_leq (universes env) template_level ar.template_level
     (* template_level is inferred by indtypes, so functor application can produce a smaller one *)
   | (RegularArity _ | TemplateArity _), _ -> assert false
@@ -136,7 +157,7 @@ let check_same_record r1 r2 = match r1, r2 with
   | (NotRecord | FakeRecord | PrimRecord _), _ -> false
 
 let check_inductive env mind mb =
-  let entry = to_entry mb in
+  let entry = to_entry mind mb in
   let { mind_packets; mind_record; mind_finite; mind_ntypes; mind_hyps;
         mind_nparams; mind_nparams_rec; mind_params_ctxt;
         mind_universes; mind_variance; mind_sec_variance;
diff --git a/checker/values.ml b/checker/values.ml
index fff166f27b..c8bbc092b4 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -228,7 +228,7 @@ let v_oracle =
   |]
 
 let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ|]
+  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|]
 
 let v_primitive =
   v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cebbfe4986..f1eb000c88 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -312,14 +312,14 @@ let cook_one_ind ~template_check ~ntypes
       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} ->
+    | TemplateArity {template_param_levels=levels;template_level;template_context} ->
       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}
+      TemplateArity {template_param_levels=levels;template_level;template_context}
   in
   let mind_arity_ctxt =
     let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0b6e59bd5e..c550b0d432 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -32,6 +32,7 @@ type engagement = set_predicativity
 type template_arity = {
   template_param_levels : Univ.Level.t option list;
   template_level : Univ.Universe.t;
+  template_context : Univ.ContextSet.t;
 }
 
 type ('a, 'b) declaration_arity =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 27e3f84464..047027984d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,7 +49,8 @@ let map_decl_arity f g = function
 let hcons_template_arity ar =
   { template_param_levels = ar.template_param_levels;
       (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
-    template_level = Univ.hcons_univ ar.template_level }
+    template_level = Univ.hcons_univ ar.template_level;
+    template_context = Univ.hcons_universe_context_set ar.template_context }
 
 let universes_context = function
   | Monomorphic _ -> Univ.AUContext.empty
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 719eb276df..113ee787f2 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -274,7 +274,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
         CErrors.user_err
           Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
       else
-        TemplateArity {template_param_levels = param_levels; template_level = min_univ}
+        TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
   in
 
   let kelim = allowed_sorts univ_info in