Skip to content

Commit

Permalink
Merge PR coq#19263: Forbid non-linear template polymorphic universe l…
Browse files Browse the repository at this point in the history
…evels.

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <[email protected]>
  • Loading branch information
coqbot-app[bot] and SkySkimmer authored Jun 25, 2024
2 parents d3e1fff + ed15f2c commit 39157c3
Show file tree
Hide file tree
Showing 3 changed files with 22 additions and 4 deletions.
8 changes: 7 additions & 1 deletion kernel/indTyping.ml
Original file line number Diff line number Diff line change
Expand Up @@ -292,7 +292,13 @@ let get_template univs ~env_params ~env_ar_par ~params entries data =
| LocalDef _ -> None
in
let template_params = List.map_filter map params in
let fold accu u = match u with None -> accu | Some u -> Level.Set.add u accu in
let fold accu u = match u with
| None -> accu
| Some u ->
if Level.Set.mem u accu then
CErrors.user_err Pp.(str "Non-linear template level " ++ Level.raw_pr u)
else Level.Set.add u accu
in
let plevels = List.fold_left fold Level.Set.empty template_params in
(* We must ensure that template levels can be substituted by an arbitrary
algebraic universe. A reasonable approximation is to restrict their
Expand Down
7 changes: 7 additions & 0 deletions test-suite/bugs/bug_19263.v
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
Set Warnings "+no-template-universe".

Fail #[universes(template)]
Inductive sum@{u} (A B : Type@{u}) : Type := inl : A -> sum A B | inr : B -> sum A B.

#[universes(template)]
Inductive sum (A B : Type) : Type := inl : A -> sum A B | inr : B -> sum A B.
11 changes: 8 additions & 3 deletions vernac/comInductive.ml
Original file line number Diff line number Diff line change
Expand Up @@ -408,17 +408,22 @@ let template_polymorphic_univs ~ctor_levels uctx paramsctxt u =
let fold_params accu decl = match decl with
| LocalAssum (_, p) ->
let c = Term.strip_prod_decls p in
let update = function None -> Some 0 | Some n -> Some (n + 1) in
begin match get_arity c with
| Some (_, l) -> Univ.Level.Set.add l accu
| Some (_, l) -> Univ.Level.Map.update l update accu
| None -> accu
end
| LocalDef _ -> accu
in
let paramslevels = List.fold_left fold_params Univ.Level.Set.empty paramsctxt in
let paramslevels = List.fold_left fold_params Univ.Level.Map.empty paramsctxt in
let is_linear l = match Univ.Level.Map.find_opt l paramslevels with
| None -> false
| Some n -> Int.equal n 0
in
let check_level (l, n) =
Int.equal n 0 &&
Univ.Level.Set.mem l (Univ.ContextSet.levels uctx) &&
Univ.Level.Set.mem l paramslevels &&
is_linear l &&
(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)
Expand Down

0 comments on commit 39157c3

Please sign in to comment.