From 0a9e55c58459ee250901f351c5f10eddd65b5cfe Mon Sep 17 00:00:00 2001 From: Tomas Diaz Date: Wed, 26 Nov 2025 18:15:46 +0100 Subject: [PATCH 1/2] feat: Remove default elim constraints Type -> s feat: Remove elim constraint Type->s by default fix: Update to have dominance check not be done on same quality Notably, dominance updates between sort variables were not checking if the variables were the same. If both were the same and they were not dominated (e.g. when removing the default Type->s constraint), then it would loop because it would postpone the dominance check. It really doesn't make sense though to update the dominance of a sort variable when adding the reflexive elimination constraint. The dominant will be the same in both cases, and if there is none, then it will be dominated eventually when checking with other sorts. fix: Cleanup delayed_check with sort variables fix: Add Type->s to MaybeSquashed fix: Add elim constraints for projections in non-primitive records chore: Add changelog entry refactor: Use Cmap_env to keep elim constraints from projs --- .../21453-remove-type-to-sorts-Changed.rst | 4 ++ kernel/indTyping.ml | 8 ++- kernel/qGraph.ml | 60 ++++++++++++------- test-suite/success/sort_poly.v | 11 +++- 4 files changed, 58 insertions(+), 25 deletions(-) create mode 100644 doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst diff --git a/doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst b/doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst new file mode 100644 index 000000000000..5b55bc8ed507 --- /dev/null +++ b/doc/changelog/01-kernel/21453-remove-type-to-sorts-Changed.rst @@ -0,0 +1,4 @@ +- **Changed:** + `Type` does not eliminate to every sort by default + (`#21453 `_, + by Tomas Diaz). diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index 72c644c19b56..4e1bb0e9067c 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -135,7 +135,13 @@ let compute_elim_squash ?(is_real_arg=false) env u info = | QSort (q, _), (SProp | Prop) -> if Environ.Internal.is_above_prop env q then info else add_squash (Sorts.quality u) info - | _, _ -> { info with ind_squashed = Some AlwaysSquashed } + | (Type _ | Set), QSort (q, _) -> add_squash (QVar q) info + | SProp, (Prop | Type _ | Set) -> + { info with ind_squashed = Some AlwaysSquashed } + | Prop, (Type _ | Set) -> { info with ind_squashed = Some AlwaysSquashed } + (* These cases should not happen because `eliminates_to` above should be true, + * e.g., Type -> (S)Prop, SProp -> SProp, etc. *) + | (Type _ | Set | SProp | Prop), _ -> assert false let check_context_univs ~ctor env info ctx = let check_one d (info,env) = diff --git a/kernel/qGraph.ml b/kernel/qGraph.ml index 55f3644d23a8..7950f6cf37c4 100644 --- a/kernel/qGraph.ml +++ b/kernel/qGraph.ml @@ -21,7 +21,6 @@ module ElimTable = struct let eliminates_to q q' = match q, q' with - | QConstant QType, _ -> true | QConstant q, QConstant q' -> const_eliminates_to q q' | QVar q, QVar q' -> QVar.equal q q' | (QConstant _ | QVar _), _ -> false @@ -159,11 +158,31 @@ let rec update_dominance g q qv = | Some q' -> update_dominant_if_related g qv q' q in match QMap.find_opt qv g.delayed_check with | None -> g' - | Some qs -> - let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) qs g' in - match g' with - | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check } - | None -> None + | Some delayed_qs -> + (* When two sort variables are `set` to each other, e.g. uState, (q1 <-> q2), without being + dominated, then both delay the domination check of each other: + delayed_check[q1] = {q2} + delayed_check[q2] = {q1} + + When one of them becomes dominated, e.g. q1 dominated by Type, then we need to clear up + any occurrence of it in the delayed check of the other, e.g. remove q1 from delayed_check[q2]. + Otherwise, we end up in a loop. *) + let remove_qv_from_delayed delayed_q delayed_check = + match QMap.find_opt delayed_q delayed_check with + | None -> delayed_check + | Some dqs -> + QMap.set delayed_q (QSet.remove qv dqs) delayed_check + in + let clearup_cyclic_delay graph = + QSet.fold (fun delayed_q acc_graph -> + { acc_graph with delayed_check = remove_qv_from_delayed delayed_q acc_graph.delayed_check }) + delayed_qs graph + in + let g' = Option.map clearup_cyclic_delay g' in + let g' = QSet.fold (fun v g -> Option.bind g (fun g -> update_dominance g q v)) delayed_qs g' in + match g' with + | Some graph -> Some { graph with delayed_check = QMap.set qv QSet.empty g.delayed_check } + | None -> None let update_dominance_if_valid g (q1,k,q2) = match k with @@ -173,6 +192,8 @@ let update_dominance_if_valid g (q1,k,q2) = else match q1, q2 with | (Quality.QConstant _ | Quality.QVar _), Quality.QConstant _ -> assert false + | Quality.QVar qv1, Quality.QVar qv2 when QVar.equal qv1 qv2 -> assert false + (* It makes no sense to update or delay the dominance of a sort variable when it eliminates to itself *) | Quality.QVar qv1, Quality.QVar qv2 -> (* 3 cases: - if [qv1] is a global, treat as constants. @@ -183,7 +204,7 @@ let update_dominance_if_valid g (q1,k,q2) = (match QMap.find_opt qv1 g.dominant with | None -> let add_delayed qs = - Some { g with delayed_check = QMap.set qv1 (QSet.add qv2 qs) g.delayed_check } + Some { g with delayed_check = QMap.add qv1 (QSet.add qv2 qs) g.delayed_check } in (match QMap.find_opt qv1 g.delayed_check with | None -> add_delayed QSet.empty @@ -232,8 +253,9 @@ let enforce_constraint (q1, k, q2) g = if ignore_constraints g then g else let e = lazy (G.get_explanation (q1,to_graph_cstr k,q2) g.graph) in raise @@ EliminationError (QualityInconsistency (None, (k, q1, q2, Some (Path e)))) - | Some g -> - dominance_check g (q1, k, q2) + | Some graph -> + if Quality.equal q1 q2 then graph + else dominance_check graph (q1, k, q2) let merge_constraints csts g = ElimConstraints.fold enforce_constraint csts g @@ -248,16 +270,11 @@ exception AlreadyDeclared = G.AlreadyDeclared let add_quality q g = let graph = G.add q g.graph in - let g = enforce_constraint (Quality.qtype, ElimConstraint.ElimTo, q) { g with graph } in - let (paths,ground_and_global_sorts) = + let ground_and_global_sorts = if Quality.is_qglobal q - then (RigidPaths.add_elim_to Quality.qtype q g.rigid_paths, Quality.Set.add q g.ground_and_global_sorts) - else (g.rigid_paths,g.ground_and_global_sorts) in - (* As Type ~> s, set Type to be the dominant sort of q if q is a variable. *) - let dominant = match q with - | Quality.QVar qv -> QMap.add qv Quality.qtype g.dominant - | Quality.QConstant _ -> g.dominant in - { g with rigid_paths = paths; ground_and_global_sorts; dominant } + then Quality.Set.add q g.ground_and_global_sorts + else g.ground_and_global_sorts in + { g with graph; ground_and_global_sorts } let enforce_eliminates_to s1 s2 g = enforce_constraint (s1, ElimConstraint.ElimTo, s2) g @@ -307,9 +324,10 @@ let merge g g' = (fun q acc -> try add_quality q acc with _ -> acc) qs g in Quality.Set.fold (fun q -> Quality.Set.fold - (fun q' acc -> if eliminates_to g' q q' - then enforce_eliminates_to q q' acc - else acc) qs) qs g + (fun q' acc -> if Quality.equal q q' then acc + else if eliminates_to g' q q' + then enforce_eliminates_to q q' acc + else acc) qs) qs g let is_empty g = QVar.Set.is_empty (qvar_domain g) diff --git a/test-suite/success/sort_poly.v b/test-suite/success/sort_poly.v index d704caac3e51..63fb1f9df2fe 100644 --- a/test-suite/success/sort_poly.v +++ b/test-suite/success/sort_poly.v @@ -213,7 +213,9 @@ Module Inductives. Definition R5f1_sprop (A:SProp) (r:R5 A) : A := let (f) := r in f. Fail Definition R5f1_prop (A:Prop) (r:R5 A) : A := let (f) := r in f. - Record R6@{s; |} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }. + (* This is now invalid since Type does not eliminate to arbitrary sorts by default *) + Fail Record R6@{s; |} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }. + Record R6@{s; |Type->s} (A:Type@{s;Set}) := { R6f1 : A; R6f2 : nat }. Check fun (A:SProp) (x y : R6 A) => eq_refl : Conversion.box _ x.(R6f1 _) = Conversion.box _ y.(R6f1 _). Fail Check fun (A:Prop) (x y : R6 A) => @@ -286,7 +288,10 @@ Module Inductives. Arguments exist3 {_ _}. - Definition π1@{s s';u v|} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A := + (* This is now invalid since Type does not eliminate to arbitrary sorts by default *) + Fail Definition π1@{s s';u v|} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A := match p return A with exist3 a _ => a end. - + Definition π1@{s s';u v|Type -> s} {A:Type@{s;u}} {P:A -> Type@{s';v}} (p : sigma3@{_ _ Type;_ _} A P) : A := + match p return A with exist3 a _ => a end. + (* s s' ; u v |= Type -> s *) End Inductives. From 353549def6359faa8c89d180090fdf1b3c078847 Mon Sep 17 00:00:00 2001 From: Tomas Diaz Date: Wed, 4 Mar 2026 17:17:52 +0100 Subject: [PATCH 2/2] test: Update with examples --- test-suite/output/sort_poly_elab.v | 14 ++++++++++++++ test-suite/success/sort_poly_elim_csts.v | 14 ++++++++++++++ 2 files changed, 28 insertions(+) diff --git a/test-suite/output/sort_poly_elab.v b/test-suite/output/sort_poly_elab.v index 9907f7cdf9ed..f11fcac6b180 100644 --- a/test-suite/output/sort_poly_elab.v +++ b/test-suite/output/sort_poly_elab.v @@ -440,6 +440,13 @@ Module Inductives. (* α α0 ; u |= α -> SProp *) About list_idS. + Fixpoint list_idTS {A : Type} (l : list@{_ Type;_} A) : list A := + match l with + | nil => nil + | cons x l => cons x (list_idTS l) + end. + About list_idTS. + Fixpoint map A B f (l : list A) : list B := match l with | nil => nil @@ -496,6 +503,13 @@ Module Inductives. (* α ; |= α -> Type *) About bool_to_Prop'. + Definition bool_idTS (b : bool@{Type;}) : bool := + match b with + | true => true + | false => false + end. + About bool_idTS. + #[universes(polymorphic=no)] Sort Test. (* Sort variables not instantiated *) diff --git a/test-suite/success/sort_poly_elim_csts.v b/test-suite/success/sort_poly_elim_csts.v index 8d5783a8e690..824bd6801f17 100644 --- a/test-suite/success/sort_poly_elim_csts.v +++ b/test-suite/success/sort_poly_elim_csts.v @@ -192,3 +192,17 @@ Fixpoint list'_idV@{s s0 s';l l'|l <= l', s0 -> s'} {A : Type@{s;l}} (l : List'@ | nil' => nil' | cons' x l => cons' x (list'_idV l) end. + +Inductive bool@{s;} : Type@{s;Set} := true | false. + +Fail Definition bool_idTS@{s;} (b : bool@{Type;}) : bool@{s;} := + match b with + | true => true + | false => false + end. + +Definition bool_idTS@{s;| Type -> s} (b : bool@{Type;}) : bool@{s;} := + match b with + | true => true + | false => false + end.