From 1518127d797bd3a33aa8b7397321d07c35bbe3bc Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 10 Dec 2025 10:24:44 -0500 Subject: [PATCH] fix negation logic --- crates/ty_python_semantic/src/types.rs | 14 ++++++++-- .../src/types/constraints.rs | 26 ++++++++++++++----- .../src/types/infer/builder.rs | 21 ++++++--------- 3 files changed, 39 insertions(+), 22 deletions(-) diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index d0efb0db19..74818fef22 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1268,8 +1268,14 @@ 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(_)) + /// Returns whether this is a "real" intersection type. (Negated types are represented by an + /// intersection containing a single negative branch, which this method does _not_ consider a + /// "real" intersection.) + pub(crate) fn is_nontrivial_intersection(self, db: &'db dyn Db) -> bool { + match self { + Type::Intersection(intersection) => !intersection.is_simple_negation(db), + _ => false, + } } pub(crate) const fn as_function_literal(self) -> Option> { @@ -14123,6 +14129,10 @@ impl<'db> IntersectionType<'db> { (self.positive(db).len() + self.negative(db).len()) == 1 } + pub(crate) fn is_simple_negation(self, db: &'db dyn Db) -> bool { + self.positive(db).len() == 0 && self.negative(db).len() == 1 + } + fn heap_size((positive, negative): &(FxOrderSet>, FxOrderSet>)) -> usize { ruff_memory_usage::order_set_heap_size(positive) + ruff_memory_usage::order_set_heap_size(negative) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 7a727f3285..4f5829fe3f 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -435,6 +435,11 @@ impl<'db> ConstraintSet<'db> { pub(crate) fn display(self, db: &'db dyn Db) -> impl Display { self.node.simplify_for_display(db).display(db) } + + #[expect(dead_code)] // Keep this around for debugging purposes + pub(crate) fn display_graph(self, db: &'db dyn Db, prefix: &dyn Display) -> impl Display { + self.node.display_graph(db, prefix) + } } impl From for ConstraintSet<'_> { @@ -498,11 +503,13 @@ impl<'db> ConstrainedTypeVar<'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: + // be a union type. Because the following equivalences hold, we can break these bounds + // apart and create an equivalent BDD with more nodes but simpler constraints. (Fewer, + // simpler constraints mean that our sequent maps won't grow pathologically large.) // - // T ≤ α & β ⇒ (T ≤ α) ∧ (T ≤ β) - // T ≤ α & ¬β ⇒ (T ≤ α) ∧ ¬(T ≤ β) - // α | β ≤ T ⇒ (α ≤ T) ∧ (β ≤ T) + // T ≤ (α & β) ⇔ (T ≤ α) ∧ (T ≤ β) + // T ≤ (¬α & ¬β) ⇔ (T ≤ ¬α) ∧ (T ≤ ¬β) + // (α | β) ≤ T ⇔ (α ≤ T) ∧ (β ≤ T) if let Type::Union(lower_union) = lower { let mut result = Node::AlwaysTrue; for lower_element in lower_union.elements(db) { @@ -513,7 +520,12 @@ impl<'db> ConstrainedTypeVar<'db> { } return result; } - if let Type::Intersection(upper_intersection) = upper { + // A negated type ¬α is represented as an intersection with no positive elements, and a + // single negative element. We _don't_ want to treat that an "intersection" for the + // purposes of simplifying upper bounds. + if let Type::Intersection(upper_intersection) = upper + && !upper_intersection.is_simple_negation(db) + { let mut result = Node::AlwaysTrue; for upper_element in upper_intersection.iter_positive(db) { result = result.and( @@ -524,7 +536,7 @@ impl<'db> ConstrainedTypeVar<'db> { for upper_element in upper_intersection.iter_negative(db) { result = result.and( db, - ConstrainedTypeVar::new_node(db, typevar, lower, upper_element).negate(db), + ConstrainedTypeVar::new_node(db, typevar, lower, upper_element.negate(db)), ); } return result; @@ -716,7 +728,7 @@ impl<'db> ConstrainedTypeVar<'db> { return IntersectionResult::Disjoint; } - if lower.is_union() || upper.is_intersection() { + if lower.is_union() || upper.is_nontrivial_intersection(db) { return IntersectionResult::CannotSimplify; } diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs index 06cb805c15..5c733454a0 100644 --- a/crates/ty_python_semantic/src/types/infer/builder.rs +++ b/crates/ty_python_semantic/src/types/infer/builder.rs @@ -10844,19 +10844,14 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> { ( Type::KnownInstance(KnownInstanceType::ConstraintSet(left)), Type::KnownInstance(KnownInstanceType::ConstraintSet(right)), - ) => { - let result = match op { - ast::CmpOp::Eq => Some( - left.constraints(self.db()).iff(self.db(), right.constraints(self.db())) - ), - ast::CmpOp::NotEq => Some( - left.constraints(self.db()).iff(self.db(), right.constraints(self.db())).negate(self.db()) - ), - _ => None, - }; - result.map(|constraints| Ok(Type::KnownInstance(KnownInstanceType::ConstraintSet( - TrackedConstraintSet::new(self.db(), constraints) - )))) + ) => match op { + ast::CmpOp::Eq => Some(Ok(Type::BooleanLiteral( + left.constraints(self.db()).iff(self.db(), right.constraints(self.db())).is_always_satisfied(self.db()), + ))), + ast::CmpOp::NotEq => Some(Ok(Type::BooleanLiteral( + !left.constraints(self.db()).iff(self.db(), right.constraints(self.db())).is_always_satisfied(self.db()), + ))), + _ => None, } (