Ensure that template parameters are shared in the same inductive block.

This could have been at the root of strange behaviours (read unsoundness).

1 files changed, 14 insertions, 19 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index b93b03ec16..c4c6d9bb4f 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 mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
+let to_entry (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
@@ -33,20 +33,9 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
         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
+      let univs = match mb.mind_template with
       | None -> ContextSet.empty
-      | Some ctx -> ctx
+      | Some ctx -> ctx.template_context
       in
       Monomorphic_entry univs
     | Polymorphic auctx -> Polymorphic_entry (AUContext.names auctx, AUContext.repr auctx)
@@ -95,13 +84,18 @@ 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;template_context} ->
-    List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
-    ContextSet.equal template_context ar.template_context &&
+  | TemplateArity ar, TemplateArity {template_level} ->
     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
 
+let check_template ar1 ar2 = match ar1, ar2 with
+| None, None -> true
+| Some ar, Some {template_context; template_param_levels} ->
+  List.equal (Option.equal Univ.Level.equal) ar.template_param_levels template_param_levels &&
+  ContextSet.equal template_context ar.template_context
+| None, Some _ | Some _, None -> false
+
 let check_kelim k1 k2 = Sorts.family_leq k1 k2
 
 (* Use [eq_ind_chk] because when we rebuild the recargs we have lost
@@ -163,10 +157,10 @@ let check_same_record r1 r2 = match r1, r2 with
   | (NotRecord | FakeRecord | PrimRecord _), _ -> false
 
 let check_inductive env mind mb =
-  let entry = to_entry mind mb in
+  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_variance; mind_sec_variance;
+        mind_universes; mind_template; mind_variance; mind_sec_variance;
         mind_private; mind_typing_flags; }
     =
     (* Locally set typing flags for further typechecking *)
@@ -197,6 +191,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 *)
+  check "mind_template" (check_template mb.mind_template mind_template);
   check "mind_variance" (Option.equal (Array.equal Univ.Variance.equal)
                            mb.mind_variance mind_variance);
   check "mind_sec_variance" (Option.is_empty mind_sec_variance);