Merge PR #11764: Simplify mutual template polymorphism

Reviewed-by: SkySkimmer

18 files changed, 204 insertions, 124 deletions

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 62e732ce69..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,39 +33,27 @@ 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)
   in
   let mind_entry_inds = Array.map_to_list (fun ind ->
-      let mind_entry_arity, mind_entry_template = match ind.mind_arity with
+      let mind_entry_arity = match ind.mind_arity with
         | RegularArity ar ->
           let ctx, arity = Term.decompose_prod_n_assum nparams ar.mind_user_arity in
           ignore ctx; (* we will check that the produced user_arity is equal to the input *)
-          arity, false
+          arity
         | TemplateArity ar ->
           let ctx = ind.mind_arity_ctxt in
           let ctx = List.firstn (List.length ctx - nparams) ctx in
-          Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level), true
+          Term.mkArity (ctx, Sorts.sort_of_univ ar.template_level)
       in
       {
         mind_entry_typename = ind.mind_typename;
         mind_entry_arity;
-        mind_entry_template;
         mind_entry_consnames = Array.to_list ind.mind_consnames;
         mind_entry_lc = Array.map_to_list (fun c ->
             let ctx, c = Term.decompose_prod_n_assum nparams c in
@@ -75,12 +63,19 @@ let to_entry mind (mb:mutual_inductive_body) : Entries.mutual_inductive_entry =
       })
       mb.mind_packets
   in
+  let check_template ind = match ind.mind_arity with
+  | RegularArity _ -> false
+  | TemplateArity _ -> true
+  in
+  let mind_entry_template = Array.exists check_template mb.mind_packets in
+  let () = if mind_entry_template then assert (Array.for_all check_template mb.mind_packets) in
   {
     mind_entry_record;
     mind_entry_finite = mb.mind_finite;
     mind_entry_params = mb.mind_params_ctxt;
     mind_entry_inds;
     mind_entry_universes;
+    mind_entry_template;
     mind_entry_cumulative= Option.has_some mb.mind_variance;
     mind_entry_private = mb.mind_private;
   }
@@ -89,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
@@ -157,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 *)
@@ -191,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);
diff --git a/checker/checkTypes.mli b/checker/checkTypes.mli
index ac9ea2fb31..9ef6ff017c 100644
--- a/checker/checkTypes.mli
+++ b/checker/checkTypes.mli
@@ -17,4 +17,4 @@ open Environ
 (*s Typing functions (not yet tagged as safe) *)
 
 val check_polymorphic_arity :
-  env -> rel_context -> template_arity -> unit
+  env -> rel_context -> template_universes -> unit
diff --git a/checker/values.ml b/checker/values.ml
index ed730cff8e..cba96e6636 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -227,8 +227,11 @@ let v_oracle =
     v_pred v_cst;
   |]
 
-let v_pol_arity =
-  v_tuple "polymorphic_arity" [|List(Opt v_level);v_univ;v_context_set|]
+let v_template_arity =
+  v_tuple "template_arity" [|v_univ|]
+
+let v_template_universes =
+  v_tuple "template_universes" [|List(Opt v_level);v_context_set|]
 
 let v_primitive =
   v_enum "primitive" 44 (* Number of "Primitive" in Int63.v and PrimFloat.v *)
@@ -265,7 +268,7 @@ let v_mono_ind_arity =
   v_tuple "monomorphic_inductive_arity" [|v_constr;v_sort|]
 
 let v_ind_arity = v_sum "inductive_arity" 0
-  [|[|v_mono_ind_arity|];[|v_pol_arity|]|]
+  [|[|v_mono_ind_arity|];[|v_template_arity|]|]
 
 let v_one_ind = v_tuple "one_inductive_body"
   [|v_id;
@@ -301,6 +304,7 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     Int;
     v_rctxt;
     v_univs; (* universes *)
+    Opt v_template_universes;
     Opt (Array v_variance);
     Opt (Array v_variance);
     Opt v_bool;
diff --git a/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh
new file mode 100644
index 0000000000..f8871ae158
--- /dev/null
+++ b/dev/ci/user-overlays/11764-ppedrot-simplify-template.sh
@@ -0,0 +1,18 @@
+if [ "$CI_PULL_REQUEST" = "11764" ] || [ "$CI_BRANCH" = "simplify-template" ]; then
+
+    elpi_CI_REF="simplify-template"
+    elpi_CI_GITURL=https://github.com/ppedrot/coq-elpi
+
+    equations_CI_REF="simplify-template"
+    equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+
+    paramcoq_CI_REF="simplify-template"
+    paramcoq_CI_GITURL=https://github.com/ppedrot/paramcoq
+
+    mtac2_CI_REF="simplify-template"
+    mtac2_CI_GITURL=https://github.com/ppedrot/Mtac2
+
+    rewriter_CI_REF="simplify-template"
+    rewriter_CI_GITURL=https://github.com/ppedrot/rewriter
+
+fi
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31dd26d2ba..13ee353c6b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t =
   t
 
 let cook_one_ind ~ntypes
-    (section_decls,_ as hyps) expmod mip =
+    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;template_context} ->
-      let sec_levels = CList.map_filter (fun d ->
-          if RelDecl.is_local_assum d then Some None
-          else None)
-          section_decls
-      in
-      let levels = List.rev_append sec_levels levels in
-      TemplateArity {template_param_levels=levels;template_level;template_context}
+    | TemplateArity {template_level} ->
+      TemplateArity {template_level}
   in
   let mind_arity_ctxt =
     let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
@@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
       in
       Some (Array.append newvariance variance), Some sec_variance
   in
+  let mind_template = match mib.mind_template with
+  | None -> None
+  | Some {template_param_levels=levels; template_context} ->
+      let sec_levels = CList.map_filter (fun d ->
+          if RelDecl.is_local_assum d then Some None
+          else None)
+          section_decls
+      in
+      let levels = List.rev_append sec_levels levels in
+      Some {template_param_levels=levels; template_context}
+  in
   {
     mind_packets;
     mind_record;
@@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib =
     mind_nparams_rec = mib.mind_nparams_rec + nnewparams;
     mind_params_ctxt;
     mind_universes;
+    mind_template;
     mind_variance;
     mind_sec_variance;
     mind_private = mib.mind_private;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ac130d018d..11a07ee5cf 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -30,8 +30,11 @@ type engagement = set_predicativity
 *)
 
 type template_arity = {
-  template_param_levels : Univ.Level.t option list;
   template_level : Univ.Universe.t;
+}
+
+type template_universes = {
+  template_param_levels : Univ.Level.t option list;
   template_context : Univ.ContextSet.t;
 }
 
@@ -218,6 +221,8 @@ type mutual_inductive_body = {
 
     mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
 
+    mind_template : template_universes option;
+
     mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
 
     mind_sec_variance : Univ.Variance.t array option;
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index a3adac7a11..a1122d1279 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -46,9 +46,10 @@ let map_decl_arity f g = function
   | TemplateArity a -> TemplateArity (g a)
 
 let hcons_template_arity ar =
+  { template_level = Univ.hcons_univ ar.template_level; }
+
+let hcons_template_universe 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_context = Univ.hcons_universe_context_set ar.template_context }
 
 let universes_context = function
@@ -247,6 +248,7 @@ let subst_mind_body sub mib =
       Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
     mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
     mind_universes = mib.mind_universes;
+    mind_template = mib.mind_template;
     mind_variance = mib.mind_variance;
     mind_sec_variance = mib.mind_sec_variance;
     mind_private = mib.mind_private;
@@ -323,6 +325,7 @@ let hcons_mind mib =
   { mib with
     mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
     mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
+    mind_template = Option.Smart.map hcons_template_universe mib.mind_template;
     mind_universes = hcons_universes mib.mind_universes }
 
 (** Hashconsing of modules *)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 8d930b521c..983fa822e9 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
 type one_inductive_entry = {
   mind_entry_typename : Id.t;
   mind_entry_arity : constr;
-  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_consnames : Id.t list;
   mind_entry_lc : constr list }
 
@@ -50,6 +49,7 @@ type mutual_inductive_entry = {
   mind_entry_params : Constr.rel_context;
   mind_entry_inds : one_inductive_entry list;
   mind_entry_universes : universes_entry;
+  mind_entry_template : bool; (* Use template polymorphism *)
   mind_entry_cumulative : bool;
   (* universe constraints and the constraints for subtyping of
      inductive types in the block. *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 501ac99ff3..1b5a77cc96 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env =
   | TemplateArity _ -> true
   | RegularArity _ -> false
 
-let template_polymorphic_variables (mind,i) env =
-  match (lookup_mind mind env).mind_packets.(i).mind_arity with
-  | TemplateArity { Declarations.template_param_levels = l; _ } ->
+let template_polymorphic_variables (mind, _) env =
+  match (lookup_mind mind env).mind_template with
+  | Some { Declarations.template_param_levels = l; _ } ->
     List.map_filter (fun level -> level) l
-  | RegularArity _ -> []
+  | None -> []
 
 let template_polymorphic_pind (ind,u) env =
   if not (Univ.Instance.is_empty u) then false
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index cc15109f06..d5aadd0c02 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -101,10 +101,10 @@ let check_indices_matter env_params info indices =
   else check_context_univs ~ctor:false env_params info indices
 
 (* env_ar contains the inductives before the current ones in the block, and no parameters *)
-let check_arity env_params env_ar ind =
+let check_arity ~template env_params env_ar ind =
   let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in
   let indices, ind_sort = Reduction.dest_arity env_params arity in
-  let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in
+  let ind_min_univ = if template then Some Universe.type0m else None in
   let univ_info = {
     ind_squashed=false;
     ind_has_relevant_arg=false;
@@ -200,28 +200,88 @@ let unbounded_from_below u cstrs =
 let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl =
   let check_level l =
     Univ.LSet.mem l (Univ.ContextSet.levels uctx) &&
+    (let () = assert (not @@ Univ.Level.is_small l) in true) &&
     unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
     not (Univ.LSet.mem l ctor_levels)
   in
   let univs = Univ.Universe.levels concl in
-  let univs =
-    Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs
-  in
+  let univs = Univ.LSet.filter (fun l -> check_level l) univs in
   let fold acc = function
     | (LocalAssum (_, p)) ->
       (let c = Term.strip_prod_assum p in
       match kind c with
         | Sort (Type u) ->
             (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
+             | Some l -> if Univ.LSet.mem l univs then Some l else None
              | None -> None)
         | _ -> None) :: acc
     | LocalDef _ -> acc
   in
   let params = List.fold_left fold [] paramsctxt in
-  params, univs
+  if Universe.is_type0m concl then Some (univs, params)
+  else if not @@ Univ.LSet.is_empty univs then Some (univs, params)
+  else None
+
+let get_param_levels ctx params arity splayed_lc =
+  let min_univ = match arity with
+  | RegularArity _ ->
+    CErrors.user_err
+      Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.")
+  | TemplateArity ar -> ar.template_level
+  in
+  let ctor_levels =
+    let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
+    let param_levels =
+      List.fold_left (fun levels d -> match d with
+          | LocalAssum _ -> levels
+          | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
+        Univ.LSet.empty params
+    in
+    Array.fold_left
+      (fun levels (d,c) ->
+          let levels =
+            List.fold_left (fun levels d ->
+                Context.Rel.Declaration.fold_constr add_levels d levels)
+              levels d
+          in
+          add_levels c levels)
+      param_levels
+      splayed_lc
+  in
+  match template_polymorphic_univs ~ctor_levels ctx params min_univ with
+  | None ->
+    CErrors.user_err
+      Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
+  | Some (_, param_levels) ->
+    param_levels
+
+let get_template univs params data =
+  let ctx = match univs with
+      | Monomorphic ctx -> ctx
+      | Polymorphic _ ->
+        CErrors.anomaly ~label:"polymorphic_template_ind"
+          Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
+  (* For each type in the block, compute potential template parameters *)
+  let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in
+  (* Pick the lower bound of template parameters. Note that in particular, if
+     one of the the inductive types from the block is Prop-valued, then no
+     parameters are template. *)
+  let fold min params =
+    let map u v = match u, v with
+    | (None, _) | (_, None) -> None
+    | Some u, Some v ->
+      let () = assert (Univ.Level.equal u v) in
+      Some u
+    in
+    List.map2 map min params
+  in
+  let params = match params with
+  | [] -> assert false
+  | hd :: rem -> List.fold_left fold hd rem
+  in
+  { template_param_levels = params; template_context = ctx }
 
-let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+let abstract_packets usubst ((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
@@ -237,40 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
 
   let arity = match univ_info.ind_min_univ with
     | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ}
-    | Some min_univ ->
-      let ctx = match univs with
-          | Monomorphic ctx -> ctx
-          | Polymorphic _ ->
-            CErrors.anomaly ~label:"polymorphic_template_ind"
-              Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in
-      let ctor_levels =
-        let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in
-        let param_levels =
-          List.fold_left (fun levels d -> match d with
-              | LocalAssum _ -> levels
-              | LocalDef (_,b,t) -> add_levels b (add_levels t levels))
-            Univ.LSet.empty params
-        in
-        Array.fold_left
-          (fun levels (d,c) ->
-             let levels =
-               List.fold_left (fun levels d ->
-                   Context.Rel.Declaration.fold_constr add_levels d levels)
-                 levels d
-             in
-             add_levels c levels)
-          param_levels
-          splayed_lc
-      in
-      let param_levels, concl_levels =
-        template_polymorphic_univs ~ctor_levels ctx params min_univ
-      in
-      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.")
-      else
-        TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
+    | Some min_univ -> TemplateArity { template_level = min_univ; }
   in
 
   let kelim = allowed_sorts univ_info in
@@ -285,7 +312,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   mind_check_names mie;
   assert (List.is_empty (Environ.rel_context env));
 
-  let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in
+  let has_template_poly = mie.mind_entry_template in
 
   (* universes *)
   let env_univs =
@@ -306,7 +333,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
   let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in
 
   (* Arities *)
-  let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in
+  let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in
   let env_ar_par = push_rel_context params env_ar in
 
   (* Constructors *)
@@ -352,7 +379,14 @@ 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 data = List.map (abstract_packets univs usubst params) data in
+  let data = List.map (abstract_packets usubst) data in
+  let template =
+    let check ((arity, _), _, _) = match arity with
+    | TemplateArity _ -> true
+    | RegularArity _ -> false
+    in
+    if List.exists check data then Some (get_template univs params data) else None
+  in
 
   let env_ar_par =
     let ctx = Environ.rel_context env_ar_par in
@@ -361,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
     Environ.push_rel_context ctx env
   in
 
-  env_ar_par, univs, variance, record, params, Array.of_list data
+  env_ar_par, univs, template, variance, record, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 723ba5459e..babb82c39e 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option
   -> mutual_inductive_entry
   -> env
   * universes
+  * template_universes option
   * Univ.Variance.t array option
   * Names.Id.t array option option
   * Constr.rel_context
@@ -44,4 +45,4 @@ val template_polymorphic_univs :
   Univ.ContextSet.t ->
   Constr.rel_context ->
   Univ.Universe.t ->
-  Univ.Level.t option list * Univ.LSet.t
+  (Univ.LSet.t * Univ.Level.t option list) option
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index b6b8e5265c..58e5e76b61 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib =
   Array.of_list (List.rev rs),
   Array.of_list (List.rev pbs)
 
-let build_inductive env ~sec_univs names prv univs variance
+let build_inductive env ~sec_univs names prv univs template variance
     paramsctxt kn isrecord isfinite inds nmr recargs =
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
@@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance
       mind_params_ctxt = paramsctxt;
       mind_packets = packets;
       mind_universes = univs;
+      mind_template = template;
       mind_variance = variance;
       mind_sec_variance = sec_variance;
       mind_private = prv;
@@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance
 
 let check_inductive env ~sec_univs kn mie =
   (* First type-check the inductive definition *)
-  let (env_ar_par, univs, variance, record, paramsctxt, inds) =
+  let (env_ar_par, univs, template, variance, record, paramsctxt, inds) =
     IndTyping.typecheck_inductive env ~sec_univs mie
   in
   (* Then check positivity conditions *)
@@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie =
       (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
   in
   (* Build the inductive packets *)
-    build_inductive env ~sec_univs names mie.mind_entry_private univs variance
+    build_inductive env ~sec_univs names mie.mind_entry_private univs template variance
       paramsctxt kn record mie.mind_entry_finite
       inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 1be86f2bf8..6325779675 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -185,8 +185,8 @@ let make_subst =
 
 exception SingletonInductiveBecomesProp of Id.t
 
-let instantiate_universes ctx ar args =
-  let subst = make_subst (ctx,ar.template_param_levels,args) in
+let instantiate_universes ctx (templ, ar) args =
+  let subst = make_subst (ctx,templ.template_param_levels,args) in
   let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in
   let ty =
     (* Singleton type not containing types are interpretable in Prop *)
@@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a -> subst_instance_constr u a.mind_user_arity
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let ctx = List.rev mip.mind_arity_ctxt in
-    let ctx,s = instantiate_universes ctx ar paramtyps in
+    let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in
       (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
          the situation where a non-Prop singleton inductive becomes Prop
          when applied to Prop params *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index b690fe1157..90571844b9 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t
 
 val max_inductive_sort : Sorts.t array -> Universe.t
 
-val instantiate_universes : Constr.rel_context ->
-  template_arity -> param_univs -> Constr.rel_context * Sorts.t
-
 (** {6 Debug} *)
 
 type size = Large | Strict
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index aafd662f7d..c9ccd668ca 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -78,9 +78,9 @@ let get_polymorphic_positions env sigma f =
   match EConstr.kind sigma f with
   | Ind (ind, u) | Construct ((ind, _), u) ->
     let mib,oib = Inductive.lookup_mind_specif env ind in
-      (match oib.mind_arity with
-      | RegularArity _ -> assert false
-      | TemplateArity templ -> templ.template_param_levels)
+      (match mib.mind_template with
+      | None -> assert false
+      | Some templ -> templ.template_param_levels)
   | _ -> assert false
 
 let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index a4406aeba1..01994a35c7 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -681,13 +681,17 @@ let type_of_inductive_knowing_conclusion env sigma ((mib,mip),u) conclty =
   match mip.mind_arity with
   | RegularArity s -> sigma, EConstr.of_constr (subst_instance_constr u s.mind_user_arity)
   | TemplateArity ar ->
+    let templ = match mib.mind_template with
+    | None -> assert false
+    | Some t -> t
+    in
     let _,scl = splay_arity env sigma conclty in
     let scl = EConstr.ESorts.kind sigma scl in
     let ctx = List.rev mip.mind_arity_ctxt in
     let evdref = ref sigma in
     let ctx =
       instantiate_universes
-        env evdref scl ar.template_level (ctx,ar.template_param_levels) in
+        env evdref scl ar.template_level (ctx,templ.template_param_levels) in
       !evdref, EConstr.of_constr (mkArity (List.rev ctx,scl))
 
 let type_of_projection_constant env (p,u) =
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index edb03a5c89..718e62b9b7 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -329,10 +329,7 @@ let template_polymorphism_candidate ~ctor_levels uctx params concl =
     if not concltemplate then false
     else
       let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
-      let params, conclunivs =
-        IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
-      in
-      not (Univ.LSet.is_empty conclunivs)
+      Option.has_some @@ IndTyping.template_polymorphic_univs ~ctor_levels uctx params conclu
   | Entries.Polymorphic_entry _ -> false
 
 let check_param = function
@@ -370,6 +367,14 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
 
   (* Build the inductive entries *)
   let entries = List.map4 (fun indname (templatearity, arity) concl (cnames,ctypes) ->
+      { mind_entry_typename = indname;
+        mind_entry_arity = arity;
+        mind_entry_consnames = cnames;
+        mind_entry_lc = ctypes
+      })
+      indnames arities arityconcl constructors
+  in
+  let template = List.map4 (fun indname (templatearity, _) concl (_, ctypes) ->
       let template_candidate () =
         templatearity ||
         let ctor_levels =
@@ -385,22 +390,17 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
         in
         template_polymorphism_candidate ~ctor_levels uctx ctx_params concl
       in
-      let template = match template with
+      match template with
         | Some template ->
           if poly && template then user_err
               Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
           template
         | None ->
           should_auto_template indname (template_candidate ())
-      in
-      { mind_entry_typename = indname;
-        mind_entry_arity = arity;
-        mind_entry_template = template;
-        mind_entry_consnames = cnames;
-        mind_entry_lc = ctypes
-      })
+      )
       indnames arities arityconcl constructors
   in
+  let is_template = List.for_all (fun t -> t) template in
   (* Build the mutual inductive entry *)
   let mind_ent =
     { mind_entry_params = ctx_params;
@@ -409,6 +409,7 @@ let interp_mutual_inductive_constr ~sigma ~template ~udecl ~ctx_params ~indnames
       mind_entry_inds = entries;
       mind_entry_private = if private_ind then Some false else None;
       mind_entry_universes = uctx;
+      mind_entry_template = is_template;
       mind_entry_cumulative = poly && cumulative;
     }
   in
diff --git a/vernac/record.ml b/vernac/record.ml
index 3e44cd85cc..065641989d 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -423,7 +423,13 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
     let args = Context.Rel.to_extended_list mkRel nfields params in
     let ind = applist (mkRel (ntypes - i + nparams + nfields), args) in
     let type_constructor = it_mkProd_or_LetIn ind fields in
-    let template =
+    { mind_entry_typename = id;
+      mind_entry_arity = arity;
+      mind_entry_consnames = [idbuild];
+      mind_entry_lc = [type_constructor] }
+  in
+  let blocks = List.mapi mk_block record_data in
+  let check_template (id, _, min_univ, _, _, fields, _, _) =
       let template_candidate () =
         (* we use some dummy values for the arities in the rel_context
            as univs_of_constr doesn't care about localassums and
@@ -454,14 +460,8 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
       | None, template ->
         (* auto detect template *)
         ComInductive.should_auto_template id (template && template_candidate ())
-    in
-    { mind_entry_typename = id;
-      mind_entry_arity = arity;
-      mind_entry_template = template;
-      mind_entry_consnames = [idbuild];
-      mind_entry_lc = [type_constructor] }
   in
-  let blocks = List.mapi mk_block record_data in
+  let template = List.for_all check_template record_data in
   let primitive =
     !primitive_flag &&
     List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
@@ -473,6 +473,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
       mind_entry_inds = blocks;
       mind_entry_private = None;
       mind_entry_universes = univs;
+      mind_entry_template = template;
       mind_entry_cumulative = poly && cumulative;
     }
   in