Merge PR coq#19254: Stricter conditions for template polymorphic levels

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>

kernel/indTyping.ml

@@ -259,8 +259,8 @@ let check_record data =
 let unbounded_from_below u cstrs =
   Univ.Constraints.for_all (fun (l, d, r) ->
       match d with
-      | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
-      | Lt | Le -> not (Univ.Level.equal r u))
+      | Eq | Lt -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+      | Le -> not (Univ.Level.equal r u))
     cstrs
 
 let get_arity c =
@@ -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

@@ -401,8 +401,8 @@ let template_polymorphic_univs ~ctor_levels uctx paramsctxt u =
     let open Univ in
     Univ.Constraints.for_all (fun (l, d, r) ->
         match d with
-        | Eq -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
-        | Lt | Le -> not (Univ.Level.equal r u))
+        | Eq | Lt -> not (Univ.Level.equal l u) && not (Univ.Level.equal r u)
+        | Le -> not (Univ.Level.equal r u))
       cstrs
   in
   let fold_params accu decl = match decl with
@@ -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