[ty] Change to BDD representation for constraint sets (#20533)

While working on #20093, I kept running into test failures due to
constraint sets not simplifying as much as they could, and therefore not
being easily testable against "always true" and "always false".

This PR updates our constraint set representation to use BDDs. Because
BDDs are reduced and ordered, they are canonical — equivalent boolean
formulas are represented by the same interned BDD node.

That said, there is a wrinkle, in that the "variables" that we use in
these BDDs — the individual constraints like `Lower ≤ T ≤ Upper` are not
always independent of each other.

As an example, given types `A ≤ B ≤ C ≤ D` and a typevar `T`, the
constraints `A ≤ T ≤ C` and `B ≤ T ≤ D` "overlap" — their intersection
is non-empty. So we should be able to simplify

```
(A ≤ T ≤ C) ∧ (B ≤ T ≤ D) == (B ≤ T ≤ C)
```

That's not a simplification that the BDD structure can perform itself,
since those three constraints are modeled as separate BDD variables, and
are therefore "opaque" to the BDD algorithms.

That means we need to perform this kind of simplification ourselves. We
look at pairs of constraints that appear in a BDD and see if they can be
simplified relative to each other, and if so, replace the pair with the
simplification. A large part of the toil of getting this PR to work was
identifying all of those patterns and getting that substitution logic
correct.

With this new representation, all existing tests pass, as well as some
new ones that represent test failures that were occuring on #20093.

---------

Co-authored-by: Carl Meyer <carl@astral.sh>

crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md

@@ -305,9 +305,9 @@ range.
 
 ```py
 def _[T]() -> None:
-    # revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Base) ∧ ¬(Sub ≤ T@_ ≤ Base))]
+    # revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ (SubSub ≤ T@_ ≤ Base))]
     reveal_type(range_constraint(SubSub, T, Base) & negated_range_constraint(Sub, T, Super))
-    # revealed: ty_extensions.ConstraintSet[((SubSub ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))]
+    # revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ (SubSub ≤ T@_ ≤ Super))]
     reveal_type(range_constraint(SubSub, T, Super) & negated_range_constraint(Sub, T, Base))
 ```
 
@@ -339,9 +339,9 @@ Otherwise, the union cannot be simplified.
 
 ```py
 def _[T]() -> None:
-    # revealed: ty_extensions.ConstraintSet[(¬(Sub ≤ T@_ ≤ Base) ∧ ¬(Base ≤ T@_ ≤ Super))]
+    # revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(Sub ≤ T@_ ≤ Base))]
     reveal_type(negated_range_constraint(Sub, T, Base) & negated_range_constraint(Base, T, Super))
-    # revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Base ≤ T@_ ≤ Super))]
+    # revealed: ty_extensions.ConstraintSet[(¬(Base ≤ T@_ ≤ Super) ∧ ¬(SubSub ≤ T@_ ≤ Sub))]
     reveal_type(negated_range_constraint(SubSub, T, Sub) & negated_range_constraint(Base, T, Super))
     # revealed: ty_extensions.ConstraintSet[(¬(SubSub ≤ T@_ ≤ Sub) ∧ ¬(Unrelated ≤ T@_))]
     reveal_type(negated_range_constraint(SubSub, T, Sub) & negated_range_constraint(Unrelated, T, object))
@@ -385,7 +385,7 @@ We cannot simplify the union of constraints that refer to different typevars.
 def _[T, U]() -> None:
     # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Sub ≤ U@_ ≤ Base)]
     reveal_type(range_constraint(Sub, T, Base) | range_constraint(Sub, U, Base))
-    # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ T@_ ≤ Base) ∨ ¬(Sub ≤ U@_ ≤ Base)]
+    # revealed: ty_extensions.ConstraintSet[¬(Sub ≤ U@_ ≤ Base) ∨ ¬(Sub ≤ T@_ ≤ Base)]
     reveal_type(negated_range_constraint(Sub, T, Base) | negated_range_constraint(Sub, U, Base))
 ```
 
@@ -417,9 +417,9 @@ Otherwise, the union cannot be simplified.
 
 ```py
 def _[T]() -> None:
-    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ (Base ≤ T@_ ≤ Super)]
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (Sub ≤ T@_ ≤ Base)]
     reveal_type(range_constraint(Sub, T, Base) | range_constraint(Base, T, Super))
-    # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) ∨ (Base ≤ T@_ ≤ Super)]
+    # revealed: ty_extensions.ConstraintSet[(Base ≤ T@_ ≤ Super) ∨ (SubSub ≤ T@_ ≤ Sub)]
     reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Base, T, Super))
     # revealed: ty_extensions.ConstraintSet[(SubSub ≤ T@_ ≤ Sub) ∨ (Unrelated ≤ T@_)]
     reveal_type(range_constraint(SubSub, T, Sub) | range_constraint(Unrelated, T, object))
@@ -488,9 +488,9 @@ range.
 
 ```py
 def _[T]() -> None:
-    # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Base) ∨ (Sub ≤ T@_ ≤ Base)]
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ ¬(SubSub ≤ T@_ ≤ Base)]
     reveal_type(negated_range_constraint(SubSub, T, Base) | range_constraint(Sub, T, Super))
-    # revealed: ty_extensions.ConstraintSet[¬(SubSub ≤ T@_ ≤ Super) ∨ (Sub ≤ T@_ ≤ Base)]
+    # revealed: ty_extensions.ConstraintSet[(Sub ≤ T@_ ≤ Base) ∨ ¬(SubSub ≤ T@_ ≤ Super)]
     reveal_type(negated_range_constraint(SubSub, T, Super) | range_constraint(Sub, T, Base))
 ```
 
@@ -562,3 +562,42 @@ def _[T]() -> None:
     # revealed: ty_extensions.ConstraintSet[always]
     reveal_type(constraint | ~constraint)
 ```
+
+### Negation of constraints involving two variables
+
+```py
+from typing import final, Never
+from ty_extensions import range_constraint
+
+class Base: ...
+
+@final
+class Unrelated: ...
+
+def _[T, U]() -> None:
+    # revealed: ty_extensions.ConstraintSet[¬(U@_ ≤ Base) ∨ ¬(T@_ ≤ Base)]
+    reveal_type(~(range_constraint(Never, T, Base) & range_constraint(Never, U, Base)))
+```
+
+The union of a constraint and its negation should always be satisfiable.
+
+```py
+def _[T, U]() -> None:
+    c1 = range_constraint(Never, T, Base) & range_constraint(Never, U, Base)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(c1 | ~c1)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(~c1 | c1)
+
+    c2 = range_constraint(Unrelated, T, object) & range_constraint(Unrelated, U, object)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(c2 | ~c2)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(~c2 | c2)
+
+    union = c1 | c2
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(union | ~union)
+    # revealed: ty_extensions.ConstraintSet[always]
+    reveal_type(~union | union)
+```

crates/ty_python_semantic/src/types/generics.rs

@@ -877,7 +877,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() {
                 return result;
             }
         }
@@ -918,7 +918,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() {
                 return result;
             }
         }
@@ -928,7 +928,7 @@ impl<'db> Specialization<'db> {
             (None, None) => {}
             (Some(self_tuple), Some(other_tuple)) => {
                 let compatible = self_tuple.is_equivalent_to_impl(db, other_tuple, visitor);
-                if result.intersect(db, &compatible).is_never_satisfied() {
+                if result.intersect(db, compatible).is_never_satisfied() {
                     return result;
                 }
             }

crates/ty_python_semantic/src/types/infer/builder.rs

@@ -6947,7 +6947,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 ast::UnaryOp::Invert,
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(constraints)),
             ) => {
-                let constraints = constraints.constraints(self.db()).clone();
+                let constraints = constraints.constraints(self.db());
                 let result = constraints.negate(self.db());
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(TrackedConstraintSet::new(
                     self.db(),
@@ -7311,9 +7311,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
                 ast::Operator::BitAnd,
             ) => {
-                let left = left.constraints(self.db()).clone();
+                let left = left.constraints(self.db());
-                let right = right.constraints(self.db()).clone();
+                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),
                 )))
@@ -7324,9 +7324,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 Type::KnownInstance(KnownInstanceType::ConstraintSet(right)),
                 ast::Operator::BitOr,
             ) => {
-                let left = left.constraints(self.db()).clone();
+                let left = left.constraints(self.db());
-                let right = right.constraints(self.db()).clone();
+                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),
                 )))

crates/ty_python_semantic/src/types/signatures.rs

@@ -551,10 +551,7 @@ impl<'db> Signature<'db> {
             let self_type = self_type.unwrap_or(Type::unknown());
             let other_type = other_type.unwrap_or(Type::unknown());
             !result
-                .intersect(
+                .intersect(db, self_type.is_equivalent_to_impl(db, other_type, visitor))
-                    db,
-                    &self_type.is_equivalent_to_impl(db, other_type, visitor),
-                )
                 .is_never_satisfied()
         };
 
@@ -699,10 +696,7 @@ impl<'db> Signature<'db> {
             let type1 = type1.unwrap_or(Type::unknown());
             let type2 = type2.unwrap_or(Type::unknown());
             !result
-                .intersect(
+                .intersect(db, type1.has_relation_to_impl(db, type2, relation, visitor))
-                    db,
-                    &type1.has_relation_to_impl(db, type2, relation, visitor),
-                )
                 .is_never_satisfied()
         };
 

crates/ty_python_semantic/src/types/tuple.rs

@@ -439,7 +439,7 @@ impl<'db> FixedLengthTuple<Type<'db>> {
                     let element_constraints =
                         self_ty.has_relation_to_impl(db, *other_ty, relation, visitor);
                     if result
-                        .intersect(db, &element_constraints)
+                        .intersect(db, element_constraints)
                         .is_never_satisfied()
                     {
                         return result;
@@ -452,7 +452,7 @@ impl<'db> FixedLengthTuple<Type<'db>> {
                     let element_constraints =
                         self_ty.has_relation_to_impl(db, *other_ty, relation, visitor);
                     if result
-                        .intersect(db, &element_constraints)
+                        .intersect(db, element_constraints)
                         .is_never_satisfied()
                     {
                         return result;
@@ -774,7 +774,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                     let element_constraints =
                         self_ty.has_relation_to_impl(db, other_ty, relation, visitor);
                     if result
-                        .intersect(db, &element_constraints)
+                        .intersect(db, element_constraints)
                         .is_never_satisfied()
                     {
                         return result;
@@ -788,7 +788,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                     let element_constraints =
                         self_ty.has_relation_to_impl(db, other_ty, relation, visitor);
                     if result
-                        .intersect(db, &element_constraints)
+                        .intersect(db, element_constraints)
                         .is_never_satisfied()
                     {
                         return result;
@@ -832,7 +832,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                             return ConstraintSet::from(false);
                         }
                     };
-                    if result.intersect(db, &pair_constraints).is_never_satisfied() {
+                    if result.intersect(db, pair_constraints).is_never_satisfied() {
                         return result;
                     }
                 }
@@ -858,7 +858,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                             return ConstraintSet::from(false);
                         }
                     };
-                    if result.intersect(db, &pair_constraints).is_never_satisfied() {
+                    if result.intersect(db, pair_constraints).is_never_satisfied() {
                         return result;
                     }
                 }