Skip to content

[ty] Simplify union lower bounds and intersection upper bounds in constraint sets #21871

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
dcreager merged 4 commits into from
Dec 10, 2025
Merged

[ty] Simplify union lower bounds and intersection upper bounds in constraint sets #21871

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
78dc896
simpler bounds
dcreager Dec 9, 2025
eb98a22
reword comment
dcreager Dec 9, 2025
0c71783
clippy
dcreager Dec 9, 2025
4643f3f
describe CannotSimplify results
dcreager Dec 9, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 9 additions & 1 deletion crates/ty_python_semantic/src/types.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1252,7 +1252,7 @@ impl<'db> Type<'db> {
}
}

pub(crate) const fn is_union(&self) -> bool {
pub(crate) const fn is_union(self) -> bool {
matches!(self, Type::Union(_))
}

Expand All @@ -1268,6 +1268,10 @@ impl<'db> Type<'db> {
self.as_union().expect("Expected a Type::Union variant")
}

pub(crate) const fn is_intersection(self) -> bool {
matches!(self, Type::Intersection(_))
}

pub(crate) const fn as_function_literal(self) -> Option<FunctionType<'db>> {
match self {
Type::FunctionLiteral(function_type) => Some(function_type),
Expand Down Expand Up @@ -14109,6 +14113,10 @@ impl<'db> IntersectionType<'db> {
self.positive(db).iter().copied()
}

pub fn iter_negative(self, db: &'db dyn Db) -> impl Iterator<Item = Type<'db>> {
self.negative(db).iter().copied()
}

pub(crate) fn has_one_element(self, db: &'db dyn Db) -> bool {
(self.positive(db).len() + self.negative(db).len()) == 1
}
Expand Down
78 changes: 70 additions & 8 deletions crates/ty_python_semantic/src/types/constraints.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -458,6 +458,19 @@ impl<'db> BoundTypeVarInstance<'db> {
}
}

#[derive(Clone, Copy, Debug)]
enum IntersectionResult<'db> {
Simplified(ConstrainedTypeVar<'db>),
CannotSimplify,
Disjoint,
}

impl IntersectionResult<'_> {
fn is_disjoint(self) -> bool {
matches!(self, IntersectionResult::Disjoint)
}
}

/// An individual constraint in a constraint set. This restricts a single typevar to be within a
/// lower and upper bound.
#[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)]
Expand All @@ -484,6 +497,39 @@ impl<'db> ConstrainedTypeVar<'db> {
debug_assert_eq!(lower, lower.bottom_materialization(db));
debug_assert_eq!(upper, upper.top_materialization(db));

// It's not useful for an upper bound to be an intersection type, or for a lower bound to
// be a union type. Both of those can be rewritten as simpler BDDs:
//
// T ≤ α & β ⇒ (T ≤ α) ∧ (T ≤ β)
// T ≤ α & ¬β ⇒ (T ≤ α) ∧ ¬(T ≤ β)
// α | β ≤ T ⇒ (α ≤ T) ∧ (β ≤ T)
Comment on lines +503 to +505
Copy link
Contributor

@sharkdp sharkdp Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You write these as implications, but don't we need those to be equivalences?

The one about negations looks interesting. I guess it could be simplified to T ≤ ¬β ⇒ ¬(T ≤ β), since the intersection part of it is already covered by the first rule. But more importantly, is this really correct? The left hand side seems to always be true for T = Never, whereas the right hand side seems to always be false for T = Never. That would mean it's not even true as an implication?

Copy link
Member Author

@dcreager dcreager Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The one about negations looks interesting. I guess it could be simplified to T ≤ ¬β ⇒ ¬(T ≤ β), since the intersection part of it is already covered by the first rule. But more importantly, is this really correct? The left hand side seems to always be true for T = Never, whereas the right hand side seems to always be false for T = Never. That would mean it's not even true as an implication?

Ah good catch! Negation doesn't distribute through the check like I wrote it. It should be something like

T ≤ ¬α & ¬β ⇒ (T ≤ ¬α) ∧ (T ≤ ¬β)

i.e. we can still separate out the negation elements of the intersection, but they should remain negated types and a positive ≤ check.

I'll fix this in a follow-on PR.

You write these as implications, but don't we need those to be equivalences?

They are equivalences, but we're using this as a normalization step, so we only want to apply them in the direction that I've written them. That is, the goal with this change is that the upper bound of a constraint will never be an intersection type anymore. (and ditto for the lower bound never being a union type)

Copy link
Contributor

@sharkdp sharkdp Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

You write these as implications, but don't we need those to be equivalences?

They are equivalences, but we're using this as a normalization step, so we only want to apply them in the direction that I've written them. That is, the goal with this change is that the upper bound of a constraint will never be an intersection type anymore. (and ditto for the lower bound never being a union type)

👍

I'm being pedantic, but I think what I meant was: we need these to be equivalences, or otherwise, the structural simplification that we apply here (in one direction) might lead to a constraint set that is not equivalent to the original constraint set anymore. But even if my thinking is correct, there's no need to change anything. The arrows can also just represent the direction in which we're performing the simplification. I mainly wanted to understand.

Copy link
Member Author

@dcreager dcreager Dec 10, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

we need these to be equivalences, or otherwise, the structural simplification that we apply here (in one direction) might lead to a constraint set that is not equivalent to the original constraint set anymore.

Got it! I think I got this meaning correct in the new comment in #21897

if let Type::Union(lower_union) = lower {
let mut result = Node::AlwaysTrue;
for lower_element in lower_union.elements(db) {
result = result.and(
db,
ConstrainedTypeVar::new_node(db, typevar, *lower_element, upper),
);
}
return result;
}
if let Type::Intersection(upper_intersection) = upper {
let mut result = Node::AlwaysTrue;
for upper_element in upper_intersection.iter_positive(db) {
result = result.and(
db,
ConstrainedTypeVar::new_node(db, typevar, lower, upper_element),
);
}
for upper_element in upper_intersection.iter_negative(db) {
result = result.and(
db,
ConstrainedTypeVar::new_node(db, typevar, lower, upper_element).negate(db),
);
}
return result;
}

// Two identical typevars must always solve to the same type, so it is not useful to have
// an upper or lower bound that is the typevar being constrained.
match lower {
Expand Down Expand Up @@ -659,18 +705,22 @@ impl<'db> ConstrainedTypeVar<'db> {
}

/// Returns the intersection of two range constraints, or `None` if the intersection is empty.
fn intersect(self, db: &'db dyn Db, other: Self) -> Option<Self> {
fn intersect(self, db: &'db dyn Db, other: Self) -> IntersectionResult<'db> {
// (s₁ ≤ α ≤ t₁) ∧ (s₂ ≤ α ≤ t₂) = (s₁ ∪ s₂) ≤ α ≤ (t₁ ∩ t₂))
let lower = UnionType::from_elements(db, [self.lower(db), other.lower(db)]);
let upper = IntersectionType::from_elements(db, [self.upper(db), other.upper(db)]);

// If `lower ≰ upper`, then the intersection is empty, since there is no type that is both
// greater than `lower`, and less than `upper`.
if !lower.is_subtype_of(db, upper) {
return None;
return IntersectionResult::Disjoint;
}

Some(Self::new(db, self.typevar(db), lower, upper))
if lower.is_union() || upper.is_intersection() {
return IntersectionResult::CannotSimplify;
}

IntersectionResult::Simplified(Self::new(db, self.typevar(db), lower, upper))
}

fn display(self, db: &'db dyn Db) -> impl Display {
Expand Down Expand Up @@ -2034,7 +2084,7 @@ impl<'db> InteriorNode<'db> {
// constraints is empty, and others that we can make when the intersection is
// non-empty.
match left_constraint.intersect(db, right_constraint) {
Some(intersection_constraint) => {
IntersectionResult::Simplified(intersection_constraint) => {
let intersection_constraint = intersection_constraint.normalized(db);

// If the intersection is non-empty, we need to create a new constraint to
Expand Down Expand Up @@ -2117,7 +2167,11 @@ impl<'db> InteriorNode<'db> {
);
}

None => {
// If the intersection doesn't simplify to a single clause, we shouldn't update the
// BDD.
IntersectionResult::CannotSimplify => {}

IntersectionResult::Disjoint => {
// All of the below hold because we just proved that the intersection of left
// and right is empty.

Expand Down Expand Up @@ -2242,7 +2296,9 @@ impl<'db> ConstraintAssignment<'db> {
(
ConstraintAssignment::Positive(self_constraint),
ConstraintAssignment::Negative(other_constraint),
) => self_constraint.intersect(db, other_constraint).is_none(),
) => self_constraint
.intersect(db, other_constraint)
.is_disjoint(),

// It's theoretically possible for a negative constraint to imply a positive constraint
// if the positive constraint is always satisfied (`Never ≤ T ≤ object`). But we never
Expand Down Expand Up @@ -2686,7 +2742,7 @@ impl<'db> SequentMap<'db> {
}

match left_constraint.intersect(db, right_constraint) {
Some(intersection_constraint) => {
IntersectionResult::Simplified(intersection_constraint) => {
tracing::debug!(
target: "ty_python_semantic::types::constraints::SequentMap",
left = %left_constraint.display(db),
Expand All @@ -2704,7 +2760,13 @@ impl<'db> SequentMap<'db> {
self.add_single_implication(db, intersection_constraint, right_constraint);
self.enqueue_constraint(intersection_constraint);
}
None => {

// The sequent map only needs to include constraints that might appear in a BDD. If the
// intersection does not collapse to a single constraint, then there's no new
// constraint that we need to add to the sequent map.
IntersectionResult::CannotSimplify => {}

IntersectionResult::Disjoint => {
tracing::debug!(
target: "ty_python_semantic::types::constraints::SequentMap",
left = %left_constraint.display(db),
Expand Down
Loading