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<T> {
     /// 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<T> {
     /// 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<Type<'db>> {
                     );
                     if result
                         .intersect(db, element_constraints)
-                        .is_never_satisfied()
+                        .is_never_satisfied(db)
                     {
                         return result;
                     }
@@ -496,7 +496,7 @@ impl<'db> FixedLengthTuple<Type<'db>> {
                     );
                     if result
                         .intersect(db, element_constraints)
-                        .is_never_satisfied()
+                        .is_never_satisfied(db)
                     {
                         return result;
                     }
@@ -834,7 +834,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                     );
                     if result
                         .intersect(db, element_constraints)
-                        .is_never_satisfied()
+                        .is_never_satisfied(db)
                     {
                         return result;
                     }
@@ -854,7 +854,7 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                     );
                     if result
                         .intersect(db, element_constraints)
-                        .is_never_satisfied()
+                        .is_never_satisfied(db)
                     {
                         return result;
                     }
@@ -907,7 +907,10 @@ 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(db)
+                    {
                         return result;
                     }
                 }
@@ -943,7 +946,10 @@ 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(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: ...