diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
index ebf69f7e4e..3064be79d6 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md
@@ -327,6 +327,17 @@ def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
     static_assert(is_subtype_of(U, U | None))
 ```
 
+A bound or constrained typevar in a union with a dynamic type is assignable to the typevar:
+
+```py
+def union_with_dynamic[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None:
+    static_assert(is_assignable_to(T | Any, T))
+    static_assert(is_assignable_to(U | Any, U))
+
+    static_assert(not is_subtype_of(T | Any, T))
+    static_assert(not is_subtype_of(U | Any, U))
+```
+
 And an intersection of a typevar with another type is always a subtype of the TypeVar:
 
 ```py
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index 1afe7cd844..f20412c073 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -39,6 +39,9 @@ use crate::suppression::check_suppressions;
 use crate::types::call::{Binding, Bindings, CallArguments, CallableBinding};
 use crate::types::class::{CodeGeneratorKind, Field};
 pub(crate) use crate::types::class_base::ClassBase;
+use crate::types::constraints::{
+    Constraints, IteratorConstraintsExtension, OptionConstraintsExtension,
+};
 use crate::types::context::{LintDiagnosticGuard, LintDiagnosticGuardBuilder};
 use crate::types::diagnostic::{INVALID_AWAIT, INVALID_TYPE_FORM, UNSUPPORTED_BOOL_CONVERSION};
 pub use crate::types::display::DisplaySettings;
@@ -73,6 +76,7 @@ mod builder;
 mod call;
 mod class;
 mod class_base;
+mod constraints;
 mod context;
 mod cyclic;
 mod diagnostic;
@@ -176,14 +180,14 @@ fn definition_expression_type<'db>(
 pub(crate) type ApplyTypeMappingVisitor<'db> = TypeTransformer<'db, TypeMapping<'db, 'db>>;
 
 /// A [`PairVisitor`] that is used in `has_relation_to` methods.
-pub(crate) type HasRelationToVisitor<'db> = PairVisitor<'db, TypeRelation>;
+pub(crate) type HasRelationToVisitor<'db, C> = PairVisitor<'db, TypeRelation, C>;
 
 /// A [`PairVisitor`] that is used in `is_disjoint_from` methods.
-pub(crate) type IsDisjointVisitor<'db> = PairVisitor<'db, IsDisjoint>;
+pub(crate) type IsDisjointVisitor<'db, C> = PairVisitor<'db, IsDisjoint, C>;
 pub(crate) struct IsDisjoint;
 
 /// A [`PairVisitor`] that is used in `is_equivalent` methods.
-pub(crate) type IsEquivalentVisitor<'db> = PairVisitor<'db, IsEquivalent>;
+pub(crate) type IsEquivalentVisitor<'db, C> = PairVisitor<'db, IsEquivalent, C>;
 pub(crate) struct IsEquivalent;
 
 /// A [`TypeTransformer`] that is used in `normalized` methods.
@@ -1080,7 +1084,7 @@ impl<'db> Type<'db> {
     /// - Converts class-based protocols into synthesized protocols
     #[must_use]
     pub(crate) fn normalized(self, db: &'db dyn Db) -> Self {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     #[must_use]
@@ -1328,6 +1332,10 @@ impl<'db> Type<'db> {
     /// intersection simplification dependent on the order in which elements are added), so we do
     /// not use this more general definition of subtyping.
     pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool {
+        self.when_subtype_of(db, target)
+    }
+
+    fn when_subtype_of<C: Constraints<'db>>(self, db: &'db dyn Db, target: Type<'db>) -> C {
         self.has_relation_to(db, target, TypeRelation::Subtyping)
     }
 
@@ -1335,40 +1343,58 @@ impl<'db> Type<'db> {
     ///
     /// [assignable to]: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation
     pub(crate) fn is_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool {
+        self.when_assignable_to(db, target)
+    }
+
+    fn when_assignable_to<C: Constraints<'db>>(self, db: &'db dyn Db, target: Type<'db>) -> C {
         self.has_relation_to(db, target, TypeRelation::Assignability)
     }
 
-    fn has_relation_to(self, db: &'db dyn Db, target: Type<'db>, relation: TypeRelation) -> bool {
-        self.has_relation_to_impl(db, target, relation, &PairVisitor::new(true))
-    }
-
-    fn has_relation_to_impl(
+    fn has_relation_to<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         target: Type<'db>,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+    ) -> C {
+        self.has_relation_to_impl(
+            db,
+            target,
+            relation,
+            &HasRelationToVisitor::new(C::always_satisfiable(db)),
+        )
+    }
+
+    fn has_relation_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        target: Type<'db>,
+        relation: TypeRelation,
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         // Subtyping implies assignability, so if subtyping is reflexive and the two types are
         // equal, it is both a subtype and assignable. Assignability is always reflexive.
         //
         // Note that we could do a full equivalence check here, but that would be both expensive
         // and unnecessary. This early return is only an optimisation.
         if (relation.is_assignability() || self.subtyping_is_always_reflexive()) && self == target {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         match (self, target) {
             // Everything is a subtype of `object`.
-            (_, Type::NominalInstance(instance)) if instance.is_object(db) => true,
+            (_, Type::NominalInstance(instance)) if instance.is_object(db) => {
+                C::always_satisfiable(db)
+            }
 
             // `Never` is the bottom type, the empty set.
             // It is a subtype of all other types.
-            (Type::Never, _) => true,
+            (Type::Never, _) => C::always_satisfiable(db),
 
             // Dynamic is only a subtype of `object` and only a supertype of `Never`; both were
             // handled above. It's always assignable, though.
-            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => relation.is_assignability(),
+            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => {
+                C::from_bool(db, relation.is_assignability())
+            }
 
             (Type::TypeAlias(self_alias), _) => visitor.visit((self, target), || {
                 self_alias
@@ -1386,12 +1412,14 @@ impl<'db> Type<'db> {
             (Type::KnownInstance(KnownInstanceType::Field(field)), right)
                 if relation.is_assignability() =>
             {
-                field.default_type(db).has_relation_to(db, right, relation)
+                field
+                    .default_type(db)
+                    .has_relation_to_impl(db, right, relation, visitor)
             }
 
             (Type::TypedDict(_), _) | (_, Type::TypedDict(_)) => {
                 // TODO: Implement assignability and subtyping for TypedDict
-                relation.is_assignability()
+                C::from_bool(db, relation.is_assignability())
             }
 
             // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied:
@@ -1405,17 +1433,17 @@ impl<'db> Type<'db> {
             (Type::NonInferableTypeVar(_), Type::Union(union))
                 if union.elements(db).contains(&self) =>
             {
-                true
+                C::always_satisfiable(db)
             }
             (Type::Intersection(intersection), Type::NonInferableTypeVar(_))
                 if intersection.positive(db).contains(&target) =>
             {
-                true
+                C::always_satisfiable(db)
             }
             (Type::Intersection(intersection), Type::NonInferableTypeVar(_))
                 if intersection.negative(db).contains(&target) =>
             {
-                false
+                C::always_satisfiable(db)
             }
 
             // Two identical typevars must always solve to the same type, so they are always
@@ -1426,7 +1454,7 @@ impl<'db> Type<'db> {
             (
                 Type::NonInferableTypeVar(lhs_bound_typevar),
                 Type::NonInferableTypeVar(rhs_bound_typevar),
-            ) if lhs_bound_typevar == rhs_bound_typevar => true,
+            ) if lhs_bound_typevar == rhs_bound_typevar => C::always_satisfiable(db),
 
             // A fully static typevar is a subtype of its upper bound, and to something similar to
             // the union of its constraints. An unbound, unconstrained, fully static typevar has an
@@ -1440,7 +1468,7 @@ impl<'db> Type<'db> {
                         bound.has_relation_to_impl(db, target, relation, visitor)
                     }
                     Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                        constraints.elements(db).iter().all(|constraint| {
+                        constraints.elements(db).iter().when_all(db, |constraint| {
                             constraint.has_relation_to_impl(db, target, relation, visitor)
                         })
                     }
@@ -1451,69 +1479,79 @@ impl<'db> Type<'db> {
             // might be specialized to any one of them. However, the constraints do not have to be
             // disjoint, which means an lhs type might be a subtype of all of the constraints.
             (_, Type::NonInferableTypeVar(bound_typevar))
-                if bound_typevar
+                if !bound_typevar
                     .typevar(db)
                     .constraints(db)
-                    .is_some_and(|constraints| {
-                        constraints.iter().all(|constraint| {
+                    .when_some_and(db, |constraints| {
+                        constraints.iter().when_all(db, |constraint| {
                             self.has_relation_to_impl(db, *constraint, relation, visitor)
                         })
-                    }) =>
+                    })
+                    .is_never_satisfied(db) =>
             {
-                true
+                // 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,
+                // not false). Once we're using real constraint sets instead of bool, we should be
+                // able to simplify the typevar logic.
+                bound_typevar
+                    .typevar(db)
+                    .constraints(db)
+                    .when_some_and(db, |constraints| {
+                        constraints.iter().when_all(db, |constraint| {
+                            self.has_relation_to_impl(db, *constraint, relation, visitor)
+                        })
+                    })
             }
 
             // `Never` is the bottom type, the empty set.
             // Other than one unlikely edge case (TypeVars bound to `Never`),
             // no other type is a subtype of or assignable to `Never`.
-            (_, Type::Never) => false,
+            (_, Type::Never) => C::unsatisfiable(db),
 
-            (Type::Union(union), _) => union
-                .elements(db)
-                .iter()
-                .all(|&elem_ty| elem_ty.has_relation_to_impl(db, target, relation, visitor)),
+            (Type::Union(union), _) => union.elements(db).iter().when_all(db, |&elem_ty| {
+                elem_ty.has_relation_to_impl(db, target, relation, visitor)
+            }),
 
-            (_, Type::Union(union)) => union
-                .elements(db)
-                .iter()
-                .any(|&elem_ty| self.has_relation_to_impl(db, elem_ty, relation, visitor)),
+            (_, Type::Union(union)) => union.elements(db).iter().when_any(db, |&elem_ty| {
+                self.has_relation_to_impl(db, elem_ty, relation, visitor)
+            }),
 
             // If both sides are intersections we need to handle the right side first
             // (A & B & C) is a subtype of (A & B) because the left is a subtype of both A and B,
             // but none of A, B, or C is a subtype of (A & B).
-            (_, Type::Intersection(intersection)) => {
-                intersection
-                    .positive(db)
-                    .iter()
-                    .all(|&pos_ty| self.has_relation_to_impl(db, pos_ty, relation, visitor))
-                    && intersection
+            (_, Type::Intersection(intersection)) => (intersection.positive(db).iter())
+                .when_all(db, |&pos_ty| {
+                    self.has_relation_to_impl(db, pos_ty, relation, visitor)
+                })
+                .and(db, || {
+                    intersection
                         .negative(db)
                         .iter()
-                        .all(|&neg_ty| self.is_disjoint_from(db, neg_ty))
+                        .when_all(db, |&neg_ty| self.when_disjoint_from(db, neg_ty))
+                }),
+            (Type::Intersection(intersection), _) => {
+                intersection.positive(db).iter().when_any(db, |&elem_ty| {
+                    elem_ty.has_relation_to_impl(db, target, relation, visitor)
+                })
             }
 
-            (Type::Intersection(intersection), _) => intersection
-                .positive(db)
-                .iter()
-                .any(|&elem_ty| elem_ty.has_relation_to_impl(db, target, relation, visitor)),
-
             // Other than the special cases checked above, no other types are a subtype of a
             // typevar, since there's no guarantee what type the typevar will be specialized to.
             // (If the typevar is bounded, it might be specialized to a smaller type than the
             // bound. This is true even if the bound is a final class, since the typevar can still
             // be specialized to `Never`.)
-            (_, Type::NonInferableTypeVar(_)) => false,
+            (_, Type::NonInferableTypeVar(_)) => C::unsatisfiable(db),
 
             // TODO: Infer specializations here
-            (Type::TypeVar(_), _) | (_, Type::TypeVar(_)) => false,
+            (Type::TypeVar(_), _) | (_, Type::TypeVar(_)) => C::unsatisfiable(db),
 
             // Note that the definition of `Type::AlwaysFalsy` depends on the return value of `__bool__`.
             // If `__bool__` always returns True or False, it can be treated as a subtype of `AlwaysTruthy` or `AlwaysFalsy`, respectively.
-            (left, Type::AlwaysFalsy) => left.bool(db).is_always_false(),
-            (left, Type::AlwaysTruthy) => left.bool(db).is_always_true(),
+            (left, Type::AlwaysFalsy) => C::from_bool(db, left.bool(db).is_always_false()),
+            (left, Type::AlwaysTruthy) => C::from_bool(db, left.bool(db).is_always_true()),
             // Currently, the only supertype of `AlwaysFalsy` and `AlwaysTruthy` is the universal set (object instance).
             (Type::AlwaysFalsy | Type::AlwaysTruthy, _) => {
-                target.is_equivalent_to(db, Type::object(db))
+                target.when_equivalent_to(db, Type::object(db))
             }
 
             // These clauses handle type variants that include function literals. A function
@@ -1522,13 +1560,13 @@ impl<'db> Type<'db> {
             // applied to the signature. Different specializations of the same function literal are
             // only subtypes of each other if they result in the same signature.
             (Type::FunctionLiteral(self_function), Type::FunctionLiteral(target_function)) => {
-                self_function.has_relation_to(db, target_function, relation)
+                self_function.has_relation_to_impl(db, target_function, relation, visitor)
             }
             (Type::BoundMethod(self_method), Type::BoundMethod(target_method)) => {
-                self_method.has_relation_to(db, target_method, relation)
+                self_method.has_relation_to_impl(db, target_method, relation, visitor)
             }
             (Type::MethodWrapper(self_method), Type::MethodWrapper(target_method)) => {
-                self_method.has_relation_to(db, target_method, relation)
+                self_method.has_relation_to_impl(db, target_method, relation, visitor)
             }
 
             // No literal type is a subtype of any other literal type, unless they are the same
@@ -1550,36 +1588,39 @@ impl<'db> Type<'db> {
                 | Type::FunctionLiteral(_)
                 | Type::ModuleLiteral(_)
                 | Type::EnumLiteral(_),
-            ) => false,
+            ) => C::unsatisfiable(db),
 
             (Type::Callable(self_callable), Type::Callable(other_callable)) => {
-                self_callable.has_relation_to(db, other_callable, relation)
+                self_callable.has_relation_to_impl(db, other_callable, relation, visitor)
             }
 
-            (_, Type::Callable(_)) => self.into_callable(db).is_some_and(|callable| {
+            (_, Type::Callable(_)) => self.into_callable(db).when_some_and(db, |callable| {
                 callable.has_relation_to_impl(db, target, relation, visitor)
             }),
 
             (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
-                left.has_relation_to(db, right, relation)
+                left.has_relation_to_impl(db, right, relation, visitor)
             }
             // A protocol instance can never be a subtype of a nominal type, with the *sole* exception of `object`.
-            (Type::ProtocolInstance(_), _) => false,
+            (Type::ProtocolInstance(_), _) => C::unsatisfiable(db),
             (_, Type::ProtocolInstance(protocol)) => {
-                self.satisfies_protocol(db, protocol, relation)
+                self.satisfies_protocol(db, protocol, relation, visitor)
             }
 
             // All `StringLiteral` types are a subtype of `LiteralString`.
-            (Type::StringLiteral(_), Type::LiteralString) => true,
+            (Type::StringLiteral(_), Type::LiteralString) => C::always_satisfiable(db),
 
             // An instance is a subtype of an enum literal, if it is an instance of the enum class
             // and the enum has only one member.
             (Type::NominalInstance(_), Type::EnumLiteral(target_enum_literal)) => {
                 if target_enum_literal.enum_class_instance(db) != self {
-                    return false;
+                    return C::unsatisfiable(db);
                 }
 
-                is_single_member_enum(db, target_enum_literal.enum_class(db))
+                C::from_bool(
+                    db,
+                    is_single_member_enum(db, target_enum_literal.enum_class(db)),
+                )
             }
 
             // Except for the special `LiteralString` case above,
@@ -1594,7 +1635,7 @@ impl<'db> Type<'db> {
                 | Type::ModuleLiteral(_)
                 | Type::EnumLiteral(_),
                 _,
-            ) => (self.literal_fallback_instance(db)).is_some_and(|instance| {
+            ) => (self.literal_fallback_instance(db)).when_some_and(db, |instance| {
                 instance.has_relation_to_impl(db, target, relation, visitor)
             }),
 
@@ -1602,7 +1643,7 @@ impl<'db> Type<'db> {
             // so it also, for now, just delegates to its instance fallback.
             (Type::FunctionLiteral(_), _) => KnownClass::FunctionType
                 .to_instance(db)
-                .has_relation_to(db, target, relation),
+                .has_relation_to_impl(db, target, relation, visitor),
 
             // The same reasoning applies for these special callable types:
             (Type::BoundMethod(_), _) => KnownClass::MethodType
@@ -1617,23 +1658,21 @@ impl<'db> Type<'db> {
 
             (Type::DataclassDecorator(_) | Type::DataclassTransformer(_), _) => {
                 // TODO: Implement subtyping using an equivalent `Callable` type.
-                false
+                C::unsatisfiable(db)
             }
 
             // `TypeIs` is invariant.
-            (Type::TypeIs(left), Type::TypeIs(right)) => {
-                left.return_type(db).has_relation_to_impl(
-                    db,
-                    right.return_type(db),
-                    relation,
-                    visitor,
-                ) && right.return_type(db).has_relation_to_impl(
-                    db,
-                    left.return_type(db),
-                    relation,
-                    visitor,
-                )
-            }
+            (Type::TypeIs(left), Type::TypeIs(right)) => left
+                .return_type(db)
+                .has_relation_to_impl(db, right.return_type(db), relation, visitor)
+                .and(db, || {
+                    right.return_type(db).has_relation_to_impl(
+                        db,
+                        left.return_type(db),
+                        relation,
+                        visitor,
+                    )
+                }),
 
             // `TypeIs[T]` is a subtype of `bool`.
             (Type::TypeIs(_), _) => KnownClass::Bool
@@ -1641,18 +1680,15 @@ impl<'db> Type<'db> {
                 .has_relation_to_impl(db, target, relation, visitor),
 
             // Function-like callables are subtypes of `FunctionType`
-            (Type::Callable(callable), _)
-                if callable.is_function_like(db)
-                    && KnownClass::FunctionType
-                        .to_instance(db)
-                        .has_relation_to_impl(db, target, relation, visitor) =>
-            {
-                true
+            (Type::Callable(callable), _) if callable.is_function_like(db) => {
+                KnownClass::FunctionType
+                    .to_instance(db)
+                    .has_relation_to_impl(db, target, relation, visitor)
             }
 
-            (Type::Callable(_), _) => false,
+            (Type::Callable(_), _) => C::unsatisfiable(db),
 
-            (Type::BoundSuper(_), Type::BoundSuper(_)) => self.is_equivalent_to(db, target),
+            (Type::BoundSuper(_), Type::BoundSuper(_)) => self.when_equivalent_to(db, target),
             (Type::BoundSuper(_), _) => KnownClass::Super
                 .to_instance(db)
                 .has_relation_to_impl(db, target, relation, visitor),
@@ -1670,7 +1706,7 @@ impl<'db> Type<'db> {
                         visitor,
                     )
                 })
-                .unwrap_or(relation.is_assignability()),
+                .unwrap_or_else(|| C::from_bool(db, relation.is_assignability())),
             (Type::GenericAlias(alias), Type::SubclassOf(target_subclass_ty)) => target_subclass_ty
                 .subclass_of()
                 .into_class()
@@ -1682,7 +1718,7 @@ impl<'db> Type<'db> {
                         visitor,
                     )
                 })
-                .unwrap_or(relation.is_assignability()),
+                .unwrap_or_else(|| C::from_bool(db, relation.is_assignability())),
 
             // This branch asks: given two types `type[T]` and `type[S]`, is `type[T]` a subtype of `type[S]`?
             (Type::SubclassOf(self_subclass_ty), Type::SubclassOf(target_subclass_ty)) => {
@@ -1704,13 +1740,16 @@ impl<'db> Type<'db> {
                 KnownClass::Type
                     .to_instance(db)
                     .has_relation_to_impl(db, other, relation, visitor)
-                    || (relation.is_assignability()
-                        && other.has_relation_to_impl(
-                            db,
-                            KnownClass::Type.to_instance(db),
-                            relation,
-                            visitor,
-                        ))
+                    .or(db, || {
+                        C::from_bool(db, relation.is_assignability()).and(db, || {
+                            other.has_relation_to_impl(
+                                db,
+                                KnownClass::Type.to_instance(db),
+                                relation,
+                                visitor,
+                            )
+                        })
+                    })
             }
 
             // Any `type[...]` type is assignable to `type[Any]`
@@ -1765,7 +1804,7 @@ impl<'db> Type<'db> {
 
             // Other than the special cases enumerated above, `Instance` types and typevars are
             // never subtypes of any other variants
-            (Type::NominalInstance(_) | Type::NonInferableTypeVar(_), _) => false,
+            (Type::NominalInstance(_) | Type::NonInferableTypeVar(_), _) => C::unsatisfiable(db),
         }
     }
 
@@ -1782,27 +1821,37 @@ 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.is_equivalent_to_impl(db, other, &PairVisitor::new(true))
+        self.when_equivalent_to(db, other)
     }
 
-    pub(crate) fn is_equivalent_to_impl(
+    fn when_equivalent_to<C: Constraints<'db>>(self, db: &'db dyn Db, other: Type<'db>) -> C {
+        self.is_equivalent_to_impl(
+            db,
+            other,
+            &IsEquivalentVisitor::new(C::always_satisfiable(db)),
+        )
+    }
+
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Type<'db>,
-        visitor: &IsEquivalentVisitor<'db>,
-    ) -> bool {
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         match (self, other) {
-            (Type::Dynamic(_), Type::Dynamic(_)) => true,
+            (Type::Dynamic(_), Type::Dynamic(_)) => C::always_satisfiable(db),
 
             (Type::SubclassOf(first), Type::SubclassOf(second)) => {
                 match (first.subclass_of(), second.subclass_of()) {
-                    (first, second) if first == second => true,
-                    (SubclassOfInner::Dynamic(_), SubclassOfInner::Dynamic(_)) => true,
-                    _ => false,
+                    (first, second) if first == second => C::always_satisfiable(db),
+                    (SubclassOfInner::Dynamic(_), SubclassOfInner::Dynamic(_)) => {
+                        C::always_satisfiable(db)
+                    }
+                    _ => C::unsatisfiable(db),
                 }
             }
 
@@ -1821,45 +1870,49 @@ impl<'db> Type<'db> {
             }
 
             (Type::NominalInstance(first), Type::NominalInstance(second)) => {
-                first.is_equivalent_to(db, second)
+                first.is_equivalent_to_impl(db, second, visitor)
             }
 
-            (Type::Union(first), Type::Union(second)) => first.is_equivalent_to(db, second),
+            (Type::Union(first), Type::Union(second)) => {
+                first.is_equivalent_to_impl(db, second, visitor)
+            }
 
             (Type::Intersection(first), Type::Intersection(second)) => {
-                first.is_equivalent_to(db, second)
+                first.is_equivalent_to_impl(db, second, visitor)
             }
 
             (Type::FunctionLiteral(self_function), Type::FunctionLiteral(target_function)) => {
-                self_function.is_equivalent_to(db, target_function)
+                self_function.is_equivalent_to_impl(db, target_function, visitor)
             }
             (Type::BoundMethod(self_method), Type::BoundMethod(target_method)) => {
-                self_method.is_equivalent_to(db, target_method)
+                self_method.is_equivalent_to_impl(db, target_method, visitor)
             }
             (Type::MethodWrapper(self_method), Type::MethodWrapper(target_method)) => {
-                self_method.is_equivalent_to(db, target_method)
+                self_method.is_equivalent_to_impl(db, target_method, visitor)
+            }
+            (Type::Callable(first), Type::Callable(second)) => {
+                first.is_equivalent_to_impl(db, second, visitor)
             }
-            (Type::Callable(first), Type::Callable(second)) => first.is_equivalent_to(db, second),
 
             (Type::ProtocolInstance(first), Type::ProtocolInstance(second)) => {
-                first.is_equivalent_to(db, second)
+                first.is_equivalent_to_impl(db, second, visitor)
             }
             (Type::ProtocolInstance(protocol), nominal @ Type::NominalInstance(n))
             | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol)) => {
-                n.is_object(db) && protocol.normalized(db) == nominal
+                C::from_bool(db, n.is_object(db) && protocol.normalized(db) == nominal)
             }
             // An instance of an enum class is equivalent to an enum literal of that class,
             // if that enum has only has one member.
             (Type::NominalInstance(instance), Type::EnumLiteral(literal))
             | (Type::EnumLiteral(literal), Type::NominalInstance(instance)) => {
                 if literal.enum_class_instance(db) != Type::NominalInstance(instance) {
-                    return false;
+                    return C::unsatisfiable(db);
                 }
 
                 let class_literal = instance.class(db).class_literal(db).0;
-                is_single_member_enum(db, class_literal)
+                C::from_bool(db, is_single_member_enum(db, class_literal))
             }
-            _ => false,
+            _ => C::unsatisfiable(db),
         }
     }
 
@@ -1868,40 +1921,44 @@ impl<'db> Type<'db> {
     /// Note: This function aims to have no false positives, but might return
     /// wrong `false` answers in some cases.
     pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool {
-        self.is_disjoint_from_impl(db, other, &PairVisitor::new(false))
+        self.when_disjoint_from(db, other)
     }
 
-    pub(crate) fn is_disjoint_from_impl(
+    fn when_disjoint_from<C: Constraints<'db>>(self, db: &'db dyn Db, other: Type<'db>) -> C {
+        self.is_disjoint_from_impl(db, other, &IsDisjointVisitor::new(C::unsatisfiable(db)))
+    }
+
+    pub(crate) fn is_disjoint_from_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Type<'db>,
-        visitor: &IsDisjointVisitor<'db>,
-    ) -> bool {
-        fn any_protocol_members_absent_or_disjoint<'db>(
+        visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
+        fn any_protocol_members_absent_or_disjoint<'db, C: Constraints<'db>>(
             db: &'db dyn Db,
             protocol: ProtocolInstanceType<'db>,
             other: Type<'db>,
-            visitor: &IsDisjointVisitor<'db>,
-        ) -> bool {
-            protocol.interface(db).members(db).any(|member| {
+            visitor: &IsDisjointVisitor<'db, C>,
+        ) -> C {
+            protocol.interface(db).members(db).when_any(db, |member| {
                 other
                     .member(db, member.name())
                     .place
                     .ignore_possibly_unbound()
-                    .is_none_or(|attribute_type| {
+                    .when_none_or(db, |attribute_type| {
                         member.has_disjoint_type_from(db, attribute_type, visitor)
                     })
             })
         }
 
         match (self, other) {
-            (Type::Never, _) | (_, Type::Never) => true,
+            (Type::Never, _) | (_, Type::Never) => C::always_satisfiable(db),
 
-            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => false,
+            (Type::Dynamic(_), _) | (_, Type::Dynamic(_)) => C::unsatisfiable(db),
 
             (Type::TypedDict(_), _) | (_, Type::TypedDict(_)) => {
                 // TODO: Implement disjointness for TypedDict
-                false
+                C::unsatisfiable(db)
             }
 
             (Type::TypeAlias(alias), _) => {
@@ -1922,44 +1979,44 @@ impl<'db> Type<'db> {
             // be specialized to the same type. (This is an important difference between typevars
             // and `Any`!) Different typevars might be disjoint, depending on their bounds and
             // constraints, which are handled below.
-            (Type::NonInferableTypeVar(self_bound_typevar), Type::NonInferableTypeVar(other_bound_typevar))
-                if self_bound_typevar == other_bound_typevar =>
-            {
-                false
-            }
+            (
+                Type::NonInferableTypeVar(self_bound_typevar),
+                Type::NonInferableTypeVar(other_bound_typevar),
+            ) if self_bound_typevar == other_bound_typevar => C::unsatisfiable(db),
 
             (tvar @ Type::NonInferableTypeVar(_), Type::Intersection(intersection))
             | (Type::Intersection(intersection), tvar @ Type::NonInferableTypeVar(_))
                 if intersection.negative(db).contains(&tvar) =>
             {
-                true
+                C::always_satisfiable(db)
             }
 
             // An unbounded typevar is never disjoint from any other type, since it might be
             // specialized to any type. A bounded typevar is not disjoint from its bound, and is
             // only disjoint from other types if its bound is. A constrained typevar is disjoint
             // from a type if all of its constraints are.
-            (Type::NonInferableTypeVar(bound_typevar), other) | (other, Type::NonInferableTypeVar(bound_typevar)) => {
+            (Type::NonInferableTypeVar(bound_typevar), other)
+            | (other, Type::NonInferableTypeVar(bound_typevar)) => {
                 match bound_typevar.typevar(db).bound_or_constraints(db) {
-                    None => false,
+                    None => C::unsatisfiable(db),
                     Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
                         bound.is_disjoint_from_impl(db, other, visitor)
                     }
-                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => constraints
-                        .elements(db)
-                        .iter()
-                        .all(|constraint| constraint.is_disjoint_from_impl(db, other, visitor)),
+                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
+                        constraints.elements(db).iter().when_all(db, |constraint| {
+                            constraint.is_disjoint_from_impl(db, other, visitor)
+                        })
+                    }
                 }
             }
 
             // TODO: Infer specializations here
-            (Type::TypeVar(_), _)
-            | (_, Type::TypeVar(_)) => false,
+            (Type::TypeVar(_), _) | (_, Type::TypeVar(_)) => C::unsatisfiable(db),
 
             (Type::Union(union), other) | (other, Type::Union(union)) => union
                 .elements(db)
                 .iter()
-                .all(|e| e.is_disjoint_from_impl(db, other, visitor)),
+                .when_all(db, |e| e.is_disjoint_from_impl(db, other, visitor)),
 
             // If we have two intersections, we test the positive elements of each one against the other intersection
             // Negative elements need a positive element on the other side in order to be disjoint.
@@ -1968,11 +2025,13 @@ impl<'db> Type<'db> {
                 self_intersection
                     .positive(db)
                     .iter()
-                    .any(|p| p.is_disjoint_from_impl(db, other, visitor))
-                    || other_intersection
-                        .positive(db)
-                        .iter()
-                        .any(|p: &Type<'_>| p.is_disjoint_from_impl(db, self, visitor))
+                    .when_any(db, |p| p.is_disjoint_from_impl(db, other, visitor))
+                    .or(db, || {
+                        other_intersection
+                            .positive(db)
+                            .iter()
+                            .when_any(db, |p| p.is_disjoint_from_impl(db, self, visitor))
+                    })
             }
 
             (Type::Intersection(intersection), other)
@@ -1980,12 +2039,14 @@ impl<'db> Type<'db> {
                 intersection
                     .positive(db)
                     .iter()
-                    .any(|p| p.is_disjoint_from_impl(db, other, visitor))
+                    .when_any(db, |p| p.is_disjoint_from_impl(db, other, visitor))
                     // A & B & Not[C] is disjoint from C
-                    || intersection
-                        .negative(db)
-                        .iter()
-                        .any(|&neg_ty| other.is_subtype_of(db, neg_ty))
+                    .or(db, || {
+                        intersection
+                            .negative(db)
+                            .iter()
+                            .when_any(db, |&neg_ty| other.when_subtype_of(db, neg_ty))
+                    })
             }
 
             // any single-valued type is disjoint from another single-valued type
@@ -2019,7 +2080,7 @@ impl<'db> Type<'db> {
                 | Type::GenericAlias(..)
                 | Type::SpecialForm(..)
                 | Type::KnownInstance(..)),
-            ) => left != right,
+            ) => C::from_bool(db, left != right),
 
             (
                 Type::SubclassOf(_),
@@ -2048,16 +2109,16 @@ impl<'db> Type<'db> {
                 | Type::WrapperDescriptor(..)
                 | Type::ModuleLiteral(..),
                 Type::SubclassOf(_),
-            ) => true,
+            ) => C::always_satisfiable(db),
 
             (Type::AlwaysTruthy, ty) | (ty, Type::AlwaysTruthy) => {
                 // `Truthiness::Ambiguous` may include `AlwaysTrue` as a subset, so it's not guaranteed to be disjoint.
                 // Thus, they are only disjoint if `ty.bool() == AlwaysFalse`.
-                ty.bool(db).is_always_false()
+                C::from_bool(db, ty.bool(db).is_always_false())
             }
             (Type::AlwaysFalsy, ty) | (ty, Type::AlwaysFalsy) => {
                 // Similarly, they are only disjoint if `ty.bool() == AlwaysTrue`.
-                ty.bool(db).is_always_true()
+                C::from_bool(db, ty.bool(db).is_always_true())
             }
 
             (Type::ProtocolInstance(left), Type::ProtocolInstance(right)) => {
@@ -2065,15 +2126,27 @@ impl<'db> Type<'db> {
             }
 
             (Type::ProtocolInstance(protocol), Type::SpecialForm(special_form))
-            | (Type::SpecialForm(special_form), Type::ProtocolInstance(protocol)) => visitor.visit((self, other), || {
-                any_protocol_members_absent_or_disjoint(db, protocol, special_form.instance_fallback(db), visitor)
-                }),
-
+            | (Type::SpecialForm(special_form), Type::ProtocolInstance(protocol)) => {
+                visitor.visit((self, other), || {
+                    any_protocol_members_absent_or_disjoint(
+                        db,
+                        protocol,
+                        special_form.instance_fallback(db),
+                        visitor,
+                    )
+                })
+            }
 
             (Type::ProtocolInstance(protocol), Type::KnownInstance(known_instance))
-            | (Type::KnownInstance(known_instance), Type::ProtocolInstance(protocol)) => visitor.visit((self, other), || {
-                any_protocol_members_absent_or_disjoint(db, protocol, known_instance.instance_fallback(db), visitor)
-            }),
+            | (Type::KnownInstance(known_instance), Type::ProtocolInstance(protocol)) => visitor
+                .visit((self, other), || {
+                    any_protocol_members_absent_or_disjoint(
+                        db,
+                        protocol,
+                        known_instance.instance_fallback(db),
+                        visitor,
+                    )
+                }),
 
             // The absence of a protocol member on one of these types guarantees
             // that the type will be disjoint from the protocol,
@@ -2112,8 +2185,7 @@ impl<'db> Type<'db> {
                 | Type::ModuleLiteral(..)
                 | Type::GenericAlias(..)
                 | Type::IntLiteral(..)
-                | Type::EnumLiteral(..)
-            ),
+                | Type::EnumLiteral(..)),
                 Type::ProtocolInstance(protocol),
             )
             | (
@@ -2128,55 +2200,65 @@ impl<'db> Type<'db> {
                 | Type::GenericAlias(..)
                 | Type::IntLiteral(..)
                 | Type::EnumLiteral(..)),
-            )  => visitor.visit((self, other), || any_protocol_members_absent_or_disjoint(db, protocol, ty, visitor)),
+            ) => visitor.visit((self, other), || {
+                any_protocol_members_absent_or_disjoint(db, protocol, ty, visitor)
+            }),
 
             // This is the same as the branch above --
             // once guard patterns are stabilised, it could be unified with that branch
             // (<https://github.com/rust-lang/rust/issues/129967>)
             (Type::ProtocolInstance(protocol), nominal @ Type::NominalInstance(n))
             | (nominal @ Type::NominalInstance(n), Type::ProtocolInstance(protocol))
-                if n.class(db).is_final(db) => visitor.visit((self, other), ||
+                if n.class(db).is_final(db) =>
             {
-                any_protocol_members_absent_or_disjoint(db, protocol, nominal, visitor)
-            }),
+                visitor.visit((self, other), || {
+                    any_protocol_members_absent_or_disjoint(db, protocol, nominal, visitor)
+                })
+            }
 
             (Type::ProtocolInstance(protocol), other)
             | (other, Type::ProtocolInstance(protocol)) => visitor.visit((self, other), || {
-                protocol.interface(db).members(db).any(|member| {
-                    matches!(
-                        other.member(db, member.name()).place,
-                        Place::Type(attribute_type, _) if member.has_disjoint_type_from(db, attribute_type, visitor)
-                    )
+                protocol.interface(db).members(db).when_any(db, |member| {
+                    match other.member(db, member.name()).place {
+                        Place::Type(attribute_type, _) => {
+                            member.has_disjoint_type_from(db, attribute_type, visitor)
+                        }
+                        Place::Unbound => C::unsatisfiable(db),
+                    }
                 })
             }),
 
             (Type::SubclassOf(subclass_of_ty), Type::ClassLiteral(class_b))
             | (Type::ClassLiteral(class_b), Type::SubclassOf(subclass_of_ty)) => {
                 match subclass_of_ty.subclass_of() {
-                    SubclassOfInner::Dynamic(_) => false,
-                    SubclassOfInner::Class(class_a) => !class_b.is_subclass_of(db, None, class_a),
+                    SubclassOfInner::Dynamic(_) => C::unsatisfiable(db),
+                    SubclassOfInner::Class(class_a) => {
+                        class_b.when_subclass_of::<C>(db, None, class_a).negate(db)
+                    }
                 }
             }
 
             (Type::SubclassOf(subclass_of_ty), Type::GenericAlias(alias_b))
             | (Type::GenericAlias(alias_b), Type::SubclassOf(subclass_of_ty)) => {
                 match subclass_of_ty.subclass_of() {
-                    SubclassOfInner::Dynamic(_) => false,
-                    SubclassOfInner::Class(class_a) => {
-                        !ClassType::from(alias_b).is_subclass_of(db, class_a)
-                    }
+                    SubclassOfInner::Dynamic(_) => C::unsatisfiable(db),
+                    SubclassOfInner::Class(class_a) => ClassType::from(alias_b)
+                        .when_subclass_of::<C>(db, class_a)
+                        .negate(db),
                 }
             }
 
-            (Type::SubclassOf(left), Type::SubclassOf(right)) => left.is_disjoint_from_impl(db, right),
+            (Type::SubclassOf(left), Type::SubclassOf(right)) => {
+                left.is_disjoint_from_impl(db, right, visitor)
+            }
 
             // for `type[Any]`/`type[Unknown]`/`type[Todo]`, we know the type cannot be any larger than `type`,
             // so although the type is dynamic we can still determine disjointedness in some situations
             (Type::SubclassOf(subclass_of_ty), other)
             | (other, Type::SubclassOf(subclass_of_ty)) => match subclass_of_ty.subclass_of() {
-                SubclassOfInner::Dynamic(_) => {
-                    KnownClass::Type.to_instance(db).is_disjoint_from_impl(db, other, visitor)
-                }
+                SubclassOfInner::Dynamic(_) => KnownClass::Type
+                    .to_instance(db)
+                    .is_disjoint_from_impl(db, other, visitor),
                 SubclassOfInner::Class(class) => class
                     .metaclass_instance_type(db)
                     .is_disjoint_from_impl(db, other, visitor),
@@ -2184,78 +2266,93 @@ impl<'db> Type<'db> {
 
             (Type::SpecialForm(special_form), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::SpecialForm(special_form)) => {
-                !special_form.is_instance_of(db, instance.class(db))
+                C::from_bool(db, !special_form.is_instance_of(db, instance.class(db)))
             }
 
             (Type::KnownInstance(known_instance), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::KnownInstance(known_instance)) => {
-                !known_instance.is_instance_of(db, instance.class(db))
+                C::from_bool(db, !known_instance.is_instance_of(db, instance.class(db)))
             }
 
             (Type::BooleanLiteral(..) | Type::TypeIs(_), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::BooleanLiteral(..) | Type::TypeIs(_)) => {
                 // A `Type::BooleanLiteral()` must be an instance of exactly `bool`
                 // (it cannot be an instance of a `bool` subclass)
-                !KnownClass::Bool.is_subclass_of(db, instance.class(db))
+                KnownClass::Bool
+                    .when_subclass_of::<C>(db, instance.class(db))
+                    .negate(db)
             }
 
             (Type::BooleanLiteral(..) | Type::TypeIs(_), _)
-            | (_, Type::BooleanLiteral(..) | Type::TypeIs(_)) => true,
+            | (_, Type::BooleanLiteral(..) | Type::TypeIs(_)) => C::always_satisfiable(db),
 
             (Type::IntLiteral(..), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::IntLiteral(..)) => {
                 // A `Type::IntLiteral()` must be an instance of exactly `int`
                 // (it cannot be an instance of an `int` subclass)
-                !KnownClass::Int.is_subclass_of(db, instance.class(db))
+                KnownClass::Int
+                    .when_subclass_of::<C>(db, instance.class(db))
+                    .negate(db)
             }
 
-            (Type::IntLiteral(..), _) | (_, Type::IntLiteral(..)) => true,
+            (Type::IntLiteral(..), _) | (_, Type::IntLiteral(..)) => C::always_satisfiable(db),
 
             (Type::StringLiteral(..), Type::LiteralString)
-            | (Type::LiteralString, Type::StringLiteral(..)) => false,
+            | (Type::LiteralString, Type::StringLiteral(..)) => C::unsatisfiable(db),
 
             (Type::StringLiteral(..) | Type::LiteralString, Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::StringLiteral(..) | Type::LiteralString) => {
                 // A `Type::StringLiteral()` or a `Type::LiteralString` must be an instance of exactly `str`
                 // (it cannot be an instance of a `str` subclass)
-                !KnownClass::Str.is_subclass_of(db, instance.class(db))
+                KnownClass::Str
+                    .when_subclass_of::<C>(db, instance.class(db))
+                    .negate(db)
             }
 
-            (Type::LiteralString, Type::LiteralString) => false,
-            (Type::LiteralString, _) | (_, Type::LiteralString) => true,
+            (Type::LiteralString, Type::LiteralString) => C::unsatisfiable(db),
+            (Type::LiteralString, _) | (_, Type::LiteralString) => C::always_satisfiable(db),
 
             (Type::BytesLiteral(..), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::BytesLiteral(..)) => {
                 // A `Type::BytesLiteral()` must be an instance of exactly `bytes`
                 // (it cannot be an instance of a `bytes` subclass)
-                !KnownClass::Bytes.is_subclass_of(db, instance.class(db))
+                KnownClass::Bytes
+                    .when_subclass_of::<C>(db, instance.class(db))
+                    .negate(db)
             }
 
-            (Type::EnumLiteral(enum_literal), instance@Type::NominalInstance(_))
-            | (instance@Type::NominalInstance(_), Type::EnumLiteral(enum_literal)) => {
-                !enum_literal.enum_class_instance(db).is_subtype_of(db, instance)
+            (Type::EnumLiteral(enum_literal), instance @ Type::NominalInstance(_))
+            | (instance @ Type::NominalInstance(_), Type::EnumLiteral(enum_literal)) => {
+                enum_literal
+                    .enum_class_instance(db)
+                    .when_subtype_of::<C>(db, instance)
+                    .negate(db)
             }
-            (Type::EnumLiteral(..), _) | (_, Type::EnumLiteral(..)) => true,
+            (Type::EnumLiteral(..), _) | (_, Type::EnumLiteral(..)) => C::always_satisfiable(db),
 
             // A class-literal type `X` is always disjoint from an instance type `Y`,
             // unless the type expressing "all instances of `Z`" is a subtype of of `Y`,
             // where `Z` is `X`'s metaclass.
             (Type::ClassLiteral(class), instance @ Type::NominalInstance(_))
-            | (instance @ Type::NominalInstance(_), Type::ClassLiteral(class)) => !class
+            | (instance @ Type::NominalInstance(_), Type::ClassLiteral(class)) => class
                 .metaclass_instance_type(db)
-                .is_subtype_of(db, instance),
+                .when_subtype_of::<C>(db, instance)
+                .negate(db),
             (Type::GenericAlias(alias), instance @ Type::NominalInstance(_))
             | (instance @ Type::NominalInstance(_), Type::GenericAlias(alias)) => {
-                !ClassType::from(alias)
+                ClassType::from(alias)
                     .metaclass_instance_type(db)
-                    .is_subtype_of(db, instance)
+                    .when_subtype_of::<C>(db, instance)
+                    .negate(db)
             }
 
             (Type::FunctionLiteral(..), Type::NominalInstance(instance))
             | (Type::NominalInstance(instance), Type::FunctionLiteral(..)) => {
                 // A `Type::FunctionLiteral()` must be an instance of exactly `types.FunctionType`
                 // (it cannot be an instance of a `types.FunctionType` subclass)
-                !KnownClass::FunctionType.is_subclass_of(db, instance.class(db))
+                KnownClass::FunctionType
+                    .when_subclass_of::<C>(db, instance.class(db))
+                    .negate(db)
             }
 
             (Type::BoundMethod(_), other) | (other, Type::BoundMethod(_)) => KnownClass::MethodType
@@ -2279,7 +2376,7 @@ impl<'db> Type<'db> {
                 // No two callable types are ever disjoint because
                 // `(*args: object, **kwargs: object) -> Never` is a subtype of all fully static
                 // callable types.
-                false
+                C::unsatisfiable(db)
             }
 
             (Type::Callable(_), Type::StringLiteral(_) | Type::BytesLiteral(_))
@@ -2287,7 +2384,7 @@ impl<'db> Type<'db> {
                 // A callable type is disjoint from other literal types. For example,
                 // `Type::StringLiteral` must be an instance of exactly `str`, not a subclass
                 // of `str`, and `str` is not callable. The same applies to other literal types.
-                true
+                C::always_satisfiable(db)
             }
 
             (Type::Callable(_), Type::SpecialForm(special_form))
@@ -2296,7 +2393,7 @@ impl<'db> Type<'db> {
                 // that are callable (like TypedDict and collection constructors).
                 // Most special forms are type constructors/annotations (like `typing.Literal`,
                 // `typing.Union`, etc.) that are subscripted, not called.
-                !special_form.is_callable()
+                C::from_bool(db, !special_form.is_callable())
             }
 
             (
@@ -2314,8 +2411,10 @@ impl<'db> Type<'db> {
                 )
                 .place
                 .ignore_possibly_unbound()
-                .is_none_or(|dunder_call| {
-                    !dunder_call.is_assignable_to(db, CallableType::unknown(db))
+                .when_none_or(db, |dunder_call| {
+                    dunder_call
+                        .when_assignable_to::<C>(db, CallableType::unknown(db))
+                        .negate(db)
                 }),
 
             (
@@ -2327,7 +2426,7 @@ impl<'db> Type<'db> {
                 Type::Callable(_) | Type::DataclassDecorator(_) | Type::DataclassTransformer(_),
             ) => {
                 // TODO: Implement disjointness for general callable type with other types
-                false
+                C::unsatisfiable(db)
             }
 
             (Type::ModuleLiteral(..), other @ Type::NominalInstance(..))
@@ -2346,7 +2445,9 @@ impl<'db> Type<'db> {
                     .is_disjoint_from_impl(db, other, visitor)
             }
 
-            (Type::BoundSuper(_), Type::BoundSuper(_)) => !self.is_equivalent_to(db, other),
+            (Type::BoundSuper(_), Type::BoundSuper(_)) => {
+                self.when_equivalent_to::<C>(db, other).negate(db)
+            }
             (Type::BoundSuper(_), other) | (other, Type::BoundSuper(_)) => KnownClass::Super
                 .to_instance(db)
                 .is_disjoint_from_impl(db, other, visitor),
@@ -5841,7 +5942,7 @@ impl<'db> Type<'db> {
         db: &'db dyn Db,
         type_mapping: &TypeMapping<'a, 'db>,
     ) -> Type<'db> {
-        self.apply_type_mapping_impl(db, type_mapping, &TypeTransformer::default())
+        self.apply_type_mapping_impl(db, type_mapping, &ApplyTypeMappingVisitor::default())
     }
 
     fn apply_type_mapping_impl<'a>(
@@ -8614,23 +8715,42 @@ impl<'db> BoundMethodType<'db> {
         )
     }
 
-    fn has_relation_to(self, db: &'db dyn Db, other: Self, relation: TypeRelation) -> bool {
+    fn has_relation_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        relation: TypeRelation,
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         // A bound method is a typically a subtype of itself. However, we must explicitly verify
         // the subtyping of the underlying function signatures (since they might be specialized
         // differently), and of the bound self parameter (taking care that parameters, including a
         // bound self parameter, are contravariant.)
         self.function(db)
-            .has_relation_to(db, other.function(db), relation)
-            && other
-                .self_instance(db)
-                .has_relation_to(db, self.self_instance(db), relation)
+            .has_relation_to_impl(db, other.function(db), relation, visitor)
+            .and(db, || {
+                other.self_instance(db).has_relation_to_impl(
+                    db,
+                    self.self_instance(db),
+                    relation,
+                    visitor,
+                )
+            })
     }
 
-    fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
-        self.function(db).is_equivalent_to(db, other.function(db))
-            && other
-                .self_instance(db)
-                .is_equivalent_to(db, self.self_instance(db))
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        self.function(db)
+            .is_equivalent_to_impl(db, other.function(db), visitor)
+            .and(db, || {
+                other
+                    .self_instance(db)
+                    .is_equivalent_to_impl(db, self.self_instance(db), visitor)
+            })
     }
 }
 
@@ -8752,26 +8872,37 @@ impl<'db> CallableType<'db> {
     /// Check whether this callable type has the given relation to another callable type.
     ///
     /// See [`Type::is_subtype_of`] and [`Type::is_assignable_to`] for more details.
-    fn has_relation_to(self, db: &'db dyn Db, other: Self, relation: TypeRelation) -> bool {
+    fn has_relation_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        relation: TypeRelation,
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         if other.is_function_like(db) && !self.is_function_like(db) {
-            return false;
+            return C::unsatisfiable(db);
         }
         self.signatures(db)
-            .has_relation_to(db, other.signatures(db), relation)
+            .has_relation_to_impl(db, other.signatures(db), relation, visitor)
     }
 
     /// Check whether this callable type is equivalent to another callable type.
     ///
     /// See [`Type::is_equivalent_to`] for more details.
-    fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
-        self.is_function_like(db) == other.is_function_like(db)
-            && self
-                .signatures(db)
-                .is_equivalent_to(db, other.signatures(db))
+        C::from_bool(db, self.is_function_like(db) == other.is_function_like(db)).and(db, || {
+            self.signatures(db)
+                .is_equivalent_to_impl(db, other.signatures(db), visitor)
+        })
     }
 }
 
@@ -8821,22 +8952,28 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
 }
 
 impl<'db> MethodWrapperKind<'db> {
-    fn has_relation_to(self, db: &'db dyn Db, other: Self, relation: TypeRelation) -> bool {
+    fn has_relation_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        relation: TypeRelation,
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match (self, other) {
             (
                 MethodWrapperKind::FunctionTypeDunderGet(self_function),
                 MethodWrapperKind::FunctionTypeDunderGet(other_function),
-            ) => self_function.has_relation_to(db, other_function, relation),
+            ) => self_function.has_relation_to_impl(db, other_function, relation, visitor),
 
             (
                 MethodWrapperKind::FunctionTypeDunderCall(self_function),
                 MethodWrapperKind::FunctionTypeDunderCall(other_function),
-            ) => self_function.has_relation_to(db, other_function, relation),
+            ) => self_function.has_relation_to_impl(db, other_function, relation, visitor),
 
             (MethodWrapperKind::PropertyDunderGet(_), MethodWrapperKind::PropertyDunderGet(_))
             | (MethodWrapperKind::PropertyDunderSet(_), MethodWrapperKind::PropertyDunderSet(_))
             | (MethodWrapperKind::StrStartswith(_), MethodWrapperKind::StrStartswith(_)) => {
-                self == other
+                C::from_bool(db, self == other)
             }
 
             (
@@ -8850,26 +8987,31 @@ impl<'db> MethodWrapperKind<'db> {
                 | MethodWrapperKind::PropertyDunderGet(_)
                 | MethodWrapperKind::PropertyDunderSet(_)
                 | MethodWrapperKind::StrStartswith(_),
-            ) => false,
+            ) => C::unsatisfiable(db),
         }
     }
 
-    fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         match (self, other) {
             (
                 MethodWrapperKind::FunctionTypeDunderGet(self_function),
                 MethodWrapperKind::FunctionTypeDunderGet(other_function),
-            ) => self_function.is_equivalent_to(db, other_function),
+            ) => self_function.is_equivalent_to_impl(db, other_function, visitor),
 
             (
                 MethodWrapperKind::FunctionTypeDunderCall(self_function),
                 MethodWrapperKind::FunctionTypeDunderCall(other_function),
-            ) => self_function.is_equivalent_to(db, other_function),
+            ) => self_function.is_equivalent_to_impl(db, other_function, visitor),
 
             (MethodWrapperKind::PropertyDunderGet(_), MethodWrapperKind::PropertyDunderGet(_))
             | (MethodWrapperKind::PropertyDunderSet(_), MethodWrapperKind::PropertyDunderSet(_))
             | (MethodWrapperKind::StrStartswith(_), MethodWrapperKind::StrStartswith(_)) => {
-                self == other
+                C::from_bool(db, self == other)
             }
 
             (
@@ -8883,7 +9025,7 @@ impl<'db> MethodWrapperKind<'db> {
                 | MethodWrapperKind::PropertyDunderGet(_)
                 | MethodWrapperKind::PropertyDunderSet(_)
                 | MethodWrapperKind::StrStartswith(_),
-            ) => false,
+            ) => C::unsatisfiable(db),
         }
     }
 
@@ -9371,7 +9513,7 @@ impl<'db> UnionType<'db> {
     /// See [`Type::normalized`] for more details.
     #[must_use]
     pub(crate) fn normalized(self, db: &'db dyn Db) -> Self {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     pub(crate) fn normalized_impl(self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
@@ -9384,26 +9526,30 @@ impl<'db> UnionType<'db> {
         UnionType::new(db, new_elements.into_boxed_slice())
     }
 
-    /// Return `true` if `self` represents the exact same sets of possible runtime objects as `other`
-    pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        _visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         let self_elements = self.elements(db);
         let other_elements = other.elements(db);
 
         if self_elements.len() != other_elements.len() {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         let sorted_self = self.normalized(db);
 
         if sorted_self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
-        sorted_self == other.normalized(db)
+        C::from_bool(db, sorted_self == other.normalized(db))
     }
 }
 
@@ -9445,7 +9591,7 @@ impl<'db> IntersectionType<'db> {
     /// See [`Type::normalized`] for more details.
     #[must_use]
     pub(crate) fn normalized(self, db: &'db dyn Db) -> Self {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     pub(crate) fn normalized_impl(self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
@@ -9471,32 +9617,37 @@ impl<'db> IntersectionType<'db> {
     }
 
     /// Return `true` if `self` represents exactly the same set of possible runtime objects as `other`
-    pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        _visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         let self_positive = self.positive(db);
         let other_positive = other.positive(db);
 
         if self_positive.len() != other_positive.len() {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         let self_negative = self.negative(db);
         let other_negative = other.negative(db);
 
         if self_negative.len() != other_negative.len() {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         let sorted_self = self.normalized(db);
 
         if sorted_self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
-        sorted_self == other.normalized(db)
+        C::from_bool(db, sorted_self == other.normalized(db))
     }
 
     /// Returns an iterator over the positive elements of the intersection. If
diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
index 49ef66960a..12a38594cb 100644
--- a/crates/ty_python_semantic/src/types/class.rs
+++ b/crates/ty_python_semantic/src/types/class.rs
@@ -18,6 +18,7 @@ use crate::semantic_index::{
     BindingWithConstraints, DeclarationWithConstraint, SemanticIndex, attribute_declarations,
     attribute_scopes,
 };
+use crate::types::constraints::{Constraints, IteratorConstraintsExtension};
 use crate::types::context::InferContext;
 use crate::types::diagnostic::{INVALID_LEGACY_TYPE_VARIABLE, INVALID_TYPE_ALIAS_TYPE};
 use crate::types::enums::enum_metadata;
@@ -28,10 +29,10 @@ use crate::types::signatures::{CallableSignature, Parameter, Parameters, Signatu
 use crate::types::tuple::{TupleSpec, TupleType};
 use crate::types::{
     ApplyTypeMappingVisitor, BareTypeAliasType, Binding, BoundSuperError, BoundSuperType,
-    CallableType, DataclassParams, DeprecatedInstance, HasRelationToVisitor, KnownInstanceType,
-    NormalizedVisitor, PropertyInstanceType, StringLiteralType, TypeAliasType, TypeMapping,
-    TypeRelation, TypeVarBoundOrConstraints, TypeVarInstance, TypeVarKind, VarianceInferable,
-    declaration_type, infer_definition_types, todo_type,
+    CallableType, DataclassParams, DeprecatedInstance, HasRelationToVisitor, IsEquivalentVisitor,
+    KnownInstanceType, NormalizedVisitor, PropertyInstanceType, StringLiteralType, TypeAliasType,
+    TypeMapping, TypeRelation, TypeVarBoundOrConstraints, TypeVarInstance, TypeVarKind,
+    VarianceInferable, declaration_type, infer_definition_types, todo_type,
 };
 use crate::{
     Db, FxIndexMap, FxOrderSet, Program,
@@ -49,7 +50,7 @@ use crate::{
     },
     types::{
         CallArguments, CallError, CallErrorKind, MetaclassCandidate, UnionBuilder, UnionType,
-        cyclic::PairVisitor, definition_expression_type,
+        definition_expression_type,
     },
 };
 use indexmap::IndexSet;
@@ -536,64 +537,88 @@ 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.has_relation_to_impl(db, other, TypeRelation::Subtyping, &PairVisitor::new(true))
+        self.when_subclass_of(db, other)
     }
 
-    pub(super) fn has_relation_to_impl(
+    pub(super) fn when_subclass_of<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: ClassType<'db>,
+    ) -> C {
+        self.has_relation_to_impl(
+            db,
+            other,
+            TypeRelation::Subtyping,
+            &HasRelationToVisitor::new(C::always_satisfiable(db)),
+        )
+    }
+
+    pub(super) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
-        self.iter_mro(db).any(|base| {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
+        self.iter_mro(db).when_any(db, |base| {
             match base {
                 ClassBase::Dynamic(_) => match relation {
-                    TypeRelation::Subtyping => other.is_object(db),
-                    TypeRelation::Assignability => !other.is_final(db),
+                    TypeRelation::Subtyping => C::from_bool(db, other.is_object(db)),
+                    TypeRelation::Assignability => C::from_bool(db, !other.is_final(db)),
                 },
 
                 // Protocol and Generic are not represented by a ClassType.
-                ClassBase::Protocol | ClassBase::Generic => false,
+                ClassBase::Protocol | ClassBase::Generic => C::unsatisfiable(db),
 
                 ClassBase::Class(base) => match (base, other) {
-                    (ClassType::NonGeneric(base), ClassType::NonGeneric(other)) => base == other,
+                    (ClassType::NonGeneric(base), ClassType::NonGeneric(other)) => {
+                        C::from_bool(db, base == other)
+                    }
                     (ClassType::Generic(base), ClassType::Generic(other)) => {
-                        base.origin(db) == other.origin(db)
-                            && base.specialization(db).has_relation_to_impl(
+                        C::from_bool(db, base.origin(db) == other.origin(db)).and(db, || {
+                            base.specialization(db).has_relation_to_impl(
                                 db,
                                 other.specialization(db),
                                 relation,
                                 visitor,
                             )
+                        })
                     }
                     (ClassType::Generic(_), ClassType::NonGeneric(_))
-                    | (ClassType::NonGeneric(_), ClassType::Generic(_)) => false,
+                    | (ClassType::NonGeneric(_), ClassType::Generic(_)) => C::unsatisfiable(db),
                 },
 
                 ClassBase::TypedDict => {
                     // TODO: Implement subclassing and assignability for TypedDicts.
-                    true
+                    C::always_satisfiable(db)
                 }
             }
         })
     }
 
-    pub(super) fn is_equivalent_to(self, db: &'db dyn Db, other: ClassType<'db>) -> bool {
+    pub(super) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: ClassType<'db>,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         match (self, other) {
             // A non-generic class is never equivalent to a generic class.
             // Two non-generic classes are only equivalent if they are equal (handled above).
-            (ClassType::NonGeneric(_), _) | (_, ClassType::NonGeneric(_)) => false,
+            (ClassType::NonGeneric(_), _) | (_, ClassType::NonGeneric(_)) => C::unsatisfiable(db),
 
             (ClassType::Generic(this), ClassType::Generic(other)) => {
-                this.origin(db) == other.origin(db)
-                    && this
-                        .specialization(db)
-                        .is_equivalent_to(db, other.specialization(db))
+                C::from_bool(db, this.origin(db) == other.origin(db)).and(db, || {
+                    this.specialization(db).is_equivalent_to_impl(
+                        db,
+                        other.specialization(db),
+                        visitor,
+                    )
+                })
             }
         }
     }
@@ -1613,6 +1638,15 @@ impl<'db> ClassLiteral<'db> {
             .contains(&ClassBase::Class(other))
     }
 
+    pub(super) fn when_subclass_of<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        specialization: Option<Specialization<'db>>,
+        other: ClassType<'db>,
+    ) -> C {
+        C::from_bool(db, self.is_subclass_of(db, specialization, other))
+    }
+
     /// Return `true` if this class constitutes a typed dict specification (inherits from
     /// `typing.TypedDict`, either directly or indirectly).
     #[salsa::tracked(
@@ -4186,6 +4220,14 @@ impl KnownClass {
             .is_ok_and(|class| class.is_subclass_of(db, None, other))
     }
 
+    pub(super) fn when_subclass_of<'db, C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: ClassType<'db>,
+    ) -> C {
+        C::from_bool(db, self.is_subclass_of(db, other))
+    }
+
     /// Return the module in which we should look up the definition for this class
     fn canonical_module(self, db: &dyn Db) -> KnownModule {
         match self {
diff --git a/crates/ty_python_semantic/src/types/class_base.rs b/crates/ty_python_semantic/src/types/class_base.rs
index e8a5fd1e41..2d05ca04ce 100644
--- a/crates/ty_python_semantic/src/types/class_base.rs
+++ b/crates/ty_python_semantic/src/types/class_base.rs
@@ -3,8 +3,7 @@ use crate::types::generics::Specialization;
 use crate::types::tuple::TupleType;
 use crate::types::{
     ApplyTypeMappingVisitor, ClassLiteral, ClassType, DynamicType, KnownClass, KnownInstanceType,
-    MroError, MroIterator, NormalizedVisitor, SpecialFormType, Type, TypeMapping, TypeTransformer,
-    todo_type,
+    MroError, MroIterator, NormalizedVisitor, SpecialFormType, Type, TypeMapping, todo_type,
 };
 
 /// Enumeration of the possible kinds of types we allow in class bases.
@@ -292,7 +291,7 @@ impl<'db> ClassBase<'db> {
             self.apply_type_mapping_impl(
                 db,
                 &TypeMapping::Specialization(specialization),
-                &TypeTransformer::default(),
+                &ApplyTypeMappingVisitor::default(),
             )
         } else {
             self
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
new file mode 100644
index 0000000000..ddf003adf3
--- /dev/null
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -0,0 +1,184 @@
+//! Constraints under which type properties hold
+//!
+//! For "concrete" types (which contain no type variables), type properties like assignability have
+//! simple answers: one type is either assignable to another type, or it isn't. (The _rules_ for
+//! comparing two particular concrete types can be rather complex, but the _answer_ is a simple
+//! "yes" or "no".)
+//!
+//! These properties are more complex when type variables are involved, because there are (usually)
+//! many different concrete types that a typevar can be specialized to, and the type property might
+//! hold for some specializations, but not for others. That means that for types that include
+//! typevars, "Is this type assignable to another?" no longer makes sense as a question. The better
+//! question is: "Under what constraints is this type assignable to another?".
+//!
+//! This module provides the machinery for representing the "under what constraints" part of that
+//! question. An individual constraint restricts the specialization of a single typevar to be within a
+//! particular lower and upper bound. You can then build up more complex constraint sets using
+//! union, intersection, and negation operations (just like types themselves).
+//!
+//! NOTE: This module is currently in a transitional state: we've added a trait that our constraint
+//! set implementations will conform to, and updated all of our type property implementations to
+//! work on any impl of that trait. But the only impl we have right now is `bool`, which means that
+//! we are still not tracking the full detail as promised in the description above. (`bool` is a
+//! perfectly fine impl, but it can generate false positives when you have to break down a
+//! particular assignability check into subchecks: each subcheck might say "yes", but technically
+//! under conflicting constraints, which a single `bool` can't track.) Soon we will add a proper
+//! constraint set implementation, and the `bool` impl of the trait (and possibly the trait itself)
+//! will go away.
+
+use crate::Db;
+
+/// Encodes the constraints under which a type property (e.g. assignability) holds.
+pub(crate) trait Constraints<'db>: Clone + Sized {
+    /// Returns a constraint set that never holds
+    fn unsatisfiable(db: &'db dyn Db) -> Self;
+
+    /// Returns a constraint set that always holds
+    fn always_satisfiable(db: &'db dyn Db) -> Self;
+
+    /// Returns whether this constraint set never holds
+    fn is_never_satisfied(&self, db: &'db dyn Db) -> bool;
+
+    /// Returns whether this constraint set always holds
+    fn is_always_satisfied(&self, db: &'db dyn Db) -> bool;
+
+    /// Updates this constraint set to hold the union of itself and another constraint set.
+    fn union(&mut self, db: &'db dyn Db, other: Self) -> &Self;
+
+    /// Updates this constraint set to hold the intersection of itself and another constraint set.
+    fn intersect(&mut self, db: &'db dyn Db, other: Self) -> &Self;
+
+    /// Returns the negation of this constraint set.
+    fn negate(self, db: &'db dyn Db) -> Self;
+
+    /// Returns a constraint set representing a boolean condition.
+    fn from_bool(db: &'db dyn Db, b: bool) -> Self {
+        if b {
+            Self::always_satisfiable(db)
+        } else {
+            Self::unsatisfiable(db)
+        }
+    }
+
+    /// Returns the intersection of this constraint set and another. The other constraint set is
+    /// provided as a thunk, to implement short-circuiting: the thunk is not forced if the
+    /// constraint set is already saturated.
+    fn and(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
+        if !self.is_never_satisfied(db) {
+            self.intersect(db, other());
+        }
+        self
+    }
+
+    /// Returns the union of this constraint set and another. The other constraint set is provided
+    /// as a thunk, to implement short-circuiting: the thunk is not forced if the constraint set is
+    /// already saturated.
+    fn or(mut self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
+        if !self.is_always_satisfied(db) {
+            self.union(db, other());
+        }
+        self
+    }
+}
+
+impl<'db> Constraints<'db> for bool {
+    fn unsatisfiable(_db: &'db dyn Db) -> Self {
+        false
+    }
+
+    fn always_satisfiable(_db: &'db dyn Db) -> Self {
+        true
+    }
+
+    fn is_never_satisfied(&self, _db: &'db dyn Db) -> bool {
+        !*self
+    }
+
+    fn is_always_satisfied(&self, _db: &'db dyn Db) -> bool {
+        *self
+    }
+
+    fn union(&mut self, _db: &'db dyn Db, other: Self) -> &Self {
+        *self = *self || other;
+        self
+    }
+
+    fn intersect(&mut self, _db: &'db dyn Db, other: Self) -> &Self {
+        *self = *self && other;
+        self
+    }
+
+    fn negate(self, _db: &'db dyn Db) -> Self {
+        !self
+    }
+}
+
+/// An extension trait for building constraint sets from [`Option`] values.
+pub(crate) trait OptionConstraintsExtension<T> {
+    /// Returns [`always_satisfiable`][Constraints::always_satisfiable] if the option is `None`;
+    /// otherwise applies a function to determine under what constraints the value inside of it
+    /// holds.
+    fn when_none_or<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnOnce(T) -> C) -> C;
+
+    /// Returns [`unsatisfiable`][Constraints::unsatisfiable] if the option is `None`; otherwise
+    /// applies a function to determine under what constraints the value inside of it holds.
+    fn when_some_and<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnOnce(T) -> C) -> C;
+}
+
+impl<T> OptionConstraintsExtension<T> for Option<T> {
+    fn when_none_or<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnOnce(T) -> C) -> C {
+        match self {
+            Some(value) => f(value),
+            None => C::always_satisfiable(db),
+        }
+    }
+
+    fn when_some_and<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnOnce(T) -> C) -> C {
+        match self {
+            Some(value) => f(value),
+            None => C::unsatisfiable(db),
+        }
+    }
+}
+
+/// An extension trait for building constraint sets from an [`Iterator`].
+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`][Constraints::is_always_satisfied] true, then the overall result
+    /// must be as well, and we stop consuming elements from the iterator.
+    fn when_any<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnMut(T) -> C) -> C;
+
+    /// Returns the constraints under which every element of the iterator holds.
+    ///
+    /// This method short-circuits; if we encounter any element that
+    /// [`is_never_satisfied`][Constraints::is_never_satisfied] true, then the overall result must
+    /// be as well, and we stop consuming elements from the iterator.
+    fn when_all<'db, C: Constraints<'db>>(self, db: &'db dyn Db, f: impl FnMut(T) -> C) -> C;
+}
+
+impl<I, T> IteratorConstraintsExtension<T> for I
+where
+    I: Iterator<Item = T>,
+{
+    fn when_any<'db, C: Constraints<'db>>(self, db: &'db dyn Db, mut f: impl FnMut(T) -> C) -> C {
+        let mut result = C::unsatisfiable(db);
+        for child in self {
+            if result.union(db, f(child)).is_always_satisfied(db) {
+                return result;
+            }
+        }
+        result
+    }
+
+    fn when_all<'db, C: Constraints<'db>>(self, db: &'db dyn Db, mut f: impl FnMut(T) -> C) -> C {
+        let mut result = C::always_satisfiable(db);
+        for child in self {
+            if result.intersect(db, f(child)).is_never_satisfied(db) {
+                return result;
+            }
+        }
+        result
+    }
+}
diff --git a/crates/ty_python_semantic/src/types/cyclic.rs b/crates/ty_python_semantic/src/types/cyclic.rs
index 27a201143b..979be6ae58 100644
--- a/crates/ty_python_semantic/src/types/cyclic.rs
+++ b/crates/ty_python_semantic/src/types/cyclic.rs
@@ -41,7 +41,7 @@ impl<Tag> Default for TypeTransformer<'_, Tag> {
     }
 }
 
-pub(crate) type PairVisitor<'db, Tag> = CycleDetector<Tag, (Type<'db>, Type<'db>), bool>;
+pub(crate) type PairVisitor<'db, Tag, C> = CycleDetector<Tag, (Type<'db>, Type<'db>), C>;
 
 #[derive(Debug)]
 pub(crate) struct CycleDetector<Tag, T, R> {
@@ -63,7 +63,7 @@ pub(crate) struct CycleDetector<Tag, T, R> {
     _tag: PhantomData<Tag>,
 }
 
-impl<Tag, T: Hash + Eq + Copy, R: Copy> CycleDetector<Tag, T, R> {
+impl<Tag, T: Hash + Eq + Clone, R: Clone> CycleDetector<Tag, T, R> {
     pub(crate) fn new(fallback: R) -> Self {
         CycleDetector {
             seen: RefCell::new(FxIndexSet::default()),
@@ -75,17 +75,17 @@ impl<Tag, T: Hash + Eq + Copy, R: Copy> CycleDetector<Tag, T, R> {
 
     pub(crate) fn visit(&self, item: T, func: impl FnOnce() -> R) -> R {
         if let Some(val) = self.cache.borrow().get(&item) {
-            return *val;
+            return val.clone();
         }
 
         // We hit a cycle
-        if !self.seen.borrow_mut().insert(item) {
-            return self.fallback;
+        if !self.seen.borrow_mut().insert(item.clone()) {
+            return self.fallback.clone();
         }
 
         let ret = func();
         self.seen.borrow_mut().pop();
-        self.cache.borrow_mut().insert(item, ret);
+        self.cache.borrow_mut().insert(item, ret.clone());
 
         ret
     }
diff --git a/crates/ty_python_semantic/src/types/function.rs b/crates/ty_python_semantic/src/types/function.rs
index 9a9c10ef75..dde034efc4 100644
--- a/crates/ty_python_semantic/src/types/function.rs
+++ b/crates/ty_python_semantic/src/types/function.rs
@@ -65,6 +65,7 @@ use crate::semantic_index::definition::Definition;
 use crate::semantic_index::scope::ScopeId;
 use crate::semantic_index::semantic_index;
 use crate::types::call::{Binding, CallArguments};
+use crate::types::constraints::Constraints;
 use crate::types::context::InferContext;
 use crate::types::diagnostic::{
     REDUNDANT_CAST, STATIC_ASSERT_ERROR, TYPE_ASSERTION_FAILURE,
@@ -77,8 +78,9 @@ use crate::types::signatures::{CallableSignature, Signature};
 use crate::types::visitor::any_over_type;
 use crate::types::{
     BoundMethodType, BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, ClassType,
-    DeprecatedInstance, DynamicType, KnownClass, NormalizedVisitor, Truthiness, Type, TypeMapping,
-    TypeRelation, TypeTransformer, UnionBuilder, all_members, walk_type_mapping,
+    DeprecatedInstance, DynamicType, HasRelationToVisitor, IsEquivalentVisitor, KnownClass,
+    NormalizedVisitor, Truthiness, Type, TypeMapping, TypeRelation, UnionBuilder, all_members,
+    walk_type_mapping,
 };
 use crate::{Db, FxOrderSet, ModuleName, resolve_module};
 
@@ -858,15 +860,16 @@ impl<'db> FunctionType<'db> {
         BoundMethodType::new(db, self, self_instance)
     }
 
-    pub(crate) fn has_relation_to(
+    pub(crate) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         relation: TypeRelation,
-    ) -> bool {
+        _visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match relation {
-            TypeRelation::Subtyping => self.is_subtype_of(db, other),
-            TypeRelation::Assignability => self.is_assignable_to(db, other),
+            TypeRelation::Subtyping => C::from_bool(db, self.is_subtype_of(db, other)),
+            TypeRelation::Assignability => C::from_bool(db, self.is_assignable_to(db, other)),
         }
     }
 
@@ -895,16 +898,21 @@ impl<'db> FunctionType<'db> {
             && self.signature(db).is_assignable_to(db, other.signature(db))
     }
 
-    pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self.normalized(db) == other.normalized(db) {
-            return true;
+            return C::always_satisfiable(db);
         }
         if self.literal(db) != other.literal(db) {
-            return false;
+            return C::unsatisfiable(db);
         }
         let self_signature = self.signature(db);
         let other_signature = other.signature(db);
-        self_signature.is_equivalent_to(db, other_signature)
+        self_signature.is_equivalent_to_impl(db, other_signature, visitor)
     }
 
     pub(crate) fn find_legacy_typevars(
@@ -920,7 +928,7 @@ impl<'db> FunctionType<'db> {
     }
 
     pub(crate) fn normalized(self, db: &'db dyn Db) -> Self {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     pub(crate) fn normalized_impl(self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 049b953949..2a686ef80a 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -9,13 +9,14 @@ use crate::semantic_index::definition::Definition;
 use crate::semantic_index::scope::{FileScopeId, NodeWithScopeKind};
 use crate::types::class::ClassType;
 use crate::types::class_base::ClassBase;
+use crate::types::constraints::Constraints;
 use crate::types::infer::infer_definition_types;
 use crate::types::instance::{Protocol, ProtocolInstanceType};
 use crate::types::signatures::{Parameter, Parameters, Signature};
 use crate::types::tuple::{TupleSpec, TupleType, walk_tuple_type};
 use crate::types::{
-    ApplyTypeMappingVisitor, BoundTypeVarInstance, HasRelationToVisitor, KnownClass,
-    KnownInstanceType, NormalizedVisitor, Type, TypeMapping, TypeRelation, TypeTransformer,
+    ApplyTypeMappingVisitor, BoundTypeVarInstance, HasRelationToVisitor, IsEquivalentVisitor,
+    KnownClass, KnownInstanceType, NormalizedVisitor, Type, TypeMapping, TypeRelation,
     TypeVarBoundOrConstraints, TypeVarInstance, TypeVarVariance, UnionType, binding_type,
     declaration_type,
 };
@@ -471,7 +472,7 @@ impl<'db> Specialization<'db> {
         db: &'db dyn Db,
         type_mapping: &TypeMapping<'a, 'db>,
     ) -> Self {
-        self.apply_type_mapping_impl(db, type_mapping, &TypeTransformer::default())
+        self.apply_type_mapping_impl(db, type_mapping, &ApplyTypeMappingVisitor::default())
     }
 
     pub(crate) fn apply_type_mapping_impl<'a>(
@@ -560,16 +561,16 @@ impl<'db> Specialization<'db> {
         Specialization::new(db, self.generic_context(db), types, tuple_inner)
     }
 
-    pub(crate) fn has_relation_to_impl(
+    pub(crate) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         let generic_context = self.generic_context(db);
         if generic_context != other.generic_context(db) {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         if let (Some(self_tuple), Some(other_tuple)) = (self.tuple_inner(db), other.tuple_inner(db))
@@ -577,6 +578,7 @@ impl<'db> Specialization<'db> {
             return self_tuple.has_relation_to_impl(db, other_tuple, relation, visitor);
         }
 
+        let mut result = C::always_satisfiable(db);
         for ((bound_typevar, self_type), other_type) in (generic_context.variables(db).into_iter())
             .zip(self.types(db))
             .zip(other.types(db))
@@ -584,7 +586,7 @@ impl<'db> Specialization<'db> {
             if self_type.is_dynamic() || other_type.is_dynamic() {
                 match relation {
                     TypeRelation::Assignability => continue,
-                    TypeRelation::Subtyping => return false,
+                    TypeRelation::Subtyping => return C::unsatisfiable(db),
                 }
             }
 
@@ -596,11 +598,12 @@ impl<'db> Specialization<'db> {
             //   - bivariant: skip, can't make subtyping/assignability false
             let compatible = match bound_typevar.variance(db) {
                 TypeVarVariance::Invariant => match relation {
-                    TypeRelation::Subtyping => self_type.is_equivalent_to(db, *other_type),
-                    TypeRelation::Assignability => {
+                    TypeRelation::Subtyping => self_type.when_equivalent_to(db, *other_type),
+                    TypeRelation::Assignability => C::from_bool(
+                        db,
                         self_type.is_assignable_to(db, *other_type)
-                            && other_type.is_assignable_to(db, *self_type)
-                    }
+                            && other_type.is_assignable_to(db, *self_type),
+                    ),
                 },
                 TypeVarVariance::Covariant => {
                     self_type.has_relation_to_impl(db, *other_type, relation, visitor)
@@ -608,22 +611,28 @@ impl<'db> Specialization<'db> {
                 TypeVarVariance::Contravariant => {
                     other_type.has_relation_to_impl(db, *self_type, relation, visitor)
                 }
-                TypeVarVariance::Bivariant => true,
+                TypeVarVariance::Bivariant => C::always_satisfiable(db),
             };
-            if !compatible {
-                return false;
+            if result.intersect(db, compatible).is_never_satisfied(db) {
+                return result;
             }
         }
 
-        true
+        result
     }
 
-    pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Specialization<'db>) -> bool {
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Specialization<'db>,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         let generic_context = self.generic_context(db);
         if generic_context != other.generic_context(db) {
-            return false;
+            return C::unsatisfiable(db);
         }
 
+        let mut result = C::always_satisfiable(db);
         for ((bound_typevar, self_type), other_type) in (generic_context.variables(db).into_iter())
             .zip(self.types(db))
             .zip(other.types(db))
@@ -637,25 +646,28 @@ impl<'db> Specialization<'db> {
             let compatible = match bound_typevar.variance(db) {
                 TypeVarVariance::Invariant
                 | TypeVarVariance::Covariant
-                | TypeVarVariance::Contravariant => self_type.is_equivalent_to(db, *other_type),
-                TypeVarVariance::Bivariant => true,
+                | TypeVarVariance::Contravariant => {
+                    self_type.is_equivalent_to_impl(db, *other_type, visitor)
+                }
+                TypeVarVariance::Bivariant => C::always_satisfiable(db),
             };
-            if !compatible {
-                return false;
+            if result.intersect(db, compatible).is_never_satisfied(db) {
+                return result;
             }
         }
 
         match (self.tuple_inner(db), other.tuple_inner(db)) {
-            (Some(_), None) | (None, Some(_)) => return false,
+            (Some(_), None) | (None, Some(_)) => return C::unsatisfiable(db),
             (None, None) => {}
             (Some(self_tuple), Some(other_tuple)) => {
-                if !self_tuple.is_equivalent_to(db, other_tuple) {
-                    return false;
+                let compatible = self_tuple.is_equivalent_to_impl(db, other_tuple, visitor);
+                if result.intersect(db, compatible).is_never_satisfied(db) {
+                    return result;
                 }
             }
         }
 
-        true
+        result
     }
 
     pub(crate) fn find_legacy_typevars(
diff --git a/crates/ty_python_semantic/src/types/instance.rs b/crates/ty_python_semantic/src/types/instance.rs
index eb6978af22..8c3cdbb786 100644
--- a/crates/ty_python_semantic/src/types/instance.rs
+++ b/crates/ty_python_semantic/src/types/instance.rs
@@ -7,12 +7,13 @@ use super::protocol_class::ProtocolInterface;
 use super::{BoundTypeVarInstance, ClassType, KnownClass, SubclassOfType, Type, TypeVarVariance};
 use crate::place::PlaceAndQualifiers;
 use crate::semantic_index::definition::Definition;
+use crate::types::constraints::{Constraints, IteratorConstraintsExtension};
 use crate::types::enums::is_single_member_enum;
 use crate::types::protocol_class::walk_protocol_interface;
 use crate::types::tuple::{TupleSpec, TupleType};
 use crate::types::{
     ApplyTypeMappingVisitor, ClassBase, DynamicType, HasRelationToVisitor, IsDisjointVisitor,
-    NormalizedVisitor, TypeMapping, TypeRelation, TypeTransformer, VarianceInferable,
+    IsEquivalentVisitor, NormalizedVisitor, TypeMapping, TypeRelation, VarianceInferable,
 };
 use crate::{Db, FxOrderSet};
 
@@ -92,23 +93,26 @@ impl<'db> Type<'db> {
             SynthesizedProtocolType::new(
                 db,
                 ProtocolInterface::with_property_members(db, members),
-                &TypeTransformer::default(),
+                &NormalizedVisitor::default(),
             ),
         ))
     }
 
     /// Return `true` if `self` conforms to the interface described by `protocol`.
-    pub(super) fn satisfies_protocol(
+    pub(super) fn satisfies_protocol<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         protocol: ProtocolInstanceType<'db>,
         relation: TypeRelation,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         protocol
             .inner
             .interface(db)
             .members(db)
-            .all(|member| member.is_satisfied_by(db, self, relation))
+            .when_all(db, |member| {
+                member.is_satisfied_by(db, self, relation, visitor)
+            })
     }
 }
 
@@ -264,13 +268,13 @@ impl<'db> NominalInstanceType<'db> {
         }
     }
 
-    pub(super) fn has_relation_to_impl(
+    pub(super) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match (self.0, other.0) {
             (
                 NominalInstanceInner::ExactTuple(tuple1),
@@ -282,35 +286,45 @@ impl<'db> NominalInstanceType<'db> {
         }
     }
 
-    pub(super) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(super) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         match (self.0, other.0) {
             (
                 NominalInstanceInner::ExactTuple(tuple1),
                 NominalInstanceInner::ExactTuple(tuple2),
-            ) => tuple1.is_equivalent_to(db, tuple2),
+            ) => tuple1.is_equivalent_to_impl(db, tuple2, visitor),
             (NominalInstanceInner::NonTuple(class1), NominalInstanceInner::NonTuple(class2)) => {
-                class1.is_equivalent_to(db, class2)
+                class1.is_equivalent_to_impl(db, class2, visitor)
             }
-            _ => false,
+            _ => C::unsatisfiable(db),
         }
     }
 
-    pub(super) fn is_disjoint_from_impl(
+    pub(super) fn is_disjoint_from_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
-        visitor: &IsDisjointVisitor<'db>,
-    ) -> bool {
+        visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
+        let mut result = C::unsatisfiable(db);
         if let Some(self_spec) = self.tuple_spec(db) {
             if let Some(other_spec) = other.tuple_spec(db) {
-                if self_spec.is_disjoint_from_impl(db, &other_spec, visitor) {
-                    return true;
+                let compatible = self_spec.is_disjoint_from_impl(db, &other_spec, visitor);
+                if result.union(db, compatible).is_always_satisfied(db) {
+                    return result;
                 }
             }
         }
-        !self
-            .class(db)
-            .could_coexist_in_mro_with(db, other.class(db))
+        result.or(db, || {
+            C::from_bool(
+                db,
+                !(self.class(db)).could_coexist_in_mro_with(db, other.class(db)),
+            )
+        })
     }
 
     pub(super) fn is_singleton(self, db: &'db dyn Db) -> bool {
@@ -479,7 +493,7 @@ impl<'db> ProtocolInstanceType<'db> {
     ///
     /// See [`Type::normalized`] for more details.
     pub(super) fn normalized(self, db: &'db dyn Db) -> Type<'db> {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     /// Return a "normalized" version of this `Protocol` type.
@@ -491,7 +505,12 @@ impl<'db> ProtocolInstanceType<'db> {
         visitor: &NormalizedVisitor<'db>,
     ) -> Type<'db> {
         let object = Type::object(db);
-        if object.satisfies_protocol(db, self, TypeRelation::Subtyping) {
+        if object.satisfies_protocol(
+            db,
+            self,
+            TypeRelation::Subtyping,
+            &HasRelationToVisitor::new(true),
+        ) {
             return object;
         }
         match self.inner {
@@ -505,30 +524,36 @@ impl<'db> ProtocolInstanceType<'db> {
     /// Return `true` if this protocol type has the given type relation to the protocol `other`.
     ///
     /// TODO: consider the types of the members as well as their existence
-    pub(super) fn has_relation_to(
+    pub(super) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         _relation: TypeRelation,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         other
             .inner
             .interface(db)
-            .is_sub_interface_of(db, self.inner.interface(db))
+            .is_sub_interface_of(db, self.inner.interface(db), visitor)
     }
 
     /// Return `true` if this protocol type is equivalent to the protocol `other`.
     ///
     /// TODO: consider the types of the members as well as their existence
-    pub(super) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(super) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        _visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         if self == other {
-            return true;
+            return C::always_satisfiable(db);
         }
         let self_normalized = self.normalized(db);
         if self_normalized == Type::ProtocolInstance(other) {
-            return true;
+            return C::always_satisfiable(db);
         }
-        self_normalized == other.normalized(db)
+        C::from_bool(db, self_normalized == other.normalized(db))
     }
 
     /// Return `true` if this protocol type is disjoint from the protocol `other`.
@@ -536,13 +561,13 @@ impl<'db> ProtocolInstanceType<'db> {
     /// TODO: a protocol `X` is disjoint from a protocol `Y` if `X` and `Y`
     /// have a member with the same name but disjoint types
     #[expect(clippy::unused_self)]
-    pub(super) fn is_disjoint_from_impl(
+    pub(super) fn is_disjoint_from_impl<C: Constraints<'db>>(
         self,
-        _db: &'db dyn Db,
+        db: &'db dyn Db,
         _other: Self,
-        _visitor: &IsDisjointVisitor<'db>,
-    ) -> bool {
-        false
+        _visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
+        C::unsatisfiable(db)
     }
 
     pub(crate) fn instance_member(self, db: &'db dyn Db, name: &str) -> PlaceAndQualifiers<'db> {
diff --git a/crates/ty_python_semantic/src/types/protocol_class.rs b/crates/ty_python_semantic/src/types/protocol_class.rs
index d910bdc1ce..6bb6a16ac4 100644
--- a/crates/ty_python_semantic/src/types/protocol_class.rs
+++ b/crates/ty_python_semantic/src/types/protocol_class.rs
@@ -16,9 +16,10 @@ use crate::{
     place::{Boundness, Place, PlaceAndQualifiers, place_from_bindings, place_from_declarations},
     semantic_index::{definition::Definition, use_def_map},
     types::{
-        BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, IsDisjointVisitor,
-        KnownFunction, NormalizedVisitor, PropertyInstanceType, Signature, Type, TypeMapping,
-        TypeQualifiers, TypeRelation, TypeTransformer, VarianceInferable,
+        BoundTypeVarInstance, CallableType, ClassBase, ClassLiteral, HasRelationToVisitor,
+        IsDisjointVisitor, KnownFunction, NormalizedVisitor, PropertyInstanceType, Signature, Type,
+        TypeMapping, TypeQualifiers, TypeRelation, VarianceInferable,
+        constraints::{Constraints, IteratorConstraintsExtension},
         signatures::{Parameter, Parameters},
     },
 };
@@ -219,10 +220,17 @@ impl<'db> ProtocolInterface<'db> {
     /// Return `true` if if all members on `self` are also members of `other`.
     ///
     /// TODO: this method should consider the types of the members as well as their names.
-    pub(super) fn is_sub_interface_of(self, db: &'db dyn Db, other: Self) -> bool {
-        self.inner(db)
-            .keys()
-            .all(|member_name| other.inner(db).contains_key(member_name))
+    pub(super) fn is_sub_interface_of<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        _visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
+        // TODO: This could just return a bool as written, but this form is what will be needed to
+        // combine the constraints when we do assignability checks on each member.
+        self.inner(db).keys().when_all(db, |member_name| {
+            C::from_bool(db, other.inner(db).contains_key(member_name))
+        })
     }
 
     pub(super) fn normalized_impl(self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
@@ -318,7 +326,7 @@ pub(super) struct ProtocolMemberData<'db> {
 
 impl<'db> ProtocolMemberData<'db> {
     fn normalized(&self, db: &'db dyn Db) -> Self {
-        self.normalized_impl(db, &TypeTransformer::default())
+        self.normalized_impl(db, &NormalizedVisitor::default())
     }
 
     fn normalized_impl(&self, db: &'db dyn Db, visitor: &NormalizedVisitor<'db>) -> Self {
@@ -504,46 +512,56 @@ impl<'a, 'db> ProtocolMember<'a, 'db> {
         }
     }
 
-    pub(super) fn has_disjoint_type_from(
+    pub(super) fn has_disjoint_type_from<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: Type<'db>,
-        visitor: &IsDisjointVisitor<'db>,
-    ) -> bool {
+        visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
         match &self.kind {
             // TODO: implement disjointness for property/method members as well as attribute members
-            ProtocolMemberKind::Property(_) | ProtocolMemberKind::Method(_) => false,
+            ProtocolMemberKind::Property(_) | ProtocolMemberKind::Method(_) => C::unsatisfiable(db),
             ProtocolMemberKind::Other(ty) => ty.is_disjoint_from_impl(db, other, visitor),
         }
     }
 
     /// Return `true` if `other` contains an attribute/method/property that satisfies
     /// the part of the interface defined by this protocol member.
-    pub(super) fn is_satisfied_by(
+    pub(super) fn is_satisfied_by<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: Type<'db>,
         relation: TypeRelation,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match &self.kind {
             // TODO: consider the types of the attribute on `other` for method members
-            ProtocolMemberKind::Method(_) => matches!(
-                other.to_meta_type(db).member(db, self.name).place,
-                Place::Type(_, Boundness::Bound)
+            ProtocolMemberKind::Method(_) => C::from_bool(
+                db,
+                matches!(
+                    other.to_meta_type(db).member(db, self.name).place,
+                    Place::Type(_, Boundness::Bound)
+                ),
             ),
             // TODO: consider the types of the attribute on `other` for property members
-            ProtocolMemberKind::Property(_) => matches!(
-                other.member(db, self.name).place,
-                Place::Type(_, Boundness::Bound)
+            ProtocolMemberKind::Property(_) => C::from_bool(
+                db,
+                matches!(
+                    other.member(db, self.name).place,
+                    Place::Type(_, Boundness::Bound)
+                ),
             ),
             ProtocolMemberKind::Other(member_type) => {
                 let Place::Type(attribute_type, Boundness::Bound) =
                     other.member(db, self.name).place
                 else {
-                    return false;
+                    return C::unsatisfiable(db);
                 };
-                member_type.has_relation_to(db, attribute_type, relation)
-                    && attribute_type.has_relation_to(db, *member_type, relation)
+                member_type
+                    .has_relation_to_impl(db, attribute_type, relation, visitor)
+                    .and(db, || {
+                        attribute_type.has_relation_to_impl(db, *member_type, relation, visitor)
+                    })
             }
         }
     }
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index 4c80c37571..478b75b057 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -17,10 +17,11 @@ use smallvec::{SmallVec, smallvec_inline};
 
 use super::{DynamicType, Type, TypeVarVariance, definition_expression_type};
 use crate::semantic_index::definition::Definition;
+use crate::types::constraints::{Constraints, IteratorConstraintsExtension};
 use crate::types::generics::{GenericContext, walk_generic_context};
 use crate::types::{
-    BindingContext, BoundTypeVarInstance, KnownClass, NormalizedVisitor, TypeMapping, TypeRelation,
-    VarianceInferable, todo_type,
+    BindingContext, BoundTypeVarInstance, HasRelationToVisitor, IsEquivalentVisitor, KnownClass,
+    NormalizedVisitor, TypeMapping, TypeRelation, VarianceInferable, todo_type,
 };
 use crate::{Db, FxOrderSet};
 use ruff_python_ast::{self as ast, name::Name};
@@ -112,27 +113,19 @@ impl<'db> CallableSignature<'db> {
         }
     }
 
-    pub(crate) fn has_relation_to(
-        &self,
-        db: &'db dyn Db,
-        other: &Self,
-        relation: TypeRelation,
-    ) -> bool {
-        match relation {
-            TypeRelation::Subtyping => self.is_subtype_of(db, other),
-            TypeRelation::Assignability => self.is_assignable_to(db, other),
-        }
-    }
-
     /// Check whether this callable type is a subtype of another callable type.
     ///
     /// See [`Type::is_subtype_of`] for more details.
     pub(crate) fn is_subtype_of(&self, db: &'db dyn Db, other: &Self) -> bool {
-        Self::has_relation_to_impl(
+        self.is_subtype_of_impl(db, other)
+    }
+
+    fn is_subtype_of_impl<C: Constraints<'db>>(&self, db: &'db dyn Db, other: &Self) -> C {
+        self.has_relation_to_impl(
             db,
-            &self.overloads,
-            &other.overloads,
+            other,
             TypeRelation::Subtyping,
+            &HasRelationToVisitor::new(C::always_satisfiable(db)),
         )
     }
 
@@ -140,55 +133,69 @@ impl<'db> CallableSignature<'db> {
     ///
     /// See [`Type::is_assignable_to`] for more details.
     pub(crate) fn is_assignable_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        Self::has_relation_to_impl(
+        self.has_relation_to_impl(
             db,
-            &self.overloads,
-            &other.overloads,
+            other,
             TypeRelation::Assignability,
+            &HasRelationToVisitor::new(true),
         )
     }
 
+    pub(crate) fn has_relation_to_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Self,
+        relation: TypeRelation,
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
+        Self::has_relation_to_inner(db, &self.overloads, &other.overloads, relation, visitor)
+    }
+
     /// Implementation of subtyping and assignability between two, possible overloaded, callable
     /// types.
-    fn has_relation_to_impl(
+    fn has_relation_to_inner<C: Constraints<'db>>(
         db: &'db dyn Db,
         self_signatures: &[Signature<'db>],
         other_signatures: &[Signature<'db>],
         relation: TypeRelation,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match (self_signatures, other_signatures) {
             ([self_signature], [other_signature]) => {
                 // Base case: both callable types contain a single signature.
-                self_signature.has_relation_to(db, other_signature, relation)
+                self_signature.has_relation_to_impl(db, other_signature, relation, visitor)
             }
 
             // `self` is possibly overloaded while `other` is definitely not overloaded.
-            (_, [_]) => self_signatures.iter().any(|self_signature| {
-                Self::has_relation_to_impl(
+            (_, [_]) => self_signatures.iter().when_any(db, |self_signature| {
+                Self::has_relation_to_inner(
                     db,
                     std::slice::from_ref(self_signature),
                     other_signatures,
                     relation,
+                    visitor,
                 )
             }),
 
             // `self` is definitely not overloaded while `other` is possibly overloaded.
-            ([_], _) => other_signatures.iter().all(|other_signature| {
-                Self::has_relation_to_impl(
+            ([_], _) => other_signatures.iter().when_all(db, |other_signature| {
+                Self::has_relation_to_inner(
                     db,
                     self_signatures,
                     std::slice::from_ref(other_signature),
                     relation,
+                    visitor,
                 )
             }),
 
             // `self` is definitely overloaded while `other` is possibly overloaded.
-            (_, _) => other_signatures.iter().all(|other_signature| {
-                Self::has_relation_to_impl(
+            (_, _) => other_signatures.iter().when_all(db, |other_signature| {
+                Self::has_relation_to_inner(
                     db,
                     self_signatures,
                     std::slice::from_ref(other_signature),
                     relation,
+                    visitor,
                 )
             }),
         }
@@ -197,18 +204,24 @@ impl<'db> CallableSignature<'db> {
     /// Check whether this callable type is equivalent to another callable type.
     ///
     /// See [`Type::is_equivalent_to`] for more details.
-    pub(crate) fn is_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
         match (self.overloads.as_slice(), other.overloads.as_slice()) {
             ([self_signature], [other_signature]) => {
                 // Common case: both callable types contain a single signature, use the custom
                 // equivalence check instead of delegating it to the subtype check.
-                self_signature.is_equivalent_to(db, other_signature)
+                self_signature.is_equivalent_to_impl(db, other_signature, visitor)
             }
             (_, _) => {
                 if self == other {
-                    return true;
+                    return C::always_satisfiable(db);
                 }
-                self.is_subtype_of(db, other) && other.is_subtype_of(db, self)
+                self.is_subtype_of_impl::<C>(db, other)
+                    .and(db, || other.is_subtype_of_impl(db, self))
             }
         }
     }
@@ -498,23 +511,31 @@ impl<'db> Signature<'db> {
     /// Return `true` if `self` has exactly the same set of possible static materializations as
     /// `other` (if `self` represents the same set of possible sets of possible runtime objects as
     /// `other`).
-    pub(crate) fn is_equivalent_to(&self, db: &'db dyn Db, other: &Signature<'db>) -> bool {
-        let check_types = |self_type: Option<Type<'db>>, other_type: Option<Type<'db>>| {
-            self_type
-                .unwrap_or(Type::unknown())
-                .is_equivalent_to(db, other_type.unwrap_or(Type::unknown()))
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Signature<'db>,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        let mut result = C::always_satisfiable(db);
+        let mut check_types = |self_type: Option<Type<'db>>, other_type: Option<Type<'db>>| {
+            let self_type = self_type.unwrap_or(Type::unknown());
+            let other_type = other_type.unwrap_or(Type::unknown());
+            !result
+                .intersect(db, self_type.is_equivalent_to_impl(db, other_type, visitor))
+                .is_never_satisfied(db)
         };
 
         if self.parameters.is_gradual() != other.parameters.is_gradual() {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         if self.parameters.len() != other.parameters.len() {
-            return false;
+            return C::unsatisfiable(db);
         }
 
         if !check_types(self.return_ty, other.return_ty) {
-            return false;
+            return result;
         }
 
         for (self_parameter, other_parameter) in self.parameters.iter().zip(&other.parameters) {
@@ -558,27 +579,28 @@ impl<'db> Signature<'db> {
 
                 (ParameterKind::KeywordVariadic { .. }, ParameterKind::KeywordVariadic { .. }) => {}
 
-                _ => return false,
+                _ => return C::unsatisfiable(db),
             }
 
             if !check_types(
                 self_parameter.annotated_type(),
                 other_parameter.annotated_type(),
             ) {
-                return false;
+                return result;
             }
         }
 
-        true
+        result
     }
 
     /// Implementation of subtyping and assignability for signature.
-    fn has_relation_to(
+    fn has_relation_to_impl<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: &Signature<'db>,
         relation: TypeRelation,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         /// A helper struct to zip two slices of parameters together that provides control over the
         /// two iterators individually. It also keeps track of the current parameter in each
         /// iterator.
@@ -640,17 +662,18 @@ impl<'db> Signature<'db> {
             }
         }
 
-        let check_types = |type1: Option<Type<'db>>, type2: Option<Type<'db>>| {
-            type1.unwrap_or(Type::unknown()).has_relation_to(
-                db,
-                type2.unwrap_or(Type::unknown()),
-                relation,
-            )
+        let mut result = C::always_satisfiable(db);
+        let mut check_types = |type1: Option<Type<'db>>, type2: Option<Type<'db>>| {
+            let type1 = type1.unwrap_or(Type::unknown());
+            let type2 = type2.unwrap_or(Type::unknown());
+            !result
+                .intersect(db, type1.has_relation_to_impl(db, type2, relation, visitor))
+                .is_never_satisfied(db)
         };
 
         // Return types are covariant.
         if !check_types(self.return_ty, other.return_ty) {
-            return false;
+            return result;
         }
 
         // A gradual parameter list is a supertype of the "bottom" parameter list (*args: object,
@@ -665,13 +688,13 @@ impl<'db> Signature<'db> {
                 .keyword_variadic()
                 .is_some_and(|(_, param)| param.annotated_type().is_some_and(|ty| ty.is_object(db)))
         {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         // If either of the parameter lists is gradual (`...`), then it is assignable to and from
         // any other parameter list, but not a subtype or supertype of any other parameter list.
         if self.parameters.is_gradual() || other.parameters.is_gradual() {
-            return relation.is_assignability();
+            return C::from_bool(db, relation.is_assignability());
         }
 
         let mut parameters = ParametersZip {
@@ -689,7 +712,7 @@ impl<'db> Signature<'db> {
             let Some(next_parameter) = parameters.next() else {
                 // All parameters have been checked or both the parameter lists were empty. In
                 // either case, `self` is a subtype of `other`.
-                return true;
+                return result;
             };
 
             match next_parameter {
@@ -709,7 +732,7 @@ impl<'db> Signature<'db> {
                         // `other`, then the non-variadic parameters in `self` must have a default
                         // value.
                         if default_type.is_none() {
-                            return false;
+                            return C::unsatisfiable(db);
                         }
                     }
                     ParameterKind::Variadic { .. } | ParameterKind::KeywordVariadic { .. } => {
@@ -721,7 +744,7 @@ impl<'db> Signature<'db> {
                 EitherOrBoth::Right(_) => {
                     // If there are more parameters in `other` than in `self`, then `self` is not a
                     // subtype of `other`.
-                    return false;
+                    return C::unsatisfiable(db);
                 }
 
                 EitherOrBoth::Both(self_parameter, other_parameter) => {
@@ -741,13 +764,13 @@ impl<'db> Signature<'db> {
                             },
                         ) => {
                             if self_default.is_none() && other_default.is_some() {
-                                return false;
+                                return C::unsatisfiable(db);
                             }
                             if !check_types(
                                 other_parameter.annotated_type(),
                                 self_parameter.annotated_type(),
                             ) {
-                                return false;
+                                return result;
                             }
                         }
 
@@ -762,17 +785,17 @@ impl<'db> Signature<'db> {
                             },
                         ) => {
                             if self_name != other_name {
-                                return false;
+                                return C::unsatisfiable(db);
                             }
                             // The following checks are the same as positional-only parameters.
                             if self_default.is_none() && other_default.is_some() {
-                                return false;
+                                return C::unsatisfiable(db);
                             }
                             if !check_types(
                                 other_parameter.annotated_type(),
                                 self_parameter.annotated_type(),
                             ) {
-                                return false;
+                                return result;
                             }
                         }
 
@@ -785,7 +808,7 @@ impl<'db> Signature<'db> {
                                 other_parameter.annotated_type(),
                                 self_parameter.annotated_type(),
                             ) {
-                                return false;
+                                return result;
                             }
 
                             if matches!(
@@ -825,7 +848,7 @@ impl<'db> Signature<'db> {
                                     other_parameter.annotated_type(),
                                     self_parameter.annotated_type(),
                                 ) {
-                                    return false;
+                                    return result;
                                 }
                                 parameters.next_other();
                             }
@@ -836,7 +859,7 @@ impl<'db> Signature<'db> {
                                 other_parameter.annotated_type(),
                                 self_parameter.annotated_type(),
                             ) {
-                                return false;
+                                return result;
                             }
                         }
 
@@ -851,7 +874,7 @@ impl<'db> Signature<'db> {
                             break;
                         }
 
-                        _ => return false,
+                        _ => return C::unsatisfiable(db),
                     }
                 }
             }
@@ -885,7 +908,7 @@ impl<'db> Signature<'db> {
                     // previous loop. They cannot be matched against any parameter in `other` which
                     // only contains keyword-only and keyword-variadic parameters so the subtype
                     // relation is invalid.
-                    return false;
+                    return C::unsatisfiable(db);
                 }
                 ParameterKind::Variadic { .. } => {}
             }
@@ -912,13 +935,13 @@ impl<'db> Signature<'db> {
                                 ..
                             } => {
                                 if self_default.is_none() && other_default.is_some() {
-                                    return false;
+                                    return C::unsatisfiable(db);
                                 }
                                 if !check_types(
                                     other_parameter.annotated_type(),
                                     self_parameter.annotated_type(),
                                 ) {
-                                    return false;
+                                    return result;
                                 }
                             }
                             _ => unreachable!(
@@ -930,25 +953,25 @@ impl<'db> Signature<'db> {
                             other_parameter.annotated_type(),
                             self_keyword_variadic_type,
                         ) {
-                            return false;
+                            return result;
                         }
                     } else {
-                        return false;
+                        return C::unsatisfiable(db);
                     }
                 }
                 ParameterKind::KeywordVariadic { .. } => {
                     let Some(self_keyword_variadic_type) = self_keyword_variadic else {
                         // For a `self <: other` relationship, if `other` has a keyword variadic
                         // parameter, `self` must also have a keyword variadic parameter.
-                        return false;
+                        return C::unsatisfiable(db);
                     };
                     if !check_types(other_parameter.annotated_type(), self_keyword_variadic_type) {
-                        return false;
+                        return result;
                     }
                 }
                 _ => {
                     // This can only occur in case of a syntax error.
-                    return false;
+                    return C::unsatisfiable(db);
                 }
             }
         }
@@ -957,11 +980,11 @@ impl<'db> Signature<'db> {
         // optional otherwise the subtype relation is invalid.
         for (_, self_parameter) in self_keywords {
             if self_parameter.default_type().is_none() {
-                return false;
+                return C::unsatisfiable(db);
             }
         }
 
-        true
+        result
     }
 
     /// Create a new signature with the given definition.
diff --git a/crates/ty_python_semantic/src/types/subclass_of.rs b/crates/ty_python_semantic/src/types/subclass_of.rs
index eeb3294363..38f399ae56 100644
--- a/crates/ty_python_semantic/src/types/subclass_of.rs
+++ b/crates/ty_python_semantic/src/types/subclass_of.rs
@@ -2,11 +2,12 @@ use ruff_python_ast::name::Name;
 
 use crate::place::PlaceAndQualifiers;
 use crate::semantic_index::definition::Definition;
+use crate::types::constraints::Constraints;
 use crate::types::variance::VarianceInferable;
 use crate::types::{
     ApplyTypeMappingVisitor, BindingContext, BoundTypeVarInstance, ClassType, DynamicType,
-    HasRelationToVisitor, KnownClass, MemberLookupPolicy, NormalizedVisitor, Type, TypeMapping,
-    TypeRelation, TypeVarInstance,
+    HasRelationToVisitor, IsDisjointVisitor, KnownClass, MemberLookupPolicy, NormalizedVisitor,
+    Type, TypeMapping, TypeRelation, TypeVarInstance,
 };
 use crate::{Db, FxOrderSet};
 
@@ -159,21 +160,23 @@ impl<'db> SubclassOfType<'db> {
     }
 
     /// Return `true` if `self` has a certain relation to `other`.
-    pub(crate) fn has_relation_to_impl(
+    pub(crate) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: SubclassOfType<'db>,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match (self.subclass_of, other.subclass_of) {
             (SubclassOfInner::Dynamic(_), SubclassOfInner::Dynamic(_)) => {
-                relation.is_assignability()
+                C::from_bool(db, relation.is_assignability())
             }
             (SubclassOfInner::Dynamic(_), SubclassOfInner::Class(other_class)) => {
-                other_class.is_object(db) || relation.is_assignability()
+                C::from_bool(db, other_class.is_object(db) || relation.is_assignability())
+            }
+            (SubclassOfInner::Class(_), SubclassOfInner::Dynamic(_)) => {
+                C::from_bool(db, relation.is_assignability())
             }
-            (SubclassOfInner::Class(_), SubclassOfInner::Dynamic(_)) => relation.is_assignability(),
 
             // For example, `type[bool]` describes all possible runtime subclasses of the class `bool`,
             // and `type[int]` describes all possible runtime subclasses of the class `int`.
@@ -187,11 +190,18 @@ impl<'db> SubclassOfType<'db> {
     /// Return` true` if `self` is a disjoint type from `other`.
     ///
     /// See [`Type::is_disjoint_from`] for more details.
-    pub(crate) fn is_disjoint_from_impl(self, db: &'db dyn Db, other: Self) -> bool {
+    pub(crate) fn is_disjoint_from_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        _visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
         match (self.subclass_of, other.subclass_of) {
-            (SubclassOfInner::Dynamic(_), _) | (_, SubclassOfInner::Dynamic(_)) => false,
+            (SubclassOfInner::Dynamic(_), _) | (_, SubclassOfInner::Dynamic(_)) => {
+                C::unsatisfiable(db)
+            }
             (SubclassOfInner::Class(self_class), SubclassOfInner::Class(other_class)) => {
-                !self_class.could_coexist_in_mro_with(db, other_class)
+                C::from_bool(db, !self_class.could_coexist_in_mro_with(db, other_class))
             }
         }
     }
diff --git a/crates/ty_python_semantic/src/types/tuple.rs b/crates/ty_python_semantic/src/types/tuple.rs
index 6058b4e49a..35de11013d 100644
--- a/crates/ty_python_semantic/src/types/tuple.rs
+++ b/crates/ty_python_semantic/src/types/tuple.rs
@@ -24,9 +24,11 @@ use itertools::{Either, EitherOrBoth, Itertools};
 use crate::semantic_index::definition::Definition;
 use crate::types::Truthiness;
 use crate::types::class::{ClassType, KnownClass};
+use crate::types::constraints::{Constraints, IteratorConstraintsExtension};
 use crate::types::{
     ApplyTypeMappingVisitor, BoundTypeVarInstance, HasRelationToVisitor, IsDisjointVisitor,
-    NormalizedVisitor, Type, TypeMapping, TypeRelation, TypeVarVariance, UnionBuilder, UnionType,
+    IsEquivalentVisitor, NormalizedVisitor, Type, TypeMapping, TypeRelation, TypeVarVariance,
+    UnionBuilder, UnionType,
 };
 use crate::util::subscript::{Nth, OutOfBoundsError, PyIndex, PySlice, StepSizeZeroError};
 use crate::{Db, FxOrderSet, Program};
@@ -254,19 +256,25 @@ impl<'db> TupleType<'db> {
             .find_legacy_typevars(db, binding_context, typevars);
     }
 
-    pub(crate) fn has_relation_to_impl(
+    pub(crate) fn has_relation_to_impl<C: Constraints<'db>>(
         self,
         db: &'db dyn Db,
         other: Self,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         self.tuple(db)
             .has_relation_to_impl(db, other.tuple(db), relation, visitor)
     }
 
-    pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Self) -> bool {
-        self.tuple(db).is_equivalent_to(db, other.tuple(db))
+    pub(crate) fn is_equivalent_to_impl<C: Constraints<'db>>(
+        self,
+        db: &'db dyn Db,
+        other: Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        self.tuple(db)
+            .is_equivalent_to_impl(db, other.tuple(db), visitor)
     }
 
     pub(crate) fn is_single_valued(self, db: &'db dyn Db) -> bool {
@@ -409,56 +417,76 @@ impl<'db> FixedLengthTuple<Type<'db>> {
         }
     }
 
-    fn has_relation_to_impl(
+    fn has_relation_to_impl<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: &Tuple<Type<'db>>,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match other {
-            Tuple::Fixed(other) => {
-                self.0.len() == other.0.len()
-                    && (self.0.iter()).zip(&other.0).all(|(self_ty, other_ty)| {
-                        self_ty.has_relation_to_impl(db, *other_ty, relation, visitor)
-                    })
-            }
+            Tuple::Fixed(other) => C::from_bool(db, self.0.len() == other.0.len()).and(db, || {
+                (self.0.iter().zip(&other.0)).when_all(db, |(self_ty, other_ty)| {
+                    self_ty.has_relation_to_impl(db, *other_ty, relation, visitor)
+                })
+            }),
 
             Tuple::Variable(other) => {
                 // This tuple must have enough elements to match up with the other tuple's prefix
                 // and suffix, and each of those elements must pairwise satisfy the relation.
+                let mut result = C::always_satisfiable(db);
                 let mut self_iter = self.0.iter();
                 for other_ty in &other.prefix {
                     let Some(self_ty) = self_iter.next() else {
-                        return false;
+                        return C::unsatisfiable(db);
                     };
-                    if !self_ty.has_relation_to_impl(db, *other_ty, relation, visitor) {
-                        return false;
+                    let element_constraints =
+                        self_ty.has_relation_to_impl(db, *other_ty, relation, visitor);
+                    if result
+                        .intersect(db, element_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
                     }
                 }
                 for other_ty in other.suffix.iter().rev() {
                     let Some(self_ty) = self_iter.next_back() else {
-                        return false;
+                        return C::unsatisfiable(db);
                     };
-                    if !self_ty.has_relation_to_impl(db, *other_ty, relation, visitor) {
-                        return false;
+                    let element_constraints =
+                        self_ty.has_relation_to_impl(db, *other_ty, relation, visitor);
+                    if result
+                        .intersect(db, element_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
                     }
                 }
 
                 // In addition, any remaining elements in this tuple must satisfy the
                 // variable-length portion of the other tuple.
-                self_iter.all(|self_ty| {
-                    self_ty.has_relation_to_impl(db, other.variable, relation, visitor)
+                result.and(db, || {
+                    self_iter.when_all(db, |self_ty| {
+                        self_ty.has_relation_to_impl(db, other.variable, relation, visitor)
+                    })
                 })
             }
         }
     }
 
-    fn is_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        self.0.len() == other.0.len()
-            && (self.0.iter())
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        C::from_bool(db, self.0.len() == other.0.len()).and(db, || {
+            (self.0.iter())
                 .zip(&other.0)
-                .all(|(self_ty, other_ty)| self_ty.is_equivalent_to(db, *other_ty))
+                .when_all(db, |(self_ty, other_ty)| {
+                    self_ty.is_equivalent_to_impl(db, *other_ty, visitor)
+                })
+        })
     }
 
     fn is_single_valued(&self, db: &'db dyn Db) -> bool {
@@ -717,13 +745,13 @@ impl<'db> VariableLengthTuple<Type<'db>> {
         }
     }
 
-    fn has_relation_to_impl(
+    fn has_relation_to_impl<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: &Tuple<Type<'db>>,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match other {
             Tuple::Fixed(other) => {
                 // The `...` length specifier of a variable-length tuple type is interpreted
@@ -738,32 +766,43 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                 // length.
                 if relation == TypeRelation::Subtyping || !matches!(self.variable, Type::Dynamic(_))
                 {
-                    return false;
+                    return C::unsatisfiable(db);
                 }
 
                 // In addition, the other tuple must have enough elements to match up with this
                 // tuple's prefix and suffix, and each of those elements must pairwise satisfy the
                 // relation.
+                let mut result = C::always_satisfiable(db);
                 let mut other_iter = other.elements().copied();
                 for self_ty in self.prenormalized_prefix_elements(db, None) {
                     let Some(other_ty) = other_iter.next() else {
-                        return false;
+                        return C::unsatisfiable(db);
                     };
-                    if !self_ty.has_relation_to_impl(db, other_ty, relation, visitor) {
-                        return false;
+                    let element_constraints =
+                        self_ty.has_relation_to_impl(db, other_ty, relation, visitor);
+                    if result
+                        .intersect(db, element_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
                     }
                 }
                 let suffix: Vec<_> = self.prenormalized_suffix_elements(db, None).collect();
                 for self_ty in suffix.iter().rev() {
                     let Some(other_ty) = other_iter.next_back() else {
-                        return false;
+                        return C::unsatisfiable(db);
                     };
-                    if !self_ty.has_relation_to_impl(db, other_ty, relation, visitor) {
-                        return false;
+                    let element_constraints =
+                        self_ty.has_relation_to_impl(db, other_ty, relation, visitor);
+                    if result
+                        .intersect(db, element_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
                     }
                 }
 
-                true
+                result
             }
 
             Tuple::Variable(other) => {
@@ -781,12 +820,13 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                 // The overlapping parts of the prefixes and suffixes must satisfy the relation.
                 // Any remaining parts must satisfy the relation with the other tuple's
                 // variable-length part.
-                if !self
-                    .prenormalized_prefix_elements(db, self_prenormalize_variable)
+                let mut result = C::always_satisfiable(db);
+                let pairwise = (self.prenormalized_prefix_elements(db, self_prenormalize_variable))
                     .zip_longest(
                         other.prenormalized_prefix_elements(db, other_prenormalize_variable),
-                    )
-                    .all(|pair| match pair {
+                    );
+                for pair in pairwise {
+                    let pair_constraints = match pair {
                         EitherOrBoth::Both(self_ty, other_ty) => {
                             self_ty.has_relation_to_impl(db, other_ty, relation, visitor)
                         }
@@ -796,11 +836,15 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                         EitherOrBoth::Right(_) => {
                             // The rhs has a required element that the lhs is not guaranteed to
                             // provide.
-                            false
+                            return C::unsatisfiable(db);
                         }
-                    })
-                {
-                    return false;
+                    };
+                    if result
+                        .intersect(db, pair_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
+                    }
                 }
 
                 let self_suffix: Vec<_> = self
@@ -809,9 +853,9 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                 let other_suffix: Vec<_> = other
                     .prenormalized_suffix_elements(db, other_prenormalize_variable)
                     .collect();
-                if !(self_suffix.iter().rev())
-                    .zip_longest(other_suffix.iter().rev())
-                    .all(|pair| match pair {
+                let pairwise = (self_suffix.iter().rev()).zip_longest(other_suffix.iter().rev());
+                for pair in pairwise {
+                    let pair_constraints = match pair {
                         EitherOrBoth::Both(self_ty, other_ty) => {
                             self_ty.has_relation_to_impl(db, *other_ty, relation, visitor)
                         }
@@ -821,34 +865,54 @@ impl<'db> VariableLengthTuple<Type<'db>> {
                         EitherOrBoth::Right(_) => {
                             // The rhs has a required element that the lhs is not guaranteed to
                             // provide.
-                            false
+                            return C::unsatisfiable(db);
                         }
-                    })
-                {
-                    return false;
+                    };
+                    if result
+                        .intersect(db, pair_constraints)
+                        .is_never_satisfied(db)
+                    {
+                        return result;
+                    }
                 }
 
                 // And lastly, the variable-length portions must satisfy the relation.
-                self.variable
-                    .has_relation_to_impl(db, other.variable, relation, visitor)
+                result.and(db, || {
+                    self.variable
+                        .has_relation_to_impl(db, other.variable, relation, visitor)
+                })
             }
         }
     }
 
-    fn is_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        self.variable.is_equivalent_to(db, other.variable)
-            && (self.prenormalized_prefix_elements(db, None))
-                .zip_longest(other.prenormalized_prefix_elements(db, None))
-                .all(|pair| match pair {
-                    EitherOrBoth::Both(self_ty, other_ty) => self_ty.is_equivalent_to(db, other_ty),
-                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
-                })
-            && (self.prenormalized_suffix_elements(db, None))
-                .zip_longest(other.prenormalized_suffix_elements(db, None))
-                .all(|pair| match pair {
-                    EitherOrBoth::Both(self_ty, other_ty) => self_ty.is_equivalent_to(db, other_ty),
-                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
-                })
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Self,
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        self.variable
+            .is_equivalent_to_impl(db, other.variable, visitor)
+            .and(db, || {
+                (self.prenormalized_prefix_elements(db, None))
+                    .zip_longest(other.prenormalized_prefix_elements(db, None))
+                    .when_all(db, |pair| match pair {
+                        EitherOrBoth::Both(self_ty, other_ty) => {
+                            self_ty.is_equivalent_to_impl(db, other_ty, visitor)
+                        }
+                        EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => C::unsatisfiable(db),
+                    })
+            })
+            .and(db, || {
+                (self.prenormalized_suffix_elements(db, None))
+                    .zip_longest(other.prenormalized_suffix_elements(db, None))
+                    .when_all(db, |pair| match pair {
+                        EitherOrBoth::Both(self_ty, other_ty) => {
+                            self_ty.is_equivalent_to_impl(db, other_ty, visitor)
+                        }
+                        EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => C::unsatisfiable(db),
+                    })
+            })
     }
 }
 
@@ -1027,13 +1091,13 @@ impl<'db> Tuple<Type<'db>> {
         }
     }
 
-    fn has_relation_to_impl(
+    fn has_relation_to_impl<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: &Self,
         relation: TypeRelation,
-        visitor: &HasRelationToVisitor<'db>,
-    ) -> bool {
+        visitor: &HasRelationToVisitor<'db, C>,
+    ) -> C {
         match self {
             Tuple::Fixed(self_tuple) => {
                 self_tuple.has_relation_to_impl(db, other, relation, visitor)
@@ -1044,96 +1108,95 @@ impl<'db> Tuple<Type<'db>> {
         }
     }
 
-    fn is_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        match (self, other) {
-            (Tuple::Fixed(self_tuple), Tuple::Fixed(other_tuple)) => {
-                self_tuple.is_equivalent_to(db, other_tuple)
-            }
-            (Tuple::Variable(self_tuple), Tuple::Variable(other_tuple)) => {
-                self_tuple.is_equivalent_to(db, other_tuple)
-            }
-            (Tuple::Fixed(_), Tuple::Variable(_)) | (Tuple::Variable(_), Tuple::Fixed(_)) => false,
-        }
-    }
-
-    pub(super) fn is_disjoint_from_impl(
+    fn is_equivalent_to_impl<C: Constraints<'db>>(
         &self,
         db: &'db dyn Db,
         other: &Self,
-        visitor: &IsDisjointVisitor<'db>,
-    ) -> bool {
+        visitor: &IsEquivalentVisitor<'db, C>,
+    ) -> C {
+        match (self, other) {
+            (Tuple::Fixed(self_tuple), Tuple::Fixed(other_tuple)) => {
+                self_tuple.is_equivalent_to_impl(db, other_tuple, visitor)
+            }
+            (Tuple::Variable(self_tuple), Tuple::Variable(other_tuple)) => {
+                self_tuple.is_equivalent_to_impl(db, other_tuple, visitor)
+            }
+            (Tuple::Fixed(_), Tuple::Variable(_)) | (Tuple::Variable(_), Tuple::Fixed(_)) => {
+                C::unsatisfiable(db)
+            }
+        }
+    }
+
+    pub(super) fn is_disjoint_from_impl<C: Constraints<'db>>(
+        &self,
+        db: &'db dyn Db,
+        other: &Self,
+        visitor: &IsDisjointVisitor<'db, C>,
+    ) -> C {
         // Two tuples with an incompatible number of required elements must always be disjoint.
         let (self_min, self_max) = self.len().size_hint();
         let (other_min, other_max) = other.len().size_hint();
         if self_max.is_some_and(|max| max < other_min) {
-            return true;
+            return C::always_satisfiable(db);
         }
         if other_max.is_some_and(|max| max < self_min) {
-            return true;
+            return C::always_satisfiable(db);
         }
 
         // If any of the required elements are pairwise disjoint, the tuples are disjoint as well.
         #[allow(clippy::items_after_statements)]
-        fn any_disjoint<'s, 'db>(
+        fn any_disjoint<'s, 'db, C: Constraints<'db>>(
             db: &'db dyn Db,
             a: impl IntoIterator<Item = &'s Type<'db>>,
             b: impl IntoIterator<Item = &'s Type<'db>>,
-            visitor: &IsDisjointVisitor<'db>,
-        ) -> bool
+            visitor: &IsDisjointVisitor<'db, C>,
+        ) -> C
         where
             'db: 's,
         {
-            a.into_iter().zip(b).any(|(self_element, other_element)| {
+            (a.into_iter().zip(b)).when_any(db, |(self_element, other_element)| {
                 self_element.is_disjoint_from_impl(db, *other_element, visitor)
             })
         }
 
         match (self, other) {
             (Tuple::Fixed(self_tuple), Tuple::Fixed(other_tuple)) => {
-                if any_disjoint(db, self_tuple.elements(), other_tuple.elements(), visitor) {
-                    return true;
-                }
+                any_disjoint(db, self_tuple.elements(), other_tuple.elements(), visitor)
             }
 
-            (Tuple::Variable(self_tuple), Tuple::Variable(other_tuple)) => {
-                if any_disjoint(
-                    db,
-                    self_tuple.prefix_elements(),
-                    other_tuple.prefix_elements(),
-                    visitor,
-                ) {
-                    return true;
-                }
-                if any_disjoint(
+            // Note that we don't compare the variable-length portions; two pure homogeneous tuples
+            // `tuple[A, ...]` and `tuple[B, ...]` can never be disjoint even if A and B are
+            // disjoint, because `tuple[()]` would be assignable to both.
+            (Tuple::Variable(self_tuple), Tuple::Variable(other_tuple)) => any_disjoint(
+                db,
+                self_tuple.prefix_elements(),
+                other_tuple.prefix_elements(),
+                visitor,
+            )
+            .or(db, || {
+                any_disjoint(
                     db,
                     self_tuple.suffix_elements().rev(),
                     other_tuple.suffix_elements().rev(),
                     visitor,
-                ) {
-                    return true;
-                }
-            }
+                )
+            }),
 
             (Tuple::Fixed(fixed), Tuple::Variable(variable))
             | (Tuple::Variable(variable), Tuple::Fixed(fixed)) => {
-                if any_disjoint(db, fixed.elements(), variable.prefix_elements(), visitor) {
-                    return true;
-                }
-                if any_disjoint(
+                any_disjoint(db, fixed.elements(), variable.prefix_elements(), visitor).or(
                     db,
-                    fixed.elements().rev(),
-                    variable.suffix_elements().rev(),
-                    visitor,
-                ) {
-                    return true;
-                }
+                    || {
+                        any_disjoint(
+                            db,
+                            fixed.elements().rev(),
+                            variable.suffix_elements().rev(),
+                            visitor,
+                        )
+                    },
+                )
             }
         }
-
-        // Two pure homogeneous tuples `tuple[A, ...]` and `tuple[B, ...]` can never be
-        // disjoint even if A and B are disjoint, because `tuple[()]` would be assignable to
-        // both.
-        false
     }
 
     pub(crate) fn is_single_valued(&self, db: &'db dyn Db) -> bool {