From c3de8847d59ebac73f192a1415e283b278e30bce Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Fri, 24 Oct 2025 13:37:56 -0400 Subject: [PATCH] [ty] Consider domain of BDD when checking whether always satisfiable (#21050) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit That PR title might be a bit inscrutable. Consider the two constraints `T ≤ bool` and `T ≤ int`. Since `bool ≤ int`, by transitivity `T ≤ bool` implies `T ≤ int`. (Every type that is a subtype of `bool` is necessarily also a subtype of `int`.) That means that `T ≤ bool ∧ T ≰ int` is an impossible combination of constraints, and is therefore not a valid input to any BDD. We say that that assignment is not in the _domain_ of the BDD. The implication `T ≤ bool → T ≤ int` can be rewritten as `T ≰ bool ∨ T ≤ int`. (That's the definition of implication.) If we construct that constraint set in an mdtest, we should get a constraint set that is always satisfiable. Previously, that constraint set would correctly _display_ as `always`, but a `static_assert` on it would fail. The underlying cause is that our `is_always_satisfied` method would only test if the BDD was the `AlwaysTrue` terminal node. `T ≰ bool ∨ T ≤ int` does not simplify that far, because we purposefully keep around those constraints in the BDD structure so that it's easier to compare against other BDDs that reference those constraints. To fix this, we need a more nuanced definition of "always satisfied". Instead of evaluating to `true` for _every_ input, we only need it to evaluate to `true` for every _valid_ input — that is, every input in its domain. --- .../mdtest/type_properties/constraints.md | 35 +++++ crates/ty_python_semantic/src/types.rs | 35 ++--- .../ty_python_semantic/src/types/call/bind.rs | 10 +- crates/ty_python_semantic/src/types/class.rs | 2 +- .../src/types/constraints.rs | 131 +++++++++++++----- .../ty_python_semantic/src/types/generics.rs | 12 +- .../src/types/infer/builder.rs | 17 ++- .../ty_python_semantic/src/types/instance.rs | 4 +- .../src/types/signatures.rs | 4 +- crates/ty_python_semantic/src/types/tuple.rs | 18 ++- .../ty_extensions/ty_extensions.pyi | 2 + 11 files changed, 194 insertions(+), 76 deletions(-) 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 607501a349..65b59a55b4 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md @@ -604,6 +604,8 @@ def _[T, U]() -> None: ## Other simplifications +### Displaying constraint sets + When displaying a constraint set, we transform the internal BDD representation into a DNF formula (i.e., the logical OR of several clauses, each of which is the logical AND of several constraints). This section contains several examples that show that we simplify the DNF formula as much as we can @@ -626,11 +628,44 @@ def f[T, U](): reveal_type((t1 | t2) & (u1 | u2)) ``` +We might simplify a BDD so much that we can no longer see the constraints that we used to construct +it! + +```py +from typing import Never +from ty_extensions import static_assert + +def f[T](): + t_int = range_constraint(Never, T, int) + t_bool = range_constraint(Never, T, bool) + + # `T ≤ bool` implies `T ≤ int`: if a type satisfies the former, it must always satisfy the + # latter. We can turn that into a constraint set, using the equivalence `p → q == ¬p ∨ q`: + implication = ~t_bool | t_int + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(implication) + static_assert(implication) + + # However, because of that implication, some inputs aren't valid: it's not possible for + # `T ≤ bool` to be true and `T ≤ int` to be false. This is reflected in the constraint set's + # "domain", which maps valid inputs to `true` and invalid inputs to `false`. This means that two + # constraint sets that are both always satisfied will not be identical if they have different + # domains! + always = range_constraint(Never, T, object) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(always) + static_assert(always) + static_assert(implication != always) +``` + +### Normalized bounds + The lower and upper bounds of a constraint are normalized, so that we equate unions and intersections whose elements appear in different orders. ```py from typing import Never +from ty_extensions import range_constraint def f[T](): # revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)] diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index d64473ddb6..0d2d7ac866 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1234,7 +1234,7 @@ impl<'db> Type<'db> { self.filter_union(db, |elem| { !elem .when_disjoint_from(db, target, inferable) - .is_always_satisfied() + .is_always_satisfied(db) }) } @@ -1524,7 +1524,7 @@ impl<'db> Type<'db> { /// See [`TypeRelation::Subtyping`] for more details. pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool { self.when_subtype_of(db, target, InferableTypeVars::None) - .is_always_satisfied() + .is_always_satisfied(db) } fn when_subtype_of( @@ -1541,7 +1541,7 @@ impl<'db> Type<'db> { /// See [`TypeRelation::Assignability`] for more details. pub(crate) fn is_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool { self.when_assignable_to(db, target, InferableTypeVars::None) - .is_always_satisfied() + .is_always_satisfied(db) } fn when_assignable_to( @@ -1559,7 +1559,7 @@ impl<'db> Type<'db> { #[salsa::tracked(cycle_initial=is_redundant_with_cycle_initial, heap_size=ruff_memory_usage::heap_size)] pub(crate) fn is_redundant_with(self, db: &'db dyn Db, other: Type<'db>) -> bool { self.has_relation_to(db, other, InferableTypeVars::None, TypeRelation::Redundancy) - .is_always_satisfied() + .is_always_satisfied(db) } fn has_relation_to( @@ -1782,7 +1782,7 @@ impl<'db> Type<'db> { ) }) }) - .is_never_satisfied() => + .is_never_satisfied(db) => { // TODO: The repetition here isn't great, but we really need the fallthrough logic, // where this arm only engages if it returns true (or in the world of constraints, @@ -1925,7 +1925,7 @@ impl<'db> Type<'db> { relation_visitor, disjointness_visitor, ) - .is_never_satisfied() + .is_never_satisfied(db) }) => { // TODO: record the unification constraints @@ -2405,7 +2405,7 @@ impl<'db> Type<'db> { /// [equivalent to]: https://typing.python.org/en/latest/spec/glossary.html#term-equivalent pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool { self.when_equivalent_to(db, other, InferableTypeVars::None) - .is_always_satisfied() + .is_always_satisfied(db) } fn when_equivalent_to( @@ -2528,7 +2528,7 @@ impl<'db> Type<'db> { /// `false` answers in some cases. pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool { self.when_disjoint_from(db, other, InferableTypeVars::None) - .is_always_satisfied() + .is_always_satisfied(db) } fn when_disjoint_from( @@ -4631,7 +4631,7 @@ impl<'db> Type<'db> { Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked_set)) => { let constraints = tracked_set.constraints(db); - Truthiness::from(constraints.is_always_satisfied()) + Truthiness::from(constraints.is_always_satisfied(db)) } Type::FunctionLiteral(_) @@ -7450,7 +7450,6 @@ impl<'db> TypeMapping<'_, 'db> { #[salsa::tracked(debug, heap_size=ruff_memory_usage::heap_size)] #[derive(PartialOrd, Ord)] pub struct TrackedConstraintSet<'db> { - #[returns(ref)] constraints: ConstraintSet<'db>, } @@ -7646,17 +7645,11 @@ impl<'db> KnownInstanceType<'db> { } KnownInstanceType::ConstraintSet(tracked_set) => { let constraints = tracked_set.constraints(self.db); - if constraints.is_always_satisfied() { - f.write_str("ty_extensions.ConstraintSet[always]") - } else if constraints.is_never_satisfied() { - f.write_str("ty_extensions.ConstraintSet[never]") - } else { - write!( - f, - "ty_extensions.ConstraintSet[{}]", - constraints.display(self.db) - ) - } + write!( + f, + "ty_extensions.ConstraintSet[{}]", + constraints.display(self.db) + ) } } } diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs index ef1d8574cb..e6121da055 100644 --- a/crates/ty_python_semantic/src/types/call/bind.rs +++ b/crates/ty_python_semantic/src/types/call/bind.rs @@ -1474,7 +1474,7 @@ impl<'db> CallableBinding<'db> { .unwrap_or(Type::unknown()); if argument_type .when_assignable_to(db, parameter_type, overload.inferable_typevars) - .is_always_satisfied() + .is_always_satisfied(db) { is_argument_assignable_to_any_overload = true; break 'overload; @@ -1707,7 +1707,7 @@ impl<'db> CallableBinding<'db> { current_parameter_type, overload.inferable_typevars, ) - .is_always_satisfied() + .is_always_satisfied(db) { participating_parameter_indexes.insert(parameter_index); } @@ -1830,7 +1830,7 @@ impl<'db> CallableBinding<'db> { first_overload_return_type, overload.inferable_typevars, ) - .is_always_satisfied() + .is_always_satisfied(db) }) } else { // No matching overload @@ -2705,7 +2705,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> { // building them in an earlier separate step. if argument_type .when_assignable_to(self.db, expected_ty, self.inferable_typevars) - .is_never_satisfied() + .is_never_satisfied(self.db) { let positional = matches!(argument, Argument::Positional | Argument::Synthetic) && !parameter.is_variadic(); @@ -2839,7 +2839,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> { KnownClass::Str.to_instance(self.db), self.inferable_typevars, ) - .is_always_satisfied() + .is_always_satisfied(self.db) { self.errors.push(BindingError::InvalidKeyType { argument_index: adjusted_argument_index, diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs index 940679ed17..61c531d17b 100644 --- a/crates/ty_python_semantic/src/types/class.rs +++ b/crates/ty_python_semantic/src/types/class.rs @@ -499,7 +499,7 @@ impl<'db> ClassType<'db> { /// Return `true` if `other` is present in this class's MRO. pub(super) fn is_subclass_of(self, db: &'db dyn Db, other: ClassType<'db>) -> bool { self.when_subclass_of(db, other, InferableTypeVars::None) - .is_always_satisfied() + .is_always_satisfied(db) } pub(super) fn when_subclass_of( diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 832aa71ab2..417399203c 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -98,7 +98,7 @@ pub(crate) trait IteratorConstraintsExtension { /// Returns the constraints under which any element of the iterator holds. /// /// This method short-circuits; if we encounter any element that - /// [`is_always_satisfied`][ConstraintSet::is_always_satisfied] true, then the overall result + /// [`is_always_satisfied`][ConstraintSet::is_always_satisfied], then the overall result /// must be as well, and we stop consuming elements from the iterator. fn when_any<'db>( self, @@ -109,7 +109,7 @@ pub(crate) trait IteratorConstraintsExtension { /// Returns the constraints under which every element of the iterator holds. /// /// This method short-circuits; if we encounter any element that - /// [`is_never_satisfied`][ConstraintSet::is_never_satisfied] true, then the overall result + /// [`is_never_satisfied`][ConstraintSet::is_never_satisfied], then the overall result /// must be as well, and we stop consuming elements from the iterator. fn when_all<'db>( self, @@ -129,7 +129,7 @@ where ) -> ConstraintSet<'db> { let mut result = ConstraintSet::never(); for child in self { - if result.union(db, f(child)).is_always_satisfied() { + if result.union(db, f(child)).is_always_satisfied(db) { return result; } } @@ -143,7 +143,7 @@ where ) -> ConstraintSet<'db> { let mut result = ConstraintSet::always(); for child in self { - if result.intersect(db, f(child)).is_never_satisfied() { + if result.intersect(db, f(child)).is_never_satisfied(db) { return result; } } @@ -176,13 +176,13 @@ impl<'db> ConstraintSet<'db> { } /// Returns whether this constraint set never holds - pub(crate) fn is_never_satisfied(self) -> bool { + pub(crate) fn is_never_satisfied(self, _db: &'db dyn Db) -> bool { self.node.is_never_satisfied() } /// Returns whether this constraint set always holds - pub(crate) fn is_always_satisfied(self) -> bool { - self.node.is_always_satisfied() + pub(crate) fn is_always_satisfied(self, db: &'db dyn Db) -> bool { + self.node.is_always_satisfied(db) } /// Updates this constraint set to hold the union of itself and another constraint set. @@ -208,7 +208,7 @@ impl<'db> ConstraintSet<'db> { /// provided as a thunk, to implement short-circuiting: the thunk is not forced if the /// constraint set is already saturated. pub(crate) fn and(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self { - if !self.is_never_satisfied() { + if !self.is_never_satisfied(db) { self.intersect(db, other()); } self @@ -218,7 +218,7 @@ impl<'db> ConstraintSet<'db> { /// as a thunk, to implement short-circuiting: the thunk is not forced if the constraint set is /// already saturated. pub(crate) fn or(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self { - if !self.is_always_satisfied() { + if !self.is_always_satisfied(db) { self.union(db, other()); } self @@ -247,7 +247,7 @@ impl<'db> ConstraintSet<'db> { } pub(crate) fn display(self, db: &'db dyn Db) -> impl Display { - self.node.display(db) + self.node.simplify(db).display(db) } } @@ -494,8 +494,16 @@ impl<'db> Node<'db> { } /// Returns whether this BDD represent the constant function `true`. - fn is_always_satisfied(self) -> bool { - matches!(self, Node::AlwaysTrue) + fn is_always_satisfied(self, db: &'db dyn Db) -> bool { + match self { + Node::AlwaysTrue => true, + Node::AlwaysFalse => false, + Node::Interior(_) => { + let domain = self.domain(db); + let restricted = self.and(db, domain); + restricted == domain + } + } } /// Returns whether this BDD represent the constant function `false`. @@ -538,6 +546,11 @@ impl<'db> Node<'db> { } } + fn implies(self, db: &'db dyn Db, other: Self) -> Self { + // p → q == ¬p ∨ q + self.negate(db).or(db, other) + } + /// Returns a new BDD that evaluates to `true` when both input BDDs evaluate to the same /// result. fn iff(self, db: &'db dyn Db, other: Self) -> Self { @@ -738,7 +751,21 @@ impl<'db> Node<'db> { fn simplify(self, db: &'db dyn Db) -> Self { match self { Node::AlwaysTrue | Node::AlwaysFalse => self, - Node::Interior(interior) => interior.simplify(db), + Node::Interior(interior) => { + let (simplified, _) = interior.simplify(db); + simplified + } + } + } + + /// Returns the domain (the set of allowed inputs) for a BDD. + fn domain(self, db: &'db dyn Db) -> Self { + match self { + Node::AlwaysTrue | Node::AlwaysFalse => Node::AlwaysTrue, + Node::Interior(interior) => { + let (_, domain) = interior.simplify(db); + domain + } } } @@ -801,10 +828,7 @@ impl<'db> Node<'db> { } } - DisplayNode { - node: self.simplify(db), - db, - } + DisplayNode { node: self, db } } /// Displays the full graph structure of this BDD. `prefix` will be output before each line @@ -1009,8 +1033,14 @@ impl<'db> InteriorNode<'db> { } } + /// Returns a simplified version of a BDD, along with the BDD's domain. + /// + /// Both are calculated by looking at the relationships that exist between the constraints that + /// are mentioned in the BDD. For instance, if one constraint implies another (`x → y`), then + /// `x ∧ ¬y` is not a valid input, and is excluded from the BDD's domain. At the same time, we + /// can rewrite any occurrences of `x ∨ y` into `y`. #[salsa::tracked(heap_size=ruff_memory_usage::heap_size)] - fn simplify(self, db: &'db dyn Db) -> Node<'db> { + fn simplify(self, db: &'db dyn Db) -> (Node<'db>, Node<'db>) { // To simplify a non-terminal BDD, we find all pairs of constraints that are mentioned in // the BDD. If any of those pairs can be simplified to some other BDD, we perform a // substitution to replace the pair with the simplification. @@ -1037,6 +1067,7 @@ impl<'db> InteriorNode<'db> { // Repeatedly pop constraint pairs off of the visit queue, checking whether each pair can // be simplified. let mut simplified = Node::Interior(self); + let mut domain = Node::AlwaysTrue; while let Some((left_constraint, right_constraint)) = to_visit.pop() { // If the constraints refer to different typevars, they trivially cannot be compared. // TODO: We might need to consider when one constraint's upper or lower bound refers to @@ -1056,12 +1087,24 @@ impl<'db> InteriorNode<'db> { None }; if let Some((larger_constraint, smaller_constraint)) = larger_smaller { + let positive_larger_node = + Node::new_satisfied_constraint(db, larger_constraint.when_true()); + let negative_larger_node = + Node::new_satisfied_constraint(db, larger_constraint.when_false()); + + let positive_smaller_node = + Node::new_satisfied_constraint(db, smaller_constraint.when_true()); + + // smaller → larger + let implication = positive_smaller_node.implies(db, positive_larger_node); + domain = domain.and(db, implication); + // larger ∨ smaller = larger simplified = simplified.substitute_union( db, larger_constraint.when_true(), smaller_constraint.when_true(), - Node::new_satisfied_constraint(db, larger_constraint.when_true()), + positive_larger_node, ); // ¬larger ∧ ¬smaller = ¬larger @@ -1069,7 +1112,7 @@ impl<'db> InteriorNode<'db> { db, larger_constraint.when_false(), smaller_constraint.when_false(), - Node::new_satisfied_constraint(db, larger_constraint.when_false()), + negative_larger_node, ); // smaller ∧ ¬larger = false @@ -1111,6 +1154,21 @@ impl<'db> InteriorNode<'db> { let negative_intersection_node = Node::new_satisfied_constraint(db, intersection_constraint.when_false()); + let positive_left_node = + Node::new_satisfied_constraint(db, left_constraint.when_true()); + let negative_left_node = + Node::new_satisfied_constraint(db, left_constraint.when_false()); + + let positive_right_node = + Node::new_satisfied_constraint(db, right_constraint.when_true()); + let negative_right_node = + Node::new_satisfied_constraint(db, right_constraint.when_false()); + + // (left ∧ right) → intersection + let implication = (positive_left_node.and(db, positive_right_node)) + .implies(db, positive_intersection_node); + domain = domain.and(db, implication); + // left ∧ right = intersection simplified = simplified.substitute_intersection( db, @@ -1134,8 +1192,7 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_true(), right_constraint.when_false(), - Node::new_satisfied_constraint(db, left_constraint.when_true()) - .and(db, negative_intersection_node), + positive_left_node.and(db, negative_intersection_node), ); // ¬left ∧ right = ¬intersection ∧ right @@ -1144,8 +1201,7 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_false(), right_constraint.when_true(), - Node::new_satisfied_constraint(db, right_constraint.when_true()) - .and(db, negative_intersection_node), + positive_right_node.and(db, negative_intersection_node), ); // left ∨ ¬right = intersection ∨ ¬right @@ -1155,8 +1211,7 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_true(), right_constraint.when_false(), - Node::new_satisfied_constraint(db, right_constraint.when_false()) - .or(db, positive_intersection_node), + negative_right_node.or(db, positive_intersection_node), ); // ¬left ∨ right = ¬left ∨ intersection @@ -1165,8 +1220,7 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_false(), right_constraint.when_true(), - Node::new_satisfied_constraint(db, left_constraint.when_false()) - .or(db, positive_intersection_node), + negative_left_node.or(db, positive_intersection_node), ); } @@ -1174,6 +1228,16 @@ impl<'db> InteriorNode<'db> { // All of the below hold because we just proved that the intersection of left // and right is empty. + let positive_left_node = + Node::new_satisfied_constraint(db, left_constraint.when_true()); + let positive_right_node = + Node::new_satisfied_constraint(db, right_constraint.when_true()); + + // (left ∧ right) → false + let implication = (positive_left_node.and(db, positive_right_node)) + .implies(db, Node::AlwaysFalse); + domain = domain.and(db, implication); + // left ∧ right = false simplified = simplified.substitute_intersection( db, @@ -1196,7 +1260,7 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_true(), right_constraint.when_false(), - Node::new_constraint(db, left_constraint), + positive_left_node, ); // ¬left ∧ right = right @@ -1205,13 +1269,13 @@ impl<'db> InteriorNode<'db> { db, left_constraint.when_false(), right_constraint.when_true(), - Node::new_constraint(db, right_constraint), + positive_right_node, ); } } } - simplified + (simplified, domain) } } @@ -1459,6 +1523,11 @@ impl<'db> SatisfiedClauses<'db> { while self.simplify_one_round() { // Keep going } + + // We can remove any clauses that have been simplified to the point where they are empty. + // (Clauses are intersections, so an empty clause is `false`, which does not contribute + // anything to the outer union.) + self.clauses.retain(|clause| !clause.constraints.is_empty()); } fn simplify_one_round(&mut self) -> bool { diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs index e8c6305d06..931ec28756 100644 --- a/crates/ty_python_semantic/src/types/generics.rs +++ b/crates/ty_python_semantic/src/types/generics.rs @@ -1179,7 +1179,7 @@ impl<'db> Specialization<'db> { ), TypeVarVariance::Bivariant => ConstraintSet::from(true), }; - if result.intersect(db, compatible).is_never_satisfied() { + if result.intersect(db, compatible).is_never_satisfied(db) { return result; } } @@ -1221,7 +1221,7 @@ impl<'db> Specialization<'db> { } TypeVarVariance::Bivariant => ConstraintSet::from(true), }; - if result.intersect(db, compatible).is_never_satisfied() { + if result.intersect(db, compatible).is_never_satisfied(db) { return result; } } @@ -1232,7 +1232,7 @@ impl<'db> Specialization<'db> { (Some(self_tuple), Some(other_tuple)) => { let compatible = self_tuple.is_equivalent_to_impl(db, other_tuple, inferable, visitor); - if result.intersect(db, compatible).is_never_satisfied() { + if result.intersect(db, compatible).is_never_satisfied(db) { return result; } } @@ -1386,7 +1386,7 @@ impl<'db> SpecializationBuilder<'db> { && !actual.is_never() && actual .when_subtype_of(self.db, formal, self.inferable) - .is_always_satisfied() + .is_always_satisfied(self.db) { return Ok(()); } @@ -1472,7 +1472,7 @@ impl<'db> SpecializationBuilder<'db> { Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { if !ty .when_assignable_to(self.db, bound, self.inferable) - .is_always_satisfied() + .is_always_satisfied(self.db) { return Err(SpecializationError::MismatchedBound { bound_typevar, @@ -1485,7 +1485,7 @@ impl<'db> SpecializationBuilder<'db> { for constraint in constraints.elements(self.db) { if ty .when_assignable_to(self.db, *constraint, self.inferable) - .is_always_satisfied() + .is_always_satisfied(self.db) { self.add_type_mapping(bound_typevar, *constraint); return Ok(()); diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs index 9eae531590..126f1ad557 100644 --- a/crates/ty_python_semantic/src/types/infer/builder.rs +++ b/crates/ty_python_semantic/src/types/infer/builder.rs @@ -8189,7 +8189,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> { ) => { let left = left.constraints(self.db()); let right = right.constraints(self.db()); - let result = left.and(self.db(), || *right); + let result = left.and(self.db(), || right); Some(Type::KnownInstance(KnownInstanceType::ConstraintSet( TrackedConstraintSet::new(self.db(), result), ))) @@ -8202,7 +8202,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> { ) => { let left = left.constraints(self.db()); let right = right.constraints(self.db()); - let result = left.or(self.db(), || *right); + let result = left.or(self.db(), || right); Some(Type::KnownInstance(KnownInstanceType::ConstraintSet( TrackedConstraintSet::new(self.db(), result), ))) @@ -8930,6 +8930,19 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> { })) } + ( + Type::KnownInstance(KnownInstanceType::ConstraintSet(left)), + Type::KnownInstance(KnownInstanceType::ConstraintSet(right)), + ) => match op { + ast::CmpOp::Eq => Some(Ok(Type::BooleanLiteral( + left.constraints(self.db()) == right.constraints(self.db()) + ))), + ast::CmpOp::NotEq => Some(Ok(Type::BooleanLiteral( + left.constraints(self.db()) != right.constraints(self.db()) + ))), + _ => None, + } + ( Type::NominalInstance(nominal1), Type::NominalInstance(nominal2), diff --git a/crates/ty_python_semantic/src/types/instance.rs b/crates/ty_python_semantic/src/types/instance.rs index c8aa42d726..fb1fb5c0a7 100644 --- a/crates/ty_python_semantic/src/types/instance.rs +++ b/crates/ty_python_semantic/src/types/instance.rs @@ -429,7 +429,7 @@ impl<'db> NominalInstanceType<'db> { disjointness_visitor, relation_visitor, ); - if result.union(db, compatible).is_always_satisfied() { + if result.union(db, compatible).is_always_satisfied(db) { return result; } } @@ -659,7 +659,7 @@ impl<'db> ProtocolInstanceType<'db> { &HasRelationToVisitor::default(), &IsDisjointVisitor::default(), ) - .is_always_satisfied() + .is_always_satisfied(db) } fn initial<'db>(_db: &'db dyn Db, _value: ProtocolInstanceType<'db>, _: ()) -> bool { diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs index 26c3aca6a1..b0ff205e48 100644 --- a/crates/ty_python_semantic/src/types/signatures.rs +++ b/crates/ty_python_semantic/src/types/signatures.rs @@ -621,7 +621,7 @@ impl<'db> Signature<'db> { db, self_type.is_equivalent_to_impl(db, other_type, inferable, visitor), ) - .is_never_satisfied() + .is_never_satisfied(db) }; if self.parameters.is_gradual() != other.parameters.is_gradual() { @@ -787,7 +787,7 @@ impl<'db> Signature<'db> { disjointness_visitor, ), ) - .is_never_satisfied() + .is_never_satisfied(db) }; // Return types are covariant. diff --git a/crates/ty_python_semantic/src/types/tuple.rs b/crates/ty_python_semantic/src/types/tuple.rs index fb08672de1..cfb2febce4 100644 --- a/crates/ty_python_semantic/src/types/tuple.rs +++ b/crates/ty_python_semantic/src/types/tuple.rs @@ -477,7 +477,7 @@ impl<'db> FixedLengthTuple> { ); if result .intersect(db, element_constraints) - .is_never_satisfied() + .is_never_satisfied(db) { return result; } @@ -496,7 +496,7 @@ impl<'db> FixedLengthTuple> { ); if result .intersect(db, element_constraints) - .is_never_satisfied() + .is_never_satisfied(db) { return result; } @@ -834,7 +834,7 @@ impl<'db> VariableLengthTuple> { ); if result .intersect(db, element_constraints) - .is_never_satisfied() + .is_never_satisfied(db) { return result; } @@ -854,7 +854,7 @@ impl<'db> VariableLengthTuple> { ); if result .intersect(db, element_constraints) - .is_never_satisfied() + .is_never_satisfied(db) { return result; } @@ -907,7 +907,10 @@ impl<'db> VariableLengthTuple> { return ConstraintSet::from(false); } }; - if result.intersect(db, pair_constraints).is_never_satisfied() { + if result + .intersect(db, pair_constraints) + .is_never_satisfied(db) + { return result; } } @@ -943,7 +946,10 @@ impl<'db> VariableLengthTuple> { return ConstraintSet::from(false); } }; - if result.intersect(db, pair_constraints).is_never_satisfied() { + if result + .intersect(db, pair_constraints) + .is_never_satisfied(db) + { return result; } } diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi index 262ded8867..6c87eb8160 100644 --- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi +++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi @@ -44,6 +44,8 @@ type JustComplex = TypeOf[1.0j] # Constraints class ConstraintSet: def __bool__(self) -> bool: ... + def __eq__(self, other: ConstraintSet) -> bool: ... + def __ne__(self, other: ConstraintSet) -> bool: ... def __and__(self, other: ConstraintSet) -> ConstraintSet: ... def __or__(self, other: ConstraintSet) -> ConstraintSet: ... def __invert__(self) -> ConstraintSet: ...