Merge PR #9918: Fix #9294: critical bug with template polymorphism

Ack-by: JasonGross
Ack-by: SkySkimmer
Ack-by: Zimmi48
Ack-by: herbelin
Ack-by: mattam82
Reviewed-by: ppedrot

8 files changed, 177 insertions, 84 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..98b869d72e 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,36 @@ 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 poly && template then user_err
+              Pp.(strbrk "Template-polymorphism and universe polymorphism are not compatible.");
+          if template && not (template_candidate ()) then
+            user_err Pp.(strbrk "Inductive " ++ Id.print ind.ind_name ++
+                         str" cannot be made template polymorphic.");
           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 e3cffa8523..8fd6bc7eab 100644
--- a/vernac/declareObl.ml
+++ b/vernac/declareObl.ml
@@ -530,7 +530,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 5d153fa8be..da14b6e979 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 11237f3873..831fb53549 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
@@ -345,12 +356,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;
@@ -404,29 +415,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;
@@ -437,7 +452,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;
@@ -454,7 +469,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
@@ -469,7 +484,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. *)
@@ -484,7 +499,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)
@@ -509,18 +524,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
@@ -575,7 +590,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);
@@ -679,24 +694,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))