Make kernel parametric on the lowest universe and fix #9294

This could be Prop (for compat with usual Coq), Set (for HoTT),
 or actually an arbitrary "i".

Take lower bound of universes into account in pretyping/engine

Reinstate proper elaboration of SProp <= l constraints:

replacing is_small with equality with lbound is _not_ semantics preserving!

lbound = Set

Elaborate template polymorphic inductives with lower bound Prop

This will make more constraints explicit

Check univ constraints with Prop as lower bound for template inductives

Restrict template polymorphic universes to those not bounded from below

Fixes #9294

fix suggested by Matthieu

Try second fix suggested by Matthieu

Take care of modifying elaboration for record declarations as well.

Rebase and export functions for debug

Remove exported functions used while debugging

Add a new typing flag "check_template" and option "-no-template-checl"

This parameterizes the new criterion on template polymorphic inductives
to allow bypassing it (necessary for backward compatibility).

Update checker to the new typing flags structure

Switch on the new template_check flag to allow old unsafe behavior in
indTyping.

This is the only change of code really impacting the kernel, together
with the commit implementing unbounded from below and parameterization
by the lower bound on universes.

Add deprecated option `Unset Template Check` allowing to make proof
scripts work with both 8.9 and 8.10 for a while

Fix `Template Check` option name and test it

Add `Unset Template Check` to Coq89.v

Cooking of inductives and template-check tests

Cleanup test-suite file for template check / universes(template) flags

cookind tests

Move test of `Unset Template Check` to the failure/ dir, but comment it
for now

Template test-suite test explanation

Overlays for PR 9918

Overlay for paramcoq

Add overlay for fiat_parsers (-no-template-check)

Add overlay for fiat_crypto_legacy

Update fiat-crypto legacy overlay

Now it points at the version that I plan on merging; I am hoping that doing this will guard against mistakes by adding an extra check that the target tested by Coq's CI on this branch works with the change I made.

Remove overlay that should no longer be necessary

The setting in the compat file should handle it

Remove now-merged fiat-crypto-legacy overlay

Update `Print Assumptions` to reflect the typing flag for template checking

Fix About and Print Assumptions for template poly, giving info on which
variables are actually polymorphic

Fix pretty printing to print global universe levels properly

Fix printing of template polymorphic universes

Fix pretty printing for template polymorphism on no universe

Fix interaction of template check and universes(template) flag

Fix indTyping to really check if there is any point in polymorphism: the
conclusion sort should be parameterized over at least one local universe

Indtyping fixes for template polymorphic Props

Allow explicit template polymorphism again

Adapt to new indTyping interface

Handle the case of template-polymorphic on no universes
correctly (morally Type0m univ represented as Prop).

Fix check of meaningfullness of template polymorphism in the kernel.

It is now done w.r.t the min_univ, the minimal universe inferred for the
inductive/record type, independently of the user-written annotation
which must only be larger than min_univ. This preserves compatibility
with UniMath and template-polymorphism as it has been implemented up-to
now.

Comment on identity non-template-polymorphism

Remove incorrect universes(template) attributes from ssr

simpl_fun can be meaningfully template-poly, as well as
pred_key (although the use is debatable: it could just
as well be in Prop).

Move `fun_of_simpl` coercion declaration out of section to respect
uniform inheritance

Remove incorrect uses of #[universes(template)] from the stdlib

Extraction of micromega changes due to moving an ind decl out of a section

Remove incorrect uses of #[universes(template)] from plugins

Fix test-suite files, removing incorrect #[universes(template)] attributes

Remove incorrect #[universes(template)] attributes in test-suite

Fix test-suite

Remove overlays as they have been merged upstream.

8 files changed, 174 insertions, 83 deletions

diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index a72e43de01..cb034bdff6 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -353,6 +353,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st gr t =
           let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
           ContextObjectMap.add (Axiom (TypeInType obj, l)) Constr.mkProp accu
       in
-      accu
-
+      if not mind.mind_typing_flags.check_template then
+        let l = try GlobRef.Map_env.find obj ax2ty with Not_found -> [] in
+        ContextObjectMap.add (Axiom (TemplatePolymorphic m, l)) Constr.mkProp accu
+      else accu
   in GlobRef.Map_env.fold fold graph ContextObjectMap.empty
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml
index d414d57c0d..98fe436a22 100644
--- a/vernac/auto_ind_decl.ml
+++ b/vernac/auto_ind_decl.ml
@@ -345,7 +345,7 @@ let build_beq_scheme mode kn =
           Vars.substl subst cores.(i)
         in
         create_input fix),
-       UState.make (Global.universes ())),
+       UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())),
       !eff
 
 let beq_scheme_kind = declare_mutual_scheme_object "_beq" build_beq_scheme
@@ -690,7 +690,7 @@ let make_bl_scheme mode mind =
   let lnonparrec,lnamesparrec = (* TODO subst *)
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let bl_goal, eff = compute_bl_goal ind lnamesparrec nparrec in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let bl_goal = EConstr.of_constr bl_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx bl_goal
@@ -820,7 +820,7 @@ let make_lb_scheme mode mind =
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let lb_goal, eff = compute_lb_goal ind lnamesparrec nparrec in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let side_eff = side_effect_of_mode mode in
   let lb_goal = EConstr.of_constr lb_goal in
   let (ans, _, ctx) = Pfedit.build_by_tactic ~poly:false ~side_eff (Global.env()) ctx lb_goal
@@ -996,7 +996,7 @@ let make_eq_decidability mode mind =
   let nparams = mib.mind_nparams in
   let nparrec = mib.mind_nparams_rec in
   let u = Univ.Instance.empty in
-  let ctx = UState.make (Global.universes ()) in
+  let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
   let lnonparrec,lnamesparrec =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   let side_eff = side_effect_of_mode mode in
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index adbe196699..87dab72880 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -114,20 +114,22 @@ let mk_mltype_data sigma env assums arity indname =
     inductives which are recognized when a "Type" appears at the end of the conlusion in
     the source syntax. *)
 
-let rec check_anonymous_type ind =
+let rec check_type_conclusion ind =
   let open Glob_term in
     match DAst.get ind with
-    | GSort (UAnonymous {rigid=true}) -> true
+    | GSort (UAnonymous {rigid=true}) -> (Some true)
+    | GSort (UNamed _) -> (Some false)
     | GProd ( _, _, _, e)
     | GLetIn (_, _, _, e)
     | GLambda (_, _, _, e)
     | GApp (e, _)
-    | GCast (e, _) -> check_anonymous_type e
-    | _ -> false
+    | GCast (e, _) -> check_type_conclusion e
+    | _ -> None
 
-let make_conclusion_flexible sigma = function
+let make_anonymous_conclusion_flexible sigma = function
   | None -> sigma
-  | Some s ->
+  | Some (false, _) -> sigma
+  | Some (true, s) ->
     (match EConstr.ESorts.kind sigma s with
      | Type u ->
        (match Univ.universe_level u with
@@ -136,17 +138,23 @@ let make_conclusion_flexible sigma = function
         | None -> sigma)
      | _ -> sigma)
 
-let interp_ind_arity env sigma ind =
+let intern_ind_arity env sigma ind =
   let c = intern_gen IsType env sigma ind.ind_arity in
   let impls = Implicit_quantifiers.implicits_of_glob_constr ~with_products:true c in
+  let pseudo_poly = check_type_conclusion c in
+  (constr_loc ind.ind_arity, c, impls, pseudo_poly)
+
+let pretype_ind_arity env sigma (loc, c, impls, pseudo_poly) =
   let sigma,t = understand_tcc env sigma ~expected_type:IsType c in
-  let pseudo_poly = check_anonymous_type c in
   match Reductionops.sort_of_arity env sigma t with
   | exception Invalid_argument _ ->
-    user_err ?loc:(constr_loc ind.ind_arity) (str "Not an arity")
+    user_err ?loc (str "Not an arity")
   | s ->
-    let concl = if pseudo_poly then Some s else None in
-    sigma, (t, Retyping.relevance_of_sort s,  concl, impls)
+    let concl = match pseudo_poly with
+      | Some b -> Some (b, s)
+      | None -> None
+    in
+    sigma, (t, Retyping.relevance_of_sort s, concl, impls)
 
 let interp_cstrs env sigma impls mldata arity ind =
   let cnames,ctyps = List.split ind.ind_lc in
@@ -251,7 +259,7 @@ let solve_constraints_system levels level_bounds =
   done;
   v
 
-let inductive_levels env evd poly arities inds =
+let inductive_levels env evd arities inds =
   let destarities = List.map (fun x -> x, Reduction.dest_arity env x) arities in
   let levels = List.map (fun (x,(ctx,a)) ->
     if Sorts.is_prop a || Sorts.is_sprop a then None
@@ -286,7 +294,7 @@ let inductive_levels env evd poly arities inds =
     CList.fold_left3 (fun (evd, arities) cu (arity,(ctx,du)) len ->
       if is_impredicative_sort env du then
         (* Any product is allowed here. *)
-        evd, arity :: arities
+        evd, (false, arity) :: arities
       else (* If in a predicative sort, or asked to infer the type,
               we take the max of:
               - indices (if in indices-matter mode)
@@ -300,7 +308,6 @@ let inductive_levels env evd poly arities inds =
               raise (InductiveError LargeNonPropInductiveNotInType)
             else evd
           else evd
-            (* Evd.set_leq_sort env evd (Type cu) du *)
         in
         let evd =
           if len >= 2 && Univ.is_type0m_univ cu then
@@ -311,14 +318,14 @@ let inductive_levels env evd poly arities inds =
           else evd
         in
         let duu = Sorts.univ_of_sort du in
-        let evd =
+        let template_prop, evd =
           if not (Univ.is_small_univ duu) && Univ.Universe.equal cu duu then
             if is_flexible_sort evd duu && not (Evd.check_leq evd Univ.type0_univ duu) then
-              Evd.set_eq_sort env evd Sorts.prop du
-            else evd
-          else Evd.set_eq_sort env evd (sort_of_univ cu) du
+              true, Evd.set_eq_sort env evd Sorts.prop du
+            else false, evd
+          else false, Evd.set_eq_sort env evd (sort_of_univ cu) du
         in
-          (evd, arity :: arities))
+          (evd, (template_prop, arity) :: arities))
     (evd,[]) (Array.to_list levels') destarities sizes
   in evd, List.rev arities
 
@@ -328,6 +335,17 @@ let check_named {CAst.loc;v=na} = match na with
   let msg = str "Parameters must be named." in
   user_err ?loc  msg
 
+let template_polymorphism_candidate env uctx params concl =
+  match uctx with
+  | Entries.Monomorphic_entry uctx ->
+    let concltemplate = Option.cata (fun s -> not (Sorts.is_small s)) false concl in
+    if not concltemplate then false
+    else
+      let template_check = Environ.check_template env in
+      let conclu = Option.cata Sorts.univ_of_sort Univ.type0m_univ concl in
+      let params, conclunivs = IndTyping.template_polymorphic_univs ~template_check uctx params conclu in
+      not (template_check && Univ.LSet.is_empty conclunivs)
+  | Entries.Polymorphic_entry _ -> false
 
 let check_param = function
 | CLocalDef (na, _, _) -> check_named na
@@ -345,25 +363,46 @@ let restrict_inductive_universes sigma ctx_params arities constructors =
   let uvars = List.fold_right (fun (_,ctypes,_) -> List.fold_right merge_universes_of_constr ctypes) constructors uvars in
   Evd.restrict_universe_context sigma uvars
 
-let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
-  check_all_names_different indl;
-  List.iter check_param paramsl;
-  if not (List.is_empty uparamsl) && not (List.is_empty notations)
-  then user_err (str "Inductives with uniform parameters may not have attached notations.");
-  let sigma, udecl = interp_univ_decl_opt env0 udecl in
+let interp_params env udecl uparamsl paramsl =
+  let sigma, udecl = interp_univ_decl_opt env udecl in
   let sigma, (uimpls, ((env_uparams, ctx_uparams), useruimpls)) =
-    interp_context_evars ~program_mode:false env0 sigma uparamsl in
+    interp_context_evars ~program_mode:false env sigma uparamsl in
   let sigma, (impls, ((env_params, ctx_params), userimpls)) =
     interp_context_evars ~program_mode:false ~impl_env:uimpls env_uparams sigma paramsl
   in
-  let indnames = List.map (fun ind -> ind.ind_name) indl in
-
   (* Names of parameters as arguments of the inductive type (defs removed) *)
   let assums = List.filter is_local_assum ctx_params in
-  let params = List.map (RelDecl.get_name %> Name.get_id) assums in
+  sigma, env_params, (ctx_params, env_uparams, ctx_uparams,
+  List.map (RelDecl.get_name %> Name.get_id) assums, userimpls, useruimpls, impls, udecl)
+
+let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
+  check_all_names_different indl;
+  List.iter check_param paramsl;
+  if not (List.is_empty uparamsl) && not (List.is_empty notations)
+  then user_err (str "Inductives with uniform parameters may not have attached notations.");
+
+  let indnames = List.map (fun ind -> ind.ind_name) indl in
+  let sigma, env_params, infos =
+    interp_params env0 udecl uparamsl paramsl
+  in
 
   (* Interpret the arities *)
-  let sigma, arities = List.fold_left_map (fun sigma -> interp_ind_arity env_params sigma) sigma indl in
+  let arities = List.map (intern_ind_arity env_params sigma) indl in
+
+  let sigma, env_params, (ctx_params, env_uparams, ctx_uparams, params, userimpls, useruimpls, impls, udecl), arities, is_template =
+    let is_template = List.exists (fun (_,_,_,pseudo_poly) -> not (Option.is_empty pseudo_poly)) arities in
+    if not poly && is_template then
+      (* In case of template polymorphism, we need to compute more constraints *)
+      let env0 = Environ.set_universes_lbound env0 Univ.Level.prop in
+      let sigma, env_params, infos =
+        interp_params env0 udecl uparamsl paramsl
+      in
+      let arities = List.map (intern_ind_arity env_params sigma) indl in
+      sigma, env_params, infos, arities, is_template
+    else sigma, env_params, infos, arities, is_template
+  in
+
+  let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
   let arities, relevances, arityconcl, indimpls = List.split4 arities in
 
   let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
@@ -410,31 +449,34 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let nf = Evarutil.nf_evars_universes sigma in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let arities = List.map EConstr.(to_constr sigma) arities in
-  let sigma = List.fold_left make_conclusion_flexible sigma arityconcl in
-  let sigma, arities = inductive_levels env_ar_params sigma poly arities constructors in
+  let sigma = List.fold_left make_anonymous_conclusion_flexible sigma arityconcl in
+  let sigma, arities = inductive_levels env_ar_params sigma arities constructors in
   let sigma = Evd.minimize_universes sigma in
   let nf = Evarutil.nf_evars_universes sigma in
-  let arities = List.map nf arities in
+  let arities = List.map (fun (template, arity) -> template, nf arity) arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf cl,impsl)) constructors in
   let ctx_params = List.map Termops.(map_rel_decl (EConstr.to_constr sigma)) ctx_params in
-  let arityconcl = List.map (Option.map (EConstr.ESorts.kind sigma)) arityconcl in
-  let sigma = restrict_inductive_universes sigma ctx_params arities constructors in
+  let arityconcl = List.map (Option.map (fun (anon, s) -> EConstr.ESorts.kind sigma s)) arityconcl in
+  let sigma = restrict_inductive_universes sigma ctx_params (List.map snd arities) constructors in
   let uctx = Evd.check_univ_decl ~poly sigma udecl in
-  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr c)) arities;
+  List.iter (fun c -> check_evars env_params (Evd.from_env env_params) sigma (EConstr.of_constr (snd c))) arities;
   Context.Rel.iter (fun c -> check_evars env0 (Evd.from_env env0) sigma (EConstr.of_constr c)) ctx_params;
   List.iter (fun (_,ctyps,_) ->
     List.iter (fun c -> check_evars env_ar_params (Evd.from_env env_ar_params) sigma (EConstr.of_constr c)) ctyps)
     constructors;
 
   (* Build the inductive entries *)
-  let entries = List.map4 (fun ind arity concl (cnames,ctypes,cimpls) ->
+  let entries = List.map4 (fun ind (templatearity, arity) concl (cnames,ctypes,cimpls) ->
+      let template_candidate () =
+        templatearity || template_polymorphism_candidate env0 uctx ctx_params concl in
       let template = match template with
         | Some template ->
           if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+          if template && not (template_candidate ()) then
+            user_err Pp.(strbrk "inductive cannot be made template polymorphic on any universe");
           template
         | None ->
-          should_auto_template ind.ind_name (not poly &&
-          Option.cata (fun s -> not (Sorts.is_small s)) false concl)
+          should_auto_template ind.ind_name (template_candidate ())
       in
       { mind_entry_typename = ind.ind_name;
         mind_entry_arity = arity;
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 285be8cd51..7587bd165f 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -62,3 +62,17 @@ val should_auto_template : Id.t -> bool -> bool
 (** [should_auto_template x b] is [true] when [b] is [true] and we
    automatically use template polymorphism. [x] is the name of the
    inductive under consideration. *)
+
+val template_polymorphism_candidate :
+  Environ.env -> Entries.universes_entry -> Constr.rel_context -> Sorts.t option -> bool
+(** [template_polymorphism_candidate env uctx params conclsort] is
+   [true] iff an inductive with params [params] and conclusion
+   [conclsort] would be definable as template polymorphic.  It should
+   have at least one universe in its monomorphic universe context that
+   can be made parametric in its conclusion sort, if one is given.
+   If the [Template Check] flag is false we just check that the conclusion sort
+   is not small. *)
+
+val sign_level : Environ.env -> Evd.evar_map -> Constr.rel_declaration list -> Univ.Universe.t
+(** [sign_level env sigma ctx] computes the universe level of the context [ctx]
+    as the [sup] of its individual assumptions, which should be well-typed in [env] and [sigma] *)
diff --git a/vernac/declareObl.ml b/vernac/declareObl.ml
index c5cbb095ca..e7773abaf4 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -541,7 +541,7 @@ let obligation_terminator entries uctx { name; num; auto } =
            declares the univs of the constant,
            each subsequent obligation declares its own additional
            universes and constraints if any *)
-        if defined then UState.make (Global.universes ())
+        if defined then UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ())
         else ctx
     in
     let prg = {prg with prg_ctx} in
diff --git a/vernac/obligations.ml b/vernac/obligations.ml
index 37fe0df0ee..334d9e81fa 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -454,7 +454,7 @@ let obligation_hook prg obl num auto { DeclareDef.Hook.S.uctx = ctx'; dref; _ }
     if not prg.prg_poly (* Not polymorphic *) then
       (* The universe context was declared globally, we continue
          from the new global environment. *)
-      let ctx = UState.make (Global.universes ()) in
+      let ctx = UState.make ~lbound:(Global.universes_lbound ()) (Global.universes ()) in
       let ctx' = UState.merge_subst ctx (UState.subst ctx') in
       Univ.Instance.empty, ctx'
     else
diff --git a/vernac/record.ml b/vernac/record.ml
index 86745212e7..cfcbd1d7ae 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -85,10 +85,10 @@ let interp_fields_evars env sigma impls_env nots l =
 
 let compute_constructor_level evars env l =
   List.fold_right (fun d (env, univ) ->
-    let univ = 
+    let univ =
       if is_local_assum d then
 	let s = Retyping.get_sort_of env evars (RelDecl.get_type d) in
-	  Univ.sup (univ_of_sort s) univ 
+          Univ.sup (univ_of_sort s) univ
       else univ
     in (EConstr.push_rel d env, univ))
     l (env, Univ.Universe.sprop)
@@ -101,8 +101,19 @@ let binder_of_decl = function
 
 let binders_of_decls = List.map binder_of_decl
 
+let check_anonymous_type ind =
+  match ind with
+  | { CAst.v = CSort (Glob_term.UAnonymous {rigid=true}) } -> true
+  | _ -> false
+
 let typecheck_params_and_fields finite def poly pl ps records =
   let env0 = Global.env () in
+  (* Special case elaboration for template-polymorphic inductives,
+     lower bound on introduced universes is Prop so that we do not miss
+     any Set <= i constraint for universes that might actually be instantiated with Prop. *)
+  let is_template =
+    List.exists (fun (_, arity, _, _) -> Option.cata check_anonymous_type true arity) records in
+  let env0 = if not poly && is_template then Environ.set_universes_lbound env0 Univ.Level.prop else env0 in
   let sigma, decl = Constrexpr_ops.interp_univ_decl_opt env0 pl in
   let () =
     let error bk {CAst.loc; v=name} =
@@ -111,15 +122,15 @@ let typecheck_params_and_fields finite def poly pl ps records =
         user_err ?loc ~hdr:"record" (str "Record parameters must be named")
       | _ -> ()
     in
-      List.iter 
+      List.iter
 	(function CLocalDef (b, _, _) -> error default_binder_kind b
 	   | CLocalAssum (ls, bk, ce) -> List.iter (error bk) ls
            | CLocalPattern {CAst.loc} ->
               Loc.raise ?loc (Stream.Error "pattern with quote not allowed in record parameters")) ps
-  in 
+  in
   let sigma, (impls_env, ((env1,newps), imps)) = interp_context_evars ~program_mode:false env0 sigma ps in
   let fold (sigma, template) (_, t, _, _) = match t with
-    | Some t -> 
+    | Some t ->
        let env = EConstr.push_rel_context newps env0 in
        let poly =
          match t with
@@ -138,7 +149,7 @@ let typecheck_params_and_fields finite def poly pl ps records =
                  (sigma, false), (s, s')
              else (sigma, false), (s, s'))
 	 | _ -> user_err ?loc:(constr_loc t) (str"Sort expected."))
-    | None -> 
+    | None ->
       let uvarkind = Evd.univ_flexible_alg in
       let sigma, s = Evd.new_sort_variable uvarkind sigma in
       (sigma, template), (EConstr.mkSort s, s)
@@ -168,23 +179,23 @@ let typecheck_params_and_fields finite def poly pl ps records =
     let _, univ = compute_constructor_level sigma env_ar newfs in
     let univ = if Sorts.is_sprop sort then univ else Univ.Universe.sup univ Univ.type0m_univ in
       if not def && is_impredicative_sort env0 sort then
-        sigma, typ
+        sigma, (univ, typ)
       else
         let sigma = Evd.set_leq_sort env_ar sigma (Sorts.sort_of_univ univ) sort in
         if Univ.is_small_univ univ &&
            Option.cata (Evd.is_flexible_level sigma) false (Evd.is_sort_variable sigma sort) then
 	   (* We can assume that the level in aritysort is not constrained
 	       and clear it, if it is flexible *)
-   Evd.set_eq_sort env_ar sigma Sorts.set sort, EConstr.mkSort (Sorts.sort_of_univ univ)
-        else sigma, typ
+   Evd.set_eq_sort env_ar sigma Sorts.set sort, (univ, EConstr.mkSort (Sorts.sort_of_univ univ))
+        else sigma, (univ, typ)
   in
   let (sigma, typs) = List.fold_left2_map fold sigma typs data in
   let sigma, (newps, ans) = Evarutil.finalize sigma (fun nf ->
       let newps = List.map (RelDecl.map_constr_het nf) newps in
-      let map (impls, newfs) typ =
+      let map (impls, newfs) (univ, typ) =
         let newfs = List.map (RelDecl.map_constr_het nf) newfs in
         let typ = nf typ in
-        (typ, impls, newfs)
+        (univ, typ, impls, newfs)
       in
       let ans = List.map2 map data typs in
       newps, ans)
@@ -295,7 +306,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
   let x = make_annot (Name binder_name) mip.mind_relevance in
   let fields = instantiate_possibly_recursive_type (fst indsp) u mib.mind_ntypes paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
-  let primitive = 
+  let primitive =
     match mib.mind_record with
     | PrimRecord _ -> true
     | FakeRecord | NotRecord -> false
@@ -310,7 +321,7 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
 	  | Anonymous ->
 	      (None::sp_projs,i,NoProjection fi::subst)
 	  | Name fid -> try
-	    let kn, term = 
+            let kn, term =
 	      if is_local_assum decl && primitive then
                 let p = Projection.Repr.make indsp
                     ~proj_npars:mib.mind_nparams
@@ -354,12 +365,12 @@ let declare_projections indsp ctx ?(kind=Decls.StructureComponent) binder_name f
                   let kn = declare_constant ~name:fid ~kind (Declare.DefinitionEntry entry) in
 		  let constr_fip =
 		    let proj_args = (*Rel 1 refers to "x"*) paramargs@[mkRel 1] in
-		      applist (mkConstU (kn,u),proj_args) 
+                      applist (mkConstU (kn,u),proj_args)
                   in
                   Declare.definition_message fid;
 		    kn, constr_fip
                 with Type_errors.TypeError (ctx,te) ->
-                  raise (NotDefinable (BadTypedProj (fid,ctx,te))) 
+                  raise (NotDefinable (BadTypedProj (fid,ctx,te)))
 	    in
             let refi = GlobRef.ConstRef kn in
 	    Impargs.maybe_declare_manual_implicits false refi impls;
@@ -413,29 +424,33 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let binder_name =
     match name with
     | None ->
-      let map (id, _, _, _, _, _, _) =
+      let map (id, _, _, _, _, _, _, _) =
         Id.of_string (Unicode.lowercase_first_char (Id.to_string id))
       in
       Array.map_of_list map record_data
     | Some n -> n
   in
   let ntypes = List.length record_data in
-  let mk_block i (id, idbuild, arity, _, fields, _, _) =
+  let mk_block i (id, idbuild, min_univ, arity, _, fields, _, _) =
     let nfields = List.length fields in
     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 =
+      let template_candidate () =
+        ComInductive.template_polymorphism_candidate (Global.env ()) univs params
+          (Some (Sorts.sort_of_univ min_univ))
+      in
       match template with
       | Some template, _ ->
         (* templateness explicitly requested *)
         if poly && template then user_err Pp.(strbrk "template and polymorphism not compatible");
+        if template && not (template_candidate ()) then
+          user_err Pp.(strbrk "record cannot be made template polymorphic on any universe");
         template
       | None, template ->
         (* auto detect template *)
-        ComInductive.should_auto_template id (template && not poly &&
-        let _, s = Reduction.dest_arity (Global.env()) arity in
-        not (Sorts.is_small s))
+        ComInductive.should_auto_template id (template && template_candidate ())
     in
     { mind_entry_typename = id;
       mind_entry_arity = arity;
@@ -446,7 +461,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let blocks = List.mapi mk_block record_data in
   let primitive =
     !primitive_flag &&
-    List.for_all (fun (_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
+    List.for_all (fun (_,_,_,_,_,fields,_,_) -> List.exists is_local_assum fields) record_data
   in
   let mie =
     { mind_entry_params = params;
@@ -463,7 +478,7 @@ let declare_structure ~cumulative finite ubinders univs paramimpls params templa
   let kn = ComInductive.declare_mutual_inductive_with_eliminations mie ubinders impls
       ~primitive_expected:!primitive_flag
   in
-  let map i (_, _, _, fieldimpls, fields, is_coe, coers) =
+  let map i (_, _, _, _, fieldimpls, fields, is_coe, coers) =
     let rsp = (kn, i) in (* This is ind path of idstruc *)
     let cstr = (rsp, 1) in
     let kinds,sp_projs = declare_projections rsp ctx ~kind binder_name.(i) coers fieldimpls fields in
@@ -478,7 +493,7 @@ let implicits_of_context ctx =
   List.map (fun name -> CAst.make (Some (name,true)))
     (List.rev (Anonymous :: (List.map RelDecl.get_name ctx)))
 
-let declare_class def cumulative ubinders univs id idbuild paramimpls params arity
+let declare_class def cumulative ubinders univs id idbuild paramimpls params univ arity
     template fieldimpls fields ?(kind=Decls.StructureComponent) coers priorities =
   let fieldimpls =
     (* Make the class implicit in the projections, and the params if applicable. *)
@@ -493,7 +508,7 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
       let binder = {binder with binder_name=Name binder_name} in
       let class_body = it_mkLambda_or_LetIn field params in
       let class_type = it_mkProd_or_LetIn arity params in
-      let class_entry = 
+      let class_entry =
         Declare.definition_entry ~types:class_type ~univs class_body in
       let cst = Declare.declare_constant ~name:id
         (DefinitionEntry class_entry) ~kind:Decls.(IsDefinition Definition)
@@ -518,18 +533,18 @@ let declare_class def cumulative ubinders univs id idbuild paramimpls params ari
       Impargs.declare_manual_implicits false (GlobRef.ConstRef proj_cst) (List.hd fieldimpls);
       Classes.set_typeclass_transparency (EvalConstRef cst) false false;
       let sub = match List.hd coers with
-	| Some b -> Some ((if b then Backward else Forward), List.hd priorities) 
-	| None -> None 
+        | Some b -> Some ((if b then Backward else Forward), List.hd priorities)
+        | None -> None
       in
       [cref, [Name proj_name, sub, Some proj_cst]]
     | _ ->
-      let record_data = [id, idbuild, arity, fieldimpls, fields, false,
+      let record_data = [id, idbuild, univ, arity, fieldimpls, fields, false,
                          List.map (fun _ -> { pf_subclass = false ; pf_canonical = true }) fields] in
       let inds = declare_structure ~cumulative Declarations.BiFinite ubinders univs paramimpls
         params template ~kind:Decls.Method ~name:[|binder_name|] record_data
       in
-       let coers = List.map2 (fun coe pri -> 
-			      Option.map (fun b -> 
+       let coers = List.map2 (fun coe pri ->
+                              Option.map (fun b ->
 			      if b then Backward, pri else Forward, pri) coe)
 	  coers priorities
        in
@@ -584,7 +599,7 @@ let add_constant_class env sigma cst =
   let ctx, _ = decompose_prod_assum ty in
   let args = Context.Rel.to_extended_vect Constr.mkRel 0 ctx in
   let t = mkApp (mkConstU (cst, Univ.make_abstract_instance univs), args) in
-  let tc = 
+  let tc =
     { cl_univs = univs;
       cl_impl = GlobRef.ConstRef cst;
       cl_context = (List.map (const None) ctx, ctx);
@@ -688,24 +703,24 @@ let definition_structure udecl kind ~template ~cumulative ~poly finite records =
   let template = template, auto_template in
   match kind with
   | Class def ->
-    let (_, id, _, cfs, idbuild, _), (arity, implfs, fields) = match records, data with
+    let (_, id, _, cfs, idbuild, _), (univ, arity, implfs, fields) = match records, data with
     | [r], [d] -> r, d
     | _, _ -> CErrors.user_err (str "Mutual definitional classes are not handled")
     in
     let priorities = List.map (fun (_, { rf_priority }) -> {hint_priority = rf_priority ; hint_pattern = None}) cfs in
     let coers = List.map (fun (_, { rf_subclass }) -> rf_subclass) cfs in
     declare_class def cumulative ubinders univs id.CAst.v idbuild
-      implpars params arity template implfs fields coers priorities
+      implpars params univ arity template implfs fields coers priorities
   | _ ->
     let map impls = implpars @ [CAst.make None] @ impls in
-    let data = List.map (fun (arity, implfs, fields) -> (arity, List.map map implfs, fields)) data in
-    let map (arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
+    let data = List.map (fun (univ, arity, implfs, fields) -> (univ, arity, List.map map implfs, fields)) data in
+    let map (univ, arity, implfs, fields) (is_coe, id, _, cfs, idbuild, _) =
       let coe = List.map (fun (_, { rf_subclass ; rf_canonical }) ->
           { pf_subclass = not (Option.is_empty rf_subclass);
             pf_canonical = rf_canonical })
           cfs
       in
-      id.CAst.v, idbuild, arity, implfs, fields, is_coe, coe
+      id.CAst.v, idbuild, univ, arity, implfs, fields, is_coe, coe
     in
     let data = List.map2 map data records in
     let inds = declare_structure ~cumulative finite ubinders univs implpars params template data in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 4ae9d6d54f..6180ab0821 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -606,6 +606,24 @@ let vernac_assumption ~atts discharge kind l nl =
             | DeclareDef.Discharge -> Dumpglob.dump_definition lid true "var") idl) l;
   ComAssumption.do_assumptions ~poly:atts.polymorphic ~program_mode:atts.program ~scope ~kind nl l
 
+let set_template_check b =
+ let typing_flags = Environ.typing_flags (Global.env ()) in
+ Global.set_typing_flags { typing_flags with Declarations.check_template = b }
+
+let is_template_check () =
+  let typing_flags = Environ.typing_flags (Global.env ()) in
+  typing_flags.Declarations.check_template
+
+let () =
+  let tccheck =
+    { optdepr = true;
+      optname = "Template universe check";
+      optkey = ["Template"; "Check"];
+      optread = (fun () -> is_template_check ());
+      optwrite = (fun b -> set_template_check b)}
+  in
+    declare_bool_option tccheck
+
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
     ~name:"Polymorphic inductive cumulativity"
@@ -2538,7 +2556,7 @@ let rec translate_vernac ~atts v = let open Vernacextend in match v with
     VtDefault(fun () ->
         vernac_hints ~atts dbnames hints)
   | VernacSyntacticDefinition (id,c,b) ->
-    VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
+     VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
   | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
     VtDefault(fun () ->
         with_section_locality ~atts (vernac_arguments qid args more_implicits nargs bidi flags))