diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md index f83bee977c..ec4a31a711 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md @@ -126,7 +126,7 @@ strict subtype of the lower bound, a strict supertype of the upper bound, or inc ```py from typing import Any, final, Never, Sequence -from ty_extensions import ConstraintSet, static_assert +from ty_extensions import ConstraintSet, Not, static_assert class Super: ... class Base(Super): ... @@ -207,6 +207,15 @@ def _[T]() -> None: static_assert(constraints == expected) ``` +A negated _type_ is not the same thing as a negated _range_. + +```py +def _[T]() -> None: + negated_type = ConstraintSet.range(Never, T, Not[int]) + negated_constraint = ~ConstraintSet.range(Never, T, int) + static_assert(negated_type != negated_constraint) +``` + ## Intersection The intersection of two constraint sets requires that the constraints in both sets hold. In many diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index 12a38a8e34..be02d27764 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> { @@ -14151,6 +14157,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).is_empty() && 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..289e134324 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; } @@ -1579,7 +1591,6 @@ impl<'db> Node<'db> { /// │ └─₀ never /// └─₀ never /// ``` - #[cfg_attr(not(test), expect(dead_code))] // Keep this around for debugging purposes fn display_graph(self, db: &'db dyn Db, prefix: &dyn Display) -> impl Display { struct DisplayNode<'a, 'db> { db: &'db dyn Db, 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, } (