diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
index 1a72da9464fe8..1da443c12f697 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md
@@ -45,31 +45,27 @@ def even_given_unsatisfiable_constraints():
 
 ## Type variables
 
-The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the
-question when considering a typevar, by translating the desired relationship into a constraint set.
+The interesting case is typevars. The other typing relationships all "punt" on the question when
+considering a typevar, by translating the desired relationship into a constraint set.
 
 ```py
 from typing import Any
 from ty_extensions import is_assignable_to, is_subtype_of
 
 def assignability[T]():
-    # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ bool]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ bool)]
     reveal_type(is_assignable_to(T, bool))
-    # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ int]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ int)]
     reveal_type(is_assignable_to(T, int))
-    # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability = *)]
     reveal_type(is_assignable_to(T, object))
 
 def subtyping[T]():
-    # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ bool]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ bool)]
     reveal_type(is_subtype_of(T, bool))
-    # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ int]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ int)]
     reveal_type(is_subtype_of(T, int))
-    # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping = *)]
     reveal_type(is_subtype_of(T, object))
 ```
 
@@ -88,49 +84,37 @@ class Contravariant[T]:
         pass
 
 def assignability[T]():
-    # aka [T@assignability ≤ object], which is always satisfiable
-    # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability = *)]
     reveal_type(is_assignable_to(T, Any))
 
-    # aka [Never ≤ T@assignability], which is always satisfiable
-    # revealed: ty_extensions.ConstraintSet[always]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability = *)]
     reveal_type(is_assignable_to(Any, T))
 
-    # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Covariant[object]]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ Covariant[object])]
     reveal_type(is_assignable_to(T, Covariant[Any]))
-    # TODO: revealed: ty_extensions.ConstraintSet[Covariant[Never] ≤ T@assignability]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(Covariant[Never] ≤ T@assignability)]
     reveal_type(is_assignable_to(Covariant[Any], T))
 
-    # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Contravariant[Never]]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ Contravariant[Never])]
     reveal_type(is_assignable_to(T, Contravariant[Any]))
-    # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[object] ≤ T@assignability]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(Contravariant[object] ≤ T@assignability)]
     reveal_type(is_assignable_to(Contravariant[Any], T))
 
 def subtyping[T]():
-    # aka [T@assignability ≤ object], which is always satisfiable
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping = Never)]
     reveal_type(is_subtype_of(T, Any))
 
-    # aka [Never ≤ T@assignability], which is always satisfiable
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping = object)]
     reveal_type(is_subtype_of(Any, T))
 
-    # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Covariant[Never]]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ Covariant[Never])]
     reveal_type(is_subtype_of(T, Covariant[Any]))
-    # TODO: revealed: ty_extensions.ConstraintSet[Covariant[object] ≤ T@subtyping]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(Covariant[object] ≤ T@subtyping)]
     reveal_type(is_subtype_of(Covariant[Any], T))
 
-    # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Contravariant[object]]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ Contravariant[object])]
     reveal_type(is_subtype_of(T, Contravariant[Any]))
-    # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[Never] ≤ T@subtyping]
-    # revealed: ty_extensions.ConstraintSet[never]
+    # revealed: ty_extensions.ConstraintSet[(Contravariant[Never] ≤ T@subtyping)]
     reveal_type(is_subtype_of(Contravariant[Any], T))
 ```
 
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
index 3ac4f9b65216c..79716ad19ad84 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
@@ -1248,14 +1248,10 @@ def identity[T](t: T) -> T:
 
 static_assert(is_assignable_to(TypeOf[identity], Callable[[int], int]))
 static_assert(is_assignable_to(TypeOf[identity], Callable[[str], str]))
-# TODO: no error
-# error: [static-assert-error]
 static_assert(not is_assignable_to(TypeOf[identity], Callable[[str], int]))
 
 static_assert(is_assignable_to(CallableTypeOf[identity], Callable[[int], int]))
 static_assert(is_assignable_to(CallableTypeOf[identity], Callable[[str], str]))
-# TODO: no error
-# error: [static-assert-error]
 static_assert(not is_assignable_to(CallableTypeOf[identity], Callable[[str], int]))
 ```
 
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
index a2b9ca89d01e1..c756ecf5f7387 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md
@@ -2221,23 +2221,11 @@ from ty_extensions import CallableTypeOf, TypeOf, is_subtype_of, static_assert
 def identity[T](t: T) -> T:
     return t
 
-# TODO: Confusingly, these are not the same results as the corresponding checks in
-# is_assignable_to.md, even though all of these types are fully static. We have some heuristics that
-# currently conflict with each other, that we are in the process of removing with the constraint set
-# work.
-# TODO: no error
-# error: [static-assert-error]
 static_assert(is_subtype_of(TypeOf[identity], Callable[[int], int]))
-# TODO: no error
-# error: [static-assert-error]
 static_assert(is_subtype_of(TypeOf[identity], Callable[[str], str]))
 static_assert(not is_subtype_of(TypeOf[identity], Callable[[str], int]))
 
-# TODO: no error
-# error: [static-assert-error]
 static_assert(is_subtype_of(CallableTypeOf[identity], Callable[[int], int]))
-# TODO: no error
-# error: [static-assert-error]
 static_assert(is_subtype_of(CallableTypeOf[identity], Callable[[str], str]))
 static_assert(not is_subtype_of(CallableTypeOf[identity], Callable[[str], int]))
 ```
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index 35574d16adef2..61773bf0543eb 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -1324,7 +1324,7 @@ impl<'db> Type<'db> {
         self.filter_union(db, |elem| {
             !elem
                 .when_disjoint_from(db, target, inferable)
-                .is_always_satisfied(db)
+                .satisfied_by_all_typevars(db, inferable)
         })
     }
 
@@ -1655,7 +1655,7 @@ impl<'db> Type<'db> {
     /// See [`TypeRelation::Subtyping`] for more details.
     pub(crate) fn is_subtype_of(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         self.when_subtype_of(db, target, InferableTypeVars::None)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     fn when_subtype_of(
@@ -1691,7 +1691,7 @@ impl<'db> Type<'db> {
     /// See `TypeRelation::Assignability` for more details.
     pub fn is_assignable_to(self, db: &'db dyn Db, target: Type<'db>) -> bool {
         self.when_assignable_to(db, target, InferableTypeVars::None)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     fn when_assignable_to(
@@ -1709,7 +1709,7 @@ impl<'db> Type<'db> {
     #[salsa::tracked(cycle_initial=is_redundant_with_cycle_initial, heap_size=ruff_memory_usage::heap_size)]
     pub(crate) fn is_redundant_with(self, db: &'db dyn Db, other: Type<'db>) -> bool {
         self.has_relation_to(db, other, InferableTypeVars::None, TypeRelation::Redundancy)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     fn has_relation_to(
@@ -1756,6 +1756,64 @@ impl<'db> Type<'db> {
         }
 
         match (self, target) {
+            // Pretend that instances of `dataclasses.Field` are assignable to their default type.
+            // This allows field definitions like `name: str = field(default="")` in dataclasses
+            // to pass the assignability check of the inferred type to the declared type.
+            (Type::KnownInstance(KnownInstanceType::Field(field)), right)
+                if relation.is_assignability() =>
+            {
+                field.default_type(db).when_none_or(|default_type| {
+                    default_type.has_relation_to_impl(
+                        db,
+                        right,
+                        inferable,
+                        relation,
+                        relation_visitor,
+                        disjointness_visitor,
+                    )
+                })
+            }
+
+            // Two identical typevars must always solve to the same type, so they are always
+            // subtypes of each other and assignable to each other.
+            //
+            // Note that this is not handled by the early return at the beginning of this method,
+            // since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive.
+            (Type::TypeVar(lhs_bound_typevar), Type::TypeVar(rhs_bound_typevar))
+                if lhs_bound_typevar.is_same_typevar_as(db, rhs_bound_typevar) =>
+            {
+                ConstraintSet::from(true)
+            }
+
+            // Typevars with non-fully-static bounds or constraints do not participate in
+            // subtyping while they are in a non-inferable position.
+            (Type::TypeVar(bound_typevar), _)
+                if relation.is_subtyping()
+                    && !bound_typevar.is_inferable(db, inferable)
+                    && !bound_typevar.has_fully_static_bound_or_constraints(db) =>
+            {
+                ConstraintSet::from(false)
+            }
+            (_, Type::TypeVar(bound_typevar))
+                if relation.is_subtyping()
+                    && !bound_typevar.is_inferable(db, inferable)
+                    && !bound_typevar.has_fully_static_bound_or_constraints(db) =>
+            {
+                ConstraintSet::from(false)
+            }
+
+            // A typevar satisfies a relation when...it satisfies the relation. Yes that's a
+            // tautology! We're moving the caller's subtyping/assignability requirement into a
+            // constraint set. If the typevar has an upper bound or constraints, then the relation
+            // only has to hold when the typevar has a valid specialization (i.e., one that
+            // satisfies the upper bound/constraints).
+            (Type::TypeVar(bound_typevar), _) => {
+                ConstraintSet::constrain_typevar(db, bound_typevar, Type::Never, target, relation)
+            }
+            (_, Type::TypeVar(bound_typevar)) => {
+                ConstraintSet::constrain_typevar(db, bound_typevar, self, Type::object(), relation)
+            }
+
             // Everything is a subtype of `object`.
             (_, Type::NominalInstance(instance)) if instance.is_object() => {
                 ConstraintSet::from(true)
@@ -1802,24 +1860,6 @@ impl<'db> Type<'db> {
                 })
             }
 
-            // Pretend that instances of `dataclasses.Field` are assignable to their default type.
-            // This allows field definitions like `name: str = field(default="")` in dataclasses
-            // to pass the assignability check of the inferred type to the declared type.
-            (Type::KnownInstance(KnownInstanceType::Field(field)), right)
-                if relation.is_assignability() =>
-            {
-                field.default_type(db).when_none_or(|default_type| {
-                    default_type.has_relation_to_impl(
-                        db,
-                        right,
-                        inferable,
-                        relation,
-                        relation_visitor,
-                        disjointness_visitor,
-                    )
-                })
-            }
-
             // Dynamic is only a subtype of `object` and only a supertype of `Never`; both were
             // handled above. It's always assignable, though.
             //
@@ -1859,130 +1899,6 @@ impl<'db> Type<'db> {
                 },
             }),
 
-            // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied:
-            // 1. `T` is a bound TypeVar and `T`'s upper bound is a subtype of `S`.
-            //    TypeVars without an explicit upper bound are treated as having an implicit upper bound of `object`.
-            // 2. `T` is a constrained TypeVar and all of `T`'s constraints are subtypes of `S`.
-            //
-            // However, there is one exception to this general rule: for any given typevar `T`,
-            // `T` will always be a subtype of any union containing `T`.
-            // A similar rule applies in reverse to intersection types.
-            (Type::TypeVar(bound_typevar), Type::Union(union))
-                if !bound_typevar.is_inferable(db, inferable)
-                    && union.elements(db).contains(&self) =>
-            {
-                ConstraintSet::from(true)
-            }
-            (Type::Intersection(intersection), Type::TypeVar(bound_typevar))
-                if !bound_typevar.is_inferable(db, inferable)
-                    && intersection.positive(db).contains(&target) =>
-            {
-                ConstraintSet::from(true)
-            }
-            (Type::Intersection(intersection), Type::TypeVar(bound_typevar))
-                if !bound_typevar.is_inferable(db, inferable)
-                    && intersection.negative(db).contains(&target) =>
-            {
-                ConstraintSet::from(false)
-            }
-
-            // Two identical typevars must always solve to the same type, so they are always
-            // subtypes of each other and assignable to each other.
-            //
-            // Note that this is not handled by the early return at the beginning of this method,
-            // since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive.
-            (Type::TypeVar(lhs_bound_typevar), Type::TypeVar(rhs_bound_typevar))
-                if !lhs_bound_typevar.is_inferable(db, inferable)
-                    && lhs_bound_typevar.is_same_typevar_as(db, rhs_bound_typevar) =>
-            {
-                ConstraintSet::from(true)
-            }
-
-            // 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
-            // implicit upper bound of `object` (which is handled above).
-            (Type::TypeVar(bound_typevar), _)
-                if !bound_typevar.is_inferable(db, inferable)
-                    && bound_typevar.typevar(db).bound_or_constraints(db).is_some() =>
-            {
-                match bound_typevar.typevar(db).bound_or_constraints(db) {
-                    None => unreachable!(),
-                    Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound
-                        .has_relation_to_impl(
-                            db,
-                            target,
-                            inferable,
-                            relation,
-                            relation_visitor,
-                            disjointness_visitor,
-                        ),
-                    Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                        constraints.elements(db).iter().when_all(db, |constraint| {
-                            constraint.has_relation_to_impl(
-                                db,
-                                target,
-                                inferable,
-                                relation,
-                                relation_visitor,
-                                disjointness_visitor,
-                            )
-                        })
-                    }
-                }
-            }
-
-            // If the typevar is constrained, there must be multiple constraints, and the typevar
-            // 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::TypeVar(bound_typevar))
-                if !bound_typevar.is_inferable(db, inferable)
-                    && !bound_typevar
-                        .typevar(db)
-                        .constraints(db)
-                        .when_some_and(|constraints| {
-                            constraints.iter().when_all(db, |constraint| {
-                                self.has_relation_to_impl(
-                                    db,
-                                    *constraint,
-                                    inferable,
-                                    relation,
-                                    relation_visitor,
-                                    disjointness_visitor,
-                                )
-                            })
-                        })
-                        .is_never_satisfied(db) =>
-            {
-                // TODO: The repetition here isn't great, but we really need the fallthrough logic,
-                // where this arm only engages if it returns true (or in the world of constraints,
-                // 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(|constraints| {
-                        constraints.iter().when_all(db, |constraint| {
-                            self.has_relation_to_impl(
-                                db,
-                                *constraint,
-                                inferable,
-                                relation,
-                                relation_visitor,
-                                disjointness_visitor,
-                            )
-                        })
-                    })
-            }
-
-            (Type::TypeVar(bound_typevar), _) if bound_typevar.is_inferable(db, inferable) => {
-                // The implicit lower bound of a typevar is `Never`, which means
-                // that it is always assignable to any other type.
-
-                // TODO: record the unification constraints
-
-                ConstraintSet::from(true)
-            }
-
             // `Never` is the bottom type, the empty set.
             (_, Type::Never) => ConstraintSet::from(false),
 
@@ -2074,55 +1990,6 @@ impl<'db> Type<'db> {
                 })
             }
 
-            // 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::TypeVar(bound_typevar)) if !bound_typevar.is_inferable(db, inferable) => {
-                ConstraintSet::from(false)
-            }
-
-            (_, Type::TypeVar(typevar))
-                if typevar.is_inferable(db, inferable)
-                    && relation.is_assignability()
-                    && typevar.typevar(db).upper_bound(db).is_none_or(|bound| {
-                        !self
-                            .has_relation_to_impl(
-                                db,
-                                bound,
-                                inferable,
-                                relation,
-                                relation_visitor,
-                                disjointness_visitor,
-                            )
-                            .is_never_satisfied(db)
-                    }) =>
-            {
-                // TODO: record the unification constraints
-
-                typevar.typevar(db).upper_bound(db).when_none_or(|bound| {
-                    self.has_relation_to_impl(
-                        db,
-                        bound,
-                        inferable,
-                        relation,
-                        relation_visitor,
-                        disjointness_visitor,
-                    )
-                })
-            }
-
-            // TODO: Infer specializations here
-            (_, Type::TypeVar(bound_typevar)) if bound_typevar.is_inferable(db, inferable) => {
-                ConstraintSet::from(false)
-            }
-            (Type::TypeVar(bound_typevar), _) => {
-                // All inferable cases should have been handled above
-                assert!(!bound_typevar.is_inferable(db, inferable));
-                ConstraintSet::from(false)
-            }
-
             // 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) => ConstraintSet::from(left.bool(db).is_always_false()),
@@ -2141,12 +2008,12 @@ impl<'db> Type<'db> {
                 self_function.has_relation_to_impl(
                     db,
                     target_function,
-                    inferable,
-                    relation,
-                    relation_visitor,
-                    disjointness_visitor,
-                )
-            }
+                inferable,
+                relation,
+                relation_visitor,
+                disjointness_visitor,
+            )
+        }
             (Type::BoundMethod(self_method), Type::BoundMethod(target_method)) => self_method
                 .has_relation_to_impl(
                     db,
@@ -2620,7 +2487,7 @@ impl<'db> Type<'db> {
     /// [equivalent to]: https://typing.python.org/en/latest/spec/glossary.html#term-equivalent
     pub(crate) fn is_equivalent_to(self, db: &'db dyn Db, other: Type<'db>) -> bool {
         self.when_equivalent_to(db, other, InferableTypeVars::None)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     fn when_equivalent_to(
@@ -2747,7 +2614,7 @@ impl<'db> Type<'db> {
     /// `false` answers in some cases.
     pub(crate) fn is_disjoint_from(self, db: &'db dyn Db, other: Type<'db>) -> bool {
         self.when_disjoint_from(db, other, InferableTypeVars::None)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     fn when_disjoint_from(
@@ -5009,7 +4876,7 @@ impl<'db> Type<'db> {
 
             Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked_set)) => {
                 let constraints = tracked_set.constraints(db);
-                Truthiness::from(constraints.is_always_satisfied(db))
+                Truthiness::from(constraints.satisfied_by_all_typevars(db, InferableTypeVars::None))
             }
 
             Type::FunctionLiteral(_)
@@ -8287,7 +8154,9 @@ impl<'db> KnownInstanceType<'db> {
                         Ok(())
                     }
                     KnownInstanceType::ConstraintSet(tracked_set) => {
-                        let constraints = tracked_set.constraints(self.db);
+                        let constraints = tracked_set
+                            .constraints(self.db)
+                            .limit_to_valid_specializations(self.db);
                         write!(
                             f,
                             "ty_extensions.ConstraintSet[{}]",
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index c4aac0bb9631a..890bdb8570e60 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -1658,7 +1658,7 @@ impl<'db> CallableBinding<'db> {
                         .unwrap_or(Type::unknown());
                     if argument_type
                         .when_assignable_to(db, parameter_type, overload.inferable_typevars)
-                        .is_always_satisfied(db)
+                        .satisfied_by_all_typevars(db, overload.inferable_typevars)
                     {
                         is_argument_assignable_to_any_overload = true;
                         break 'overload;
@@ -1888,7 +1888,7 @@ impl<'db> CallableBinding<'db> {
                                 current_parameter_type,
                                 overload.inferable_typevars,
                             )
-                            .is_always_satisfied(db)
+                            .satisfied_by_all_typevars(db, overload.inferable_typevars)
                         {
                             participating_parameter_indexes.insert(parameter_index);
                         }
@@ -2011,7 +2011,7 @@ impl<'db> CallableBinding<'db> {
                             first_overload_return_type,
                             overload.inferable_typevars,
                         )
-                        .is_always_satisfied(db)
+                        .satisfied_by_all_typevars(db, overload.inferable_typevars)
                 })
             } else {
                 // No matching overload
@@ -2974,15 +2974,12 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                 argument_type = argument_type.apply_specialization(self.db, specialization);
                 expected_ty = expected_ty.apply_specialization(self.db, specialization);
             }
-            // This is one of the few places where we want to check if there's _any_ specialization
-            // where assignability holds; normally we want to check that assignability holds for
-            // _all_ specializations.
             // TODO: Soon we will go further, and build the actual specializations from the
             // constraint set that we get from this assignability check, instead of inferring and
             // building them in an earlier separate step.
-            if argument_type
+            if !argument_type
                 .when_assignable_to(self.db, expected_ty, self.inferable_typevars)
-                .is_never_satisfied(self.db)
+                .satisfied_by_all_typevars(self.db, self.inferable_typevars)
             {
                 let positional = matches!(argument, Argument::Positional | Argument::Synthetic)
                     && !parameter.is_variadic();
@@ -3116,7 +3113,7 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     KnownClass::Str.to_instance(self.db),
                     self.inferable_typevars,
                 )
-                .is_always_satisfied(self.db)
+                .satisfied_by_all_typevars(self.db, self.inferable_typevars)
             {
                 self.errors.push(BindingError::InvalidKeyType {
                     argument_index: adjusted_argument_index,
diff --git a/crates/ty_python_semantic/src/types/class.rs b/crates/ty_python_semantic/src/types/class.rs
index 002fcba574671..bcc79b8087946 100644
--- a/crates/ty_python_semantic/src/types/class.rs
+++ b/crates/ty_python_semantic/src/types/class.rs
@@ -527,7 +527,7 @@ impl<'db> ClassType<'db> {
     /// Return `true` if `other` is present in this class's MRO.
     pub(super) fn is_subclass_of(self, db: &'db dyn Db, other: ClassType<'db>) -> bool {
         self.when_subclass_of(db, other, InferableTypeVars::None)
-            .is_always_satisfied(db)
+            .satisfied_by_all_typevars(db, InferableTypeVars::None)
     }
 
     pub(super) fn when_subclass_of(
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index a64099352b33c..96b881a482abb 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -345,6 +345,17 @@ impl<'db> ConstraintSet<'db> {
         self.node.satisfied_by_all_typevars(db, inferable)
     }
 
+    /// Returns a new constraint set that ensures that all typevars mentioned in the current
+    /// constraint set have valid specializations, according to any upper bound or constraints they
+    /// might have.
+    pub(crate) fn limit_to_valid_specializations(self, db: &'db dyn Db) -> Self {
+        let mut result = self;
+        self.node.for_each_constraint(db, &mut |constraint| {
+            result.intersect(db, constraint.typevar(db).valid_specializations(db));
+        });
+        result
+    }
+
     /// Updates this constraint set to hold the union of itself and another constraint set.
     pub(crate) fn union(&mut self, db: &'db dyn Db, other: Self) -> Self {
         self.node = self.node.or(db, other.node);
@@ -1031,65 +1042,41 @@ impl<'db> Node<'db> {
         db: &'db dyn Db,
         inferable: InferableTypeVars<'_, 'db>,
     ) -> bool {
-        match self {
+        let interior = match self {
             Node::AlwaysTrue => return true,
             Node::AlwaysFalse => return false,
-            Node::Interior(_) => {}
-        }
-
-        let mut typevars = FxHashSet::default();
-        self.for_each_constraint(db, &mut |constraint| {
-            typevars.insert(constraint.typevar(db));
-        });
-
-        // Returns if some specialization satisfies this constraint set.
-        let some_specialization_satisfies = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
-            !when_satisfied.is_never_satisfied(db)
-        };
-
-        // Returns if all specializations satisfy this constraint set.
-        let all_specializations_satisfy = move |specializations: Node<'db>| {
-            let when_satisfied = specializations.implies(db, self).and(db, specializations);
-            when_satisfied
-                .iff(db, specializations)
-                .is_always_satisfied(db)
+            Node::Interior(interior) => interior,
         };
 
-        for typevar in typevars {
-            if typevar.is_inferable(db, inferable) {
-                // If the typevar is in inferable position, we need to verify that some valid
-                // specialization satisfies the constraint set.
-                let valid_specializations = typevar.valid_specializations(db);
-                if !some_specialization_satisfies(valid_specializations) {
-                    return false;
-                }
+        let mut valid_inferable_specializations = Node::AlwaysTrue;
+        let mut valid_non_inferable_specializations = Node::AlwaysTrue;
+        let mut add_typevar = |bound_typevar: BoundTypeVarInstance<'db>| {
+            if bound_typevar.is_inferable(db, inferable) {
+                let valid_specializations =
+                    bound_typevar.valid_specializations_with_materialization(db, true);
+                valid_inferable_specializations =
+                    valid_inferable_specializations.and(db, valid_specializations);
             } else {
-                // If the typevar is in non-inferable position, we need to verify that all required
-                // specializations satisfy the constraint set. Complicating things, the typevar
-                // might have gradual constraints. For those, we need to know the range of valid
-                // materializations, but we only need some materialization to satisfy the
-                // constraint set.
-                //
-                // NB: We could also model this by introducing a synthetic typevar for the gradual
-                // constraint, treating that synthetic typevar as always inferable (so that we only
-                // need to verify for some materialization), and then update this typevar's
-                // constraint to refer to the synthetic typevar instead of the original gradual
-                // constraint.
-                let (static_specializations, gradual_constraints) =
-                    typevar.required_specializations(db);
-                if !all_specializations_satisfy(static_specializations) {
-                    return false;
-                }
-                for gradual_constraint in gradual_constraints {
-                    if !some_specialization_satisfies(gradual_constraint) {
-                        return false;
-                    }
-                }
+                let valid_specializations =
+                    bound_typevar.valid_specializations_with_materialization(db, false);
+                valid_non_inferable_specializations =
+                    valid_non_inferable_specializations.and(db, valid_specializations);
             }
-        }
+        };
+        self.for_each_constraint(db, &mut |constraint| {
+            add_typevar(constraint.typevar(db));
+            if let Type::TypeVar(bound_typevar) = constraint.lower(db) {
+                add_typevar(bound_typevar);
+            }
+            if let Type::TypeVar(bound_typevar) = constraint.upper(db) {
+                add_typevar(bound_typevar);
+            }
+        });
 
-        true
+        let restricted = self.and(db, valid_inferable_specializations);
+        let restricted = restricted.exists(db, inferable.iter());
+        let restricted = valid_non_inferable_specializations.implies(db, restricted);
+        restricted.is_always_satisfied(db)
     }
 
     /// Returns a new BDD that is the _existential abstraction_ of `self` for a set of typevars.
@@ -2287,6 +2274,12 @@ struct SequentMap<'db> {
     >,
     /// Sequents of the form `C → D`
     single_implications: FxHashMap<ConstrainedTypeVar<'db>, FxHashSet<ConstrainedTypeVar<'db>>>,
+
+    /// A dependency map recording which typevars depend on each other. (A typevar `T` depends on a
+    /// typevar `U` if there is any constraint `T ≤ U` or `U ≤ T` in the constraint set.)
+    typevar_dependencies:
+        FxHashMap<BoundTypeVarIdentity<'db>, FxHashSet<BoundTypeVarIdentity<'db>>>,
+
     /// Constraints that we have already processed
     processed: FxHashSet<ConstrainedTypeVar<'db>>,
     /// Constraints that enqueued to be processed
@@ -2294,6 +2287,18 @@ struct SequentMap<'db> {
 }
 
 impl<'db> SequentMap<'db> {
+    fn get_typevar_dependencies(
+        &self,
+        bound_typevar: BoundTypeVarIdentity<'db>,
+    ) -> impl Iterator<Item = BoundTypeVarIdentity<'db>> + '_ {
+        self.typevar_dependencies
+            .get(&bound_typevar)
+            .map(|dependencies| dependencies.into_iter())
+            .into_iter()
+            .flatten()
+            .copied()
+    }
+
     fn add(&mut self, db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) {
         self.enqueue_constraint(constraint);
 
@@ -2383,6 +2388,22 @@ impl<'db> SequentMap<'db> {
             .insert(post);
     }
 
+    fn add_typevar_dependency(
+        &mut self,
+        left: BoundTypeVarIdentity<'db>,
+        right: BoundTypeVarIdentity<'db>,
+    ) {
+        // The typevar dependency map is reflexive, so add the dependency in both directions.
+        self.typevar_dependencies
+            .entry(left)
+            .or_default()
+            .insert(right);
+        self.typevar_dependencies
+            .entry(right)
+            .or_default()
+            .insert(left);
+    }
+
     fn add_sequents_for_single(&mut self, db: &'db dyn Db, constraint: ConstrainedTypeVar<'db>) {
         // If this constraint binds its typevar to `Never ≤ T ≤ object`, then the typevar can take
         // on any type, and the constraint is always satisfied.
@@ -2403,9 +2424,14 @@ impl<'db> SequentMap<'db> {
         // Technically, (1) also allows `(S = T) → (S = S)`, but the rhs of that is vacuously true,
         // so we don't add a sequent for that case.
 
+        let typevar = constraint.typevar(db);
+        let lower = constraint.lower(db);
+        let upper = constraint.upper(db);
         let post_constraint = match (lower, upper) {
             // Case 1
             (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar)) => {
+                self.add_typevar_dependency(typevar.identity(db), lower_typevar.identity(db));
+                self.add_typevar_dependency(typevar.identity(db), upper_typevar.identity(db));
                 if !lower_typevar.is_same_typevar_as(db, upper_typevar) {
                     ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper)
                 } else {
@@ -2415,11 +2441,13 @@ impl<'db> SequentMap<'db> {
 
             // Case 2
             (Type::TypeVar(lower_typevar), _) => {
+                self.add_typevar_dependency(typevar.identity(db), lower_typevar.identity(db));
                 ConstrainedTypeVar::new(db, lower_typevar, Type::Never, upper)
             }
 
             // Case 3
             (_, Type::TypeVar(upper_typevar)) => {
+                self.add_typevar_dependency(typevar.identity(db), upper_typevar.identity(db));
                 ConstrainedTypeVar::new(db, upper_typevar, lower, Type::object())
             }
 
@@ -2554,17 +2582,36 @@ impl<'db> SequentMap<'db> {
                 let left_upper = left_constraint.upper(db);
                 let right_lower = right_constraint.lower(db);
                 let right_upper = right_constraint.upper(db);
+                let new_constraint = |bound_typevar: BoundTypeVarInstance<'db>,
+                                      right_lower: Type<'db>,
+                                      right_upper: Type<'db>| {
+                    let right_lower = if let Type::TypeVar(other_bound_typevar) = right_lower
+                        && bound_typevar.is_same_typevar_as(db, other_bound_typevar)
+                    {
+                        Type::Never
+                    } else {
+                        right_lower
+                    };
+                    let right_upper = if let Type::TypeVar(other_bound_typevar) = right_upper
+                        && bound_typevar.is_same_typevar_as(db, other_bound_typevar)
+                    {
+                        Type::object()
+                    } else {
+                        right_upper
+                    };
+                    ConstrainedTypeVar::new(db, bound_typevar, right_lower, right_upper)
+                };
                 let post_constraint = match (left_lower, left_upper) {
                     (Type::TypeVar(bound_typevar), Type::TypeVar(other_bound_typevar))
                         if bound_typevar.is_same_typevar_as(db, other_bound_typevar) =>
                     {
-                        ConstrainedTypeVar::new(db, bound_typevar, right_lower, right_upper)
+                        new_constraint(bound_typevar, right_lower, right_upper)
                     }
                     (Type::TypeVar(bound_typevar), _) => {
-                        ConstrainedTypeVar::new(db, bound_typevar, Type::Never, right_upper)
+                        new_constraint(bound_typevar, Type::Never, right_upper)
                     }
                     (_, Type::TypeVar(bound_typevar)) => {
-                        ConstrainedTypeVar::new(db, bound_typevar, right_lower, Type::object())
+                        new_constraint(bound_typevar, right_lower, Type::object())
                     }
                     _ => return,
                 };
@@ -3030,7 +3077,24 @@ impl<'db> BoundTypeVarInstance<'db> {
     /// Returns the valid specializations of a typevar. This is used when checking a constraint set
     /// when this typevar is in inferable position, where we only need _some_ specialization to
     /// satisfy the constraint set.
-    fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> {
+    pub(crate) fn valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> {
+        let node = self.valid_specializations_with_materialization(db, true);
+        ConstraintSet { node }
+    }
+
+    /// Returns the valid specializations of a typevar, choosing whether to use the top or bottom
+    /// materialization of any gradual types that appear in the bounds or constraints.
+    ///
+    /// For inferable typevars we want the most permissive view of gradual types (top
+    /// materialization), so that we succeed if there exists _any_ materialization that works.
+    /// For non-inferable typevars we want the most restrictive view (bottom materialization), so
+    /// that we only consider the specializations that are guaranteed to be valid regardless of how
+    /// the gradual type is materialized.
+    fn valid_specializations_with_materialization(
+        self,
+        db: &'db dyn Db,
+        use_top_materialization: bool,
+    ) -> Node<'db> {
         // For gradual upper bounds and constraints, we are free to choose any materialization that
         // makes the check succeed. In inferable positions, it is most helpful to choose a
         // materialization that is as permissive as possible, since that maximizes the number of
@@ -3044,14 +3108,33 @@ impl<'db> BoundTypeVarInstance<'db> {
         match self.typevar(db).bound_or_constraints(db) {
             None => Node::AlwaysTrue,
             Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
-                let bound = bound.top_materialization(db);
+                let bound = if use_top_materialization {
+                    bound.top_materialization(db)
+                } else {
+                    bound.bottom_materialization(db)
+                };
                 ConstrainedTypeVar::new_node(db, self, Type::Never, bound)
             }
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
                 let mut specializations = Node::AlwaysFalse;
                 for constraint in constraints.elements(db) {
-                    let constraint_lower = constraint.bottom_materialization(db);
-                    let constraint_upper = constraint.top_materialization(db);
+                    let (constraint_lower, constraint_upper) = if use_top_materialization {
+                        (
+                            constraint.bottom_materialization(db),
+                            constraint.top_materialization(db),
+                        )
+                    } else {
+                        // For non-inferable typevars, we still have to consider all of the
+                        // explicitly-declared constraints. Keep the range of materializations
+                        // to avoid dropping permissive gradual constraints while staying fully
+                        // static. Reversing the order ensures that gradual constraints (like `Any`)
+                        // don't blow the valid-specialization set wide open for non-inferable
+                        // typevars.
+                        (
+                            constraint.top_materialization(db),
+                            constraint.bottom_materialization(db),
+                        )
+                    };
                     specializations = specializations.or(
                         db,
                         ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper),
@@ -3131,7 +3214,7 @@ impl<'db> GenericContext<'db> {
         let abstracted = self
             .variables(db)
             .fold(constraints.node, |constraints, bound_typevar| {
-                constraints.and(db, bound_typevar.valid_specializations(db))
+                constraints.and(db, bound_typevar.valid_specializations(db).node)
             });
 
         // Then we find all of the "representative types" for each typevar in the constraint set.
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 060341339686c..a9f0fc6c8e81a 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -128,7 +128,7 @@ pub(crate) enum InferableTypeVars<'a, 'db> {
     ),
 }
 
-impl<'db> BoundTypeVarInstance<'db> {
+impl<'db> BoundTypeVarIdentity<'db> {
     pub(crate) fn is_inferable(
         self,
         db: &'db dyn Db,
@@ -136,7 +136,7 @@ impl<'db> BoundTypeVarInstance<'db> {
     ) -> bool {
         match inferable {
             InferableTypeVars::None => false,
-            InferableTypeVars::One(typevars) => typevars.contains(&self.identity(db)),
+            InferableTypeVars::One(typevars) => typevars.contains(&self),
             InferableTypeVars::Two(left, right) => {
                 self.is_inferable(db, *left) || self.is_inferable(db, *right)
             }
@@ -144,6 +144,34 @@ impl<'db> BoundTypeVarInstance<'db> {
     }
 }
 
+impl<'db> BoundTypeVarInstance<'db> {
+    pub(crate) fn is_inferable(
+        self,
+        db: &'db dyn Db,
+        inferable: InferableTypeVars<'_, 'db>,
+    ) -> bool {
+        self.identity(db).is_inferable(db, inferable)
+    }
+
+    /// Returns `true` if all bounds or constraints on this typevar are fully static.
+    ///
+    /// A type is fully static if its top and bottom materializations are the same; dynamic types
+    /// (like `Any`) will have different materializations.
+    pub(crate) fn has_fully_static_bound_or_constraints(self, db: &'db dyn Db) -> bool {
+        match self.typevar(db).bound_or_constraints(db) {
+            None => true,
+            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                bound.top_materialization(db) == bound.bottom_materialization(db)
+            }
+            Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
+                constraints.elements(db).iter().all(|constraint| {
+                    constraint.top_materialization(db) == constraint.bottom_materialization(db)
+                })
+            }
+        }
+    }
+}
+
 impl<'a, 'db> InferableTypeVars<'a, 'db> {
     pub(crate) fn merge(&'a self, other: &'a InferableTypeVars<'a, 'db>) -> Self {
         match (self, other) {
@@ -1511,7 +1539,7 @@ impl<'db> SpecializationBuilder<'db> {
                     let assignable_elements = (formal.elements(self.db).iter()).filter(|ty| {
                         actual
                             .when_subtype_of(self.db, **ty, self.inferable)
-                            .is_always_satisfied(self.db)
+                            .satisfied_by_all_typevars(self.db, self.inferable)
                     });
                     if assignable_elements.exactly_one().is_ok() {
                         return Ok(());
@@ -1521,6 +1549,20 @@ impl<'db> SpecializationBuilder<'db> {
                 let bound_typevars =
                     (formal.elements(self.db).iter()).filter_map(|ty| ty.as_typevar());
                 if let Ok(bound_typevar) = bound_typevars.exactly_one() {
+                    // If the actual argument can be satisfied by a non-typevar element of the
+                    // union, then prefer that element and avoid inferring a mapping for the
+                    // typevar. This lets other occurrences of the typevar (if any) drive the
+                    // specialization instead of opportunistically binding it here.
+                    let matches_non_typevar = formal.elements(self.db).iter().any(|ty| {
+                        !ty.has_typevar(self.db)
+                            && actual
+                                .when_subtype_of(self.db, *ty, self.inferable)
+                                .satisfied_by_all_typevars(self.db, self.inferable)
+                    });
+                    if matches_non_typevar {
+                        return Ok(());
+                    }
+
                     self.add_type_mapping(bound_typevar, actual, polarity, f);
                 }
             }
@@ -1542,7 +1584,7 @@ impl<'db> SpecializationBuilder<'db> {
                     Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
                         if !ty
                             .when_assignable_to(self.db, bound, self.inferable)
-                            .is_always_satisfied(self.db)
+                            .satisfied_by_all_typevars(self.db, self.inferable)
                         {
                             return Err(SpecializationError::MismatchedBound {
                                 bound_typevar,
@@ -1563,7 +1605,7 @@ impl<'db> SpecializationBuilder<'db> {
                         for constraint in constraints.elements(self.db) {
                             if ty
                                 .when_assignable_to(self.db, *constraint, self.inferable)
-                                .is_always_satisfied(self.db)
+                                .satisfied_by_all_typevars(self.db, self.inferable)
                             {
                                 self.add_type_mapping(bound_typevar, *constraint, polarity, f);
                                 return Ok(());
diff --git a/crates/ty_python_semantic/src/types/instance.rs b/crates/ty_python_semantic/src/types/instance.rs
index 04a560be83756..0fa82bbbccd49 100644
--- a/crates/ty_python_semantic/src/types/instance.rs
+++ b/crates/ty_python_semantic/src/types/instance.rs
@@ -679,7 +679,7 @@ impl<'db> ProtocolInstanceType<'db> {
                     &HasRelationToVisitor::default(),
                     &IsDisjointVisitor::default(),
                 )
-                .is_always_satisfied(db)
+                .satisfied_by_all_typevars(db, InferableTypeVars::None)
         }
 
         fn initial<'db>(
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index 0460f31f08d3b..4885558de7ef8 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -829,6 +829,7 @@ impl<'db> Signature<'db> {
             relation_visitor,
             disjointness_visitor,
         );
+        let when = when.limit_to_valid_specializations(db);
 
         // But the caller does not need to consider those extra typevars. Whatever constraint set
         // we produce, we reduce it back down to the inferable set that the caller asked about.