Forbid inflationary universes to be template polymorphic.

Template inductive types with a signature Type@{u} -> Type@{u+1} allowed
to make the algebraic increment to increase arbitrarily. Despite being
a very weak invariant, most parts of the code expect at most a +1 increment
in algebraic universes. We prevent a source of generation of such ill-formed
algebraic types by forbidding template polymorphic arities to return a +n
on a template universe.

Fixes coq#19230: Anomaly with explicit universe +1 and template polymorphism.

kernel/indTyping.ml

@@ -273,12 +273,12 @@ let get_arity c =
     end
   | _ -> None
 
-let get_template univs ~env_params ~env_ar_par ~params entries =
+let get_template univs ~env_params ~env_ar_par ~params entries data =
   match univs with
   | Polymorphic_ind_entry _ | Monomorphic_ind_entry -> None
   | Template_ind_entry ctx ->
-    let entry = match entries with
-      | [entry] -> entry
+    let entry, sort = match entries, data with
+      | [entry], [(_, _, info)] -> entry, info.ind_univ
       | _ -> CErrors.user_err Pp.(str "Template-polymorphism not allowed with mutual inductives.")
     in
     (* Compute potential template parameters *)
@@ -298,6 +298,10 @@ let get_template univs ~env_params ~env_ar_par ~params entries =
        algebraic universe. A reasonable approximation is to restrict their
        appearance to the sort of arities from parameters.
 
+       Furthermore, to prevent the generation of algebraic levels with increments
+       strictly larger than 1, we must also forbid the return sort to contain
+       a positive increment on a template level, see #19230.
+
        TODO: when algebraic universes land, remove this check. *)
     let plevels =
       let fold plevels c = Level.Set.diff plevels (Vars.universes_of_constr c) in
@@ -317,6 +321,13 @@ let get_template univs ~env_params ~env_ar_par ~params entries =
       let plevels = List.fold_left fold plevels entry.mind_entry_lc in
       plevels
     in
+    let plevels = match sort with
+    | Type u ->
+      let fold accu (l, n) = if Int.equal n 0 then accu else Level.Set.remove l accu in
+      List.fold_left fold plevels (Universe.repr u)
+    | Prop | SProp | Set -> plevels
+    | QSort _ -> assert false
+    in
     let map = function
     | None -> None
     | Some l -> if Level.Set.mem l plevels then Some l else None
@@ -462,7 +473,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) =
         Some variances
   in
 
-  let template = get_template mie.mind_entry_universes ~env_params ~env_ar_par ~params mie.mind_entry_inds in
+  let template = get_template mie.mind_entry_universes ~env_params ~env_ar_par ~params mie.mind_entry_inds data in
 
   (* Abstract universes *)
   let usubst, univs = match mie.mind_entry_universes with

test-suite/bugs/bug_19230.v

@@ -0,0 +1,3 @@
+(* This inductive cannot be template *)
+Inductive foo@{u} (A:Type@{u}) : Type@{u+1} := .
+Fail Check foo (foo (foo nat)).

vernac/comInductive.ml

@@ -415,16 +415,17 @@ let template_polymorphic_univs ~ctor_levels uctx paramsctxt u =
   | LocalDef _ -> accu
   in
   let paramslevels = List.fold_left fold_params Univ.Level.Set.empty paramsctxt in
-  let check_level l =
+  let check_level (l, n) =
+    Int.equal n 0 &&
     Univ.Level.Set.mem l (Univ.ContextSet.levels uctx) &&
     Univ.Level.Set.mem l paramslevels &&
     (let () = assert (not @@ Univ.Level.is_set l) in true) &&
     unbounded_from_below l (Univ.ContextSet.constraints uctx) &&
     not (Univ.Level.Set.mem l ctor_levels)
   in
-  let univs = Univ.Universe.levels u in
-  let univs = Univ.Level.Set.filter (fun l -> check_level l) univs in
-  univs
+  let univs = Univ.Universe.repr u in
+  let univs = List.filter check_level univs in
+  List.fold_left (fun accu (l, _) -> Univ.Level.Set.add l accu) Univ.Level.Set.empty univs
 
 let template_polymorphism_candidate uctx params entry template_syntax = match template_syntax with
 | SyntaxNoTemplatePoly -> Univ.Level.Set.empty