Merge PR #11546: Remove the Template Check option.

Reviewed-by: SkySkimmer
Ack-by: Zimmi48

7 files changed, 10 insertions, 50 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index f1eb000c88..31dd26d2ba 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -258,17 +258,6 @@ let cook_constant { from = cb; info } =
 (********************************)
 (* Discharging mutual inductive *)
 
-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 =
@@ -305,7 +294,7 @@ let abstract_projection ~params expmod hyps t =
   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
+let cook_one_ind ~ntypes
     (section_decls,_ as hyps) expmod mip =
   let mind_arity = match mip.mind_arity with
     | RegularArity {mind_user_arity=arity;mind_sort=sort} ->
@@ -314,7 +303,7 @@ let cook_one_ind ~template_check ~ntypes
       RegularArity {mind_user_arity=arity; mind_sort=sort}
     | 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)
+          if RelDecl.is_local_assum d then Some None
           else None)
           section_decls
       in
@@ -362,14 +351,13 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
   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)
+    Array.map (cook_one_ind ~ntypes hyps expmod)
       mib.mind_packets
   in
   let mind_record = match mib.mind_record with
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c550b0d432..ac130d018d 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -89,10 +89,6 @@ type typing_flags = {
   indices_matter: bool;
   (** The universe of an inductive type must be above that of its indices. *)
 
-  check_template : bool;
-  (* If [false] then we don't check that the universes template-polymorphic
-     inductive parameterize on are necessarily local and unbounded from below.
-     This potentially introduces inconsistencies. *)
 }
 
 (* some contraints are in constant_constraints, some other may be in
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 047027984d..a3adac7a11 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,7 +26,6 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
-  check_template = true;
 }
 
 (** {6 Arities } *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index f04863386f..87f2f234da 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -275,7 +275,6 @@ let type_in_type env = not (typing_flags env).check_universes
 let deactivated_guard env = not (typing_flags env).check_guarded
 
 let indices_matter env = env.env_typing_flags.indices_matter
-let check_template env = env.env_typing_flags.check_template
 
 let universes env = env.env_stratification.env_universes
 let universes_lbound env = env.env_stratification.env_universes_lbound
@@ -449,7 +448,6 @@ let same_flags {
      share_reduction;
      enable_VM;
      enable_native_compiler;
-     check_template;
   } alt =
   check_guarded == alt.check_guarded &&
   check_positive == alt.check_positive &&
@@ -458,8 +456,7 @@ let same_flags {
   indices_matter == alt.indices_matter &&
   share_reduction == alt.share_reduction &&
   enable_VM == alt.enable_VM &&
-  enable_native_compiler == alt.enable_native_compiler &&
-  check_template == alt.check_template
+  enable_native_compiler == alt.enable_native_compiler
 [@warning "+9"]
 
 let set_typing_flags c env = (* Unsafe *)
@@ -591,9 +588,6 @@ let polymorphic_pind (ind,u) env =
 let type_in_type_ind (mind,_i) env =
   not (lookup_mind mind env).mind_typing_flags.check_universes
 
-let template_checked_ind (mind,_i) env =
-  (lookup_mind mind env).mind_typing_flags.check_template
-
 let template_polymorphic_ind (mind,i) env =
   match (lookup_mind mind env).mind_packets.(i).mind_arity with
   | TemplateArity _ -> true
@@ -802,14 +796,6 @@ let get_template_polymorphic_variables env r =
   | IndRef ind -> template_polymorphic_variables ind env
   | ConstructRef cstr -> template_polymorphic_variables (inductive_of_constructor cstr) env
 
-let is_template_checked env r =
-  let open Names.GlobRef in
-  match r with
-  | VarRef _id -> false
-  | ConstRef _c -> false
-  | IndRef ind -> template_checked_ind ind env
-  | ConstructRef cstr -> template_checked_ind (inductive_of_constructor cstr) env
-
 let is_type_in_type env r =
   let open Names.GlobRef in
   match r with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index bd5a000c2b..e80d0a9b9f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -112,7 +112,6 @@ val is_impredicative_set : env -> bool
 val type_in_type : env -> bool
 val deactivated_guard : env -> bool
 val indices_matter : env -> bool
-val check_template : env -> bool
 
 val is_impredicative_sort : env -> Sorts.t -> bool
 val is_impredicative_univ : env -> Univ.Universe.t -> bool
@@ -274,7 +273,6 @@ val type_in_type_ind : inductive -> env -> bool
 val template_polymorphic_ind : inductive -> env -> bool
 val template_polymorphic_variables : inductive -> env -> Univ.Level.t list
 val template_polymorphic_pind : pinductive -> env -> bool
-val template_checked_ind : inductive -> env -> bool
 
 (** {5 Modules } *)
 
@@ -373,7 +371,6 @@ val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declarat
 val is_polymorphic : env -> Names.GlobRef.t -> bool
 val is_template_polymorphic : env -> GlobRef.t -> bool
 val get_template_polymorphic_variables : env -> GlobRef.t -> Univ.Level.t list
-val is_template_checked : env -> GlobRef.t -> bool
 val is_type_in_type : env -> GlobRef.t -> bool
 
 (** Native compiler *)
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 113ee787f2..cc15109f06 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -197,7 +197,7 @@ let unbounded_from_below u cstrs =
    (starting from the most recent and ignoring let-definitions) is not
    contributing to the inductive type's sort or is Some u_k if its level
    is u_k and is contributing. *)
-let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt concl =
+let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
   let check_level l =
     Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
     unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
@@ -205,27 +205,23 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
   in
   let univs = Univ.Universe.levels concl in
   let univs =
-    if template_check then
-      Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
-    else univs (* Doesn't check the universes can be generalized *)
+    Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
   in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
         | Sort (Type u) ->
-          if template_check then
             (match Univ.Universe.level u with
              | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None
              | None -> None)
-          else Univ.Universe.level u
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
   let params = List.fold_left fold [] paramsctxt in
   params, univs
 
-let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
   if not (Universe.Set.is_empty univ_info.missing)
   then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
   let arity = Vars.subst_univs_level_constr usubst arity in
@@ -267,9 +263,9 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
           splayed_lc
       in
       let param_levels, concl_levels =
-        template_polymorphic_univs ~template_check ~ctor_levels ctx params min_univ
+        template_polymorphic_univs ~ctor_levels ctx params min_univ
       in
-      if template_check && List.for_all (fun x -> Option.is_empty x) param_levels
+      if List.for_all (fun x -> Option.is_empty x) param_levels
          && Univ.LSet.is_empty concl_levels then
         CErrors.user_err
           Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
@@ -356,8 +352,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   (* Abstract universes *)
   let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
   let params = Vars.subst_univs_level_context usubst params in
-  let template_check = Environ.check_template env in
-  let data = List.map (abstract_packets ~template_check univs usubst params) data in
+  let data = List.map (abstract_packets univs usubst params) data in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8dea8f046d..723ba5459e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -40,7 +40,6 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
 (* Utility function to compute the actual universe parameters
    of a template polymorphic inductive *)
 val template_polymorphic_univs :
-  template_check:bool ->
   ctor_levels:Univ.LSet.t ->
   Univ.ContextSet.t ->
   Constr.rel_context ->