diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index d447c634a621..725e332637bf 100644 --- a/kernel/indTyping.ml +++ b/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 diff --git a/test-suite/bugs/bug_19230.v b/test-suite/bugs/bug_19230.v new file mode 100644 index 000000000000..7b11af84296c --- /dev/null +++ b/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)). diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml index cdfeada2ceef..d85d22131ef6 100644 --- a/vernac/comInductive.ml +++ b/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