diff --git a/crates/ty_python_semantic/resources/mdtest/bidirectional.md b/crates/ty_python_semantic/resources/mdtest/bidirectional.md
index 2cc55132621af..f6ad334c15e42 100644
--- a/crates/ty_python_semantic/resources/mdtest/bidirectional.md
+++ b/crates/ty_python_semantic/resources/mdtest/bidirectional.md
@@ -235,7 +235,9 @@ def _(xy: X | Y):
 The type context of all matching overloads are considered during argument inference:
 
 ```py
-from typing import overload, TypedDict
+from concurrent.futures import Future
+from os.path import abspath
+from typing import Awaitable, Callable, TypeVar, Union, overload, TypedDict
 
 def int_or_str() -> int | str:
     raise NotImplementedError
@@ -330,6 +332,24 @@ def f7(y: object) -> object:
 # TODO: We should reveal `list[int | str]` here.
 x9 = f7(reveal_type(["Sheet1"]))  # revealed: list[str]
 reveal_type(x9)  # revealed: list[int | str]
+
+# TODO: We should not error here once call inference can conjoin constraints
+# from all call arguments.
+def f8(xs: tuple[str, ...]) -> tuple[str, ...]:
+    # error: [invalid-return-type]
+    return tuple(map(abspath, xs))
+
+T2 = TypeVar("T2")
+
+def sink(func: Callable[[], Union[Awaitable[T2], T2]], future: Future[T2]) -> None:
+    raise NotImplementedError
+
+# TODO: This should not error once we conjoin constraints from all call arguments.
+def f9(func: Callable[[], Union[Awaitable[T2], T2]]) -> Future[T2]:
+    future: Future[T2] = Future()
+    # error: [invalid-argument-type]
+    sink(func, future)
+    return future
 ```
 
 ## Class constructor parameters
diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md
index 956105c723d35..7040433ea8763 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/functions.md
@@ -514,22 +514,98 @@ reveal_type(g(f("a")))  # revealed: tuple[Literal["a"], int] | None
 
 ## Passing generic functions to generic functions
 
-```py
+`functions.pyi`:
+
+```pyi
 from typing import Callable
 
-def invoke[A, B](fn: Callable[[A], B], value: A) -> B:
-    return fn(value)
+def invoke[A, B](fn: Callable[[A], B], value: A) -> B: ...
+def identity[T](x: T) -> T: ...
 
-def identity[T](x: T) -> T:
-    return x
+class Covariant[T]:
+    def get(self) -> T:
+        raise NotImplementedError
 
-def head[T](xs: list[T]) -> T:
-    return xs[0]
+def head_covariant[T](xs: Covariant[T]) -> T: ...
+def lift_covariant[T](xs: T) -> Covariant[T]: ...
+
+class Contravariant[T]:
+    def receive(self, input: T): ...
+
+def head_contravariant[T](xs: Contravariant[T]) -> T: ...
+def lift_contravariant[T](xs: T) -> Contravariant[T]: ...
+
+class Invariant[T]:
+    mutable_attribute: T
+
+def head_invariant[T](xs: Invariant[T]) -> T: ...
+def lift_invariant[T](xs: T) -> Invariant[T]: ...
+```
+
+A simple function that passes through its parameter type unchanged:
+
+`simple.py`:
+
+```py
+from functions import invoke, identity
 
 reveal_type(invoke(identity, 1))  # revealed: Literal[1]
+```
+
+When the either the parameter or the return type is a generic alias referring to the typevar, we
+should still be able to propagate the specializations through. This should work regardless of the
+typevar's variance in the generic alias.
+
+TODO: This currently only works for the `lift` functions (TODO: and only currently for the covariant
+case). For the `lift` functions, the parameter type is a bare typevar, resulting in us inferring a
+type mapping of `A = int, B = Class[A]`. When specializing, we can substitute the mapping of `A`
+into the mapping of `B`, giving the correct return type.
+
+For the `head` functions, the parameter type is a generic alias, resulting in us inferring a type
+mapping of `A = Class[int], A = Class[B]`. At this point, the old solver is not able to unify the
+two mappings for `A`, and we have no mapping for `B`. As a result, we infer `Unknown` for the return
+type.
+
+As part of migrating to the new solver, we will generate a single constraint set combining all of
+the facts that we learn while checking the arguments. And the constraint set implementation should
+be able to unify the two assignments to `A`.
 
-# TODO: this should be `Unknown | int`
-reveal_type(invoke(head, [1, 2, 3]))  # revealed: Unknown
+`covariant.py`:
+
+```py
+from functions import invoke, Covariant, head_covariant, lift_covariant
+
+# TODO: revealed: `int`
+# revealed: Unknown
+reveal_type(invoke(head_covariant, Covariant[int]()))
+# revealed: Covariant[Literal[1]]
+reveal_type(invoke(lift_covariant, 1))
+```
+
+`contravariant.py`:
+
+```py
+from functions import invoke, Contravariant, head_contravariant, lift_contravariant
+
+# TODO: revealed: `int`
+# revealed: Unknown
+reveal_type(invoke(head_contravariant, Contravariant[int]()))
+# TODO: revealed: Contravariant[int]
+# revealed: Unknown
+reveal_type(invoke(lift_contravariant, 1))
+```
+
+`invariant.py`:
+
+```py
+from functions import invoke, Invariant, head_invariant, lift_invariant
+
+# TODO: revealed: `int`
+# revealed: Unknown
+reveal_type(invoke(head_invariant, Invariant[int]()))
+# TODO: revealed: `Invariant[int]`
+# revealed: Unknown
+reveal_type(invoke(lift_invariant, 1))
 ```
 
 ## Protocols as TypeVar bounds
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 fd23c826e4b04..94f2f7518e11f 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
@@ -576,4 +576,431 @@ def concrete_pivot[T, U]():
     static_assert(not constraints.implies_subtype_of(T, U))
 ```
 
+### Transitivity can propagate through nested covariant typevars
+
+When a typevar appears nested inside a covariant generic type in another constraint's bound, we can
+propagate the bound "into" the generic type.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+def upper_bound[T, U]():
+    # If (T ≤ int) ∧ (U ≤ Covariant[T]), then by covariance, Covariant[T] ≤ Covariant[int],
+    # and by transitivity, U ≤ Covariant[int].
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T])
+    static_assert(constraints.implies_subtype_of(U, Covariant[int]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[str]))
+
+def lower_bound[T, U]():
+    # If (int ≤ T ∧ Covariant[T] ≤ U), then by covariance, Covariant[int] ≤ Covariant[T],
+    # and by transitivity, Covariant[int] ≤ U. Since bool ≤ int, Covariant[bool] ≤ U also holds.
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Covariant[T], U, object)
+    static_assert(constraints.implies_subtype_of(Covariant[int], U))
+    static_assert(constraints.implies_subtype_of(Covariant[bool], U))
+    static_assert(not constraints.implies_subtype_of(Covariant[str], U))
+
+# Repeat with reversed typevar ordering to verify BDD-ordering independence.
+def upper_bound[U, T]():
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Covariant[T])
+    static_assert(constraints.implies_subtype_of(U, Covariant[int]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[str]))
+
+def lower_bound[U, T]():
+    # Since bool ≤ int, Covariant[bool] ≤ U also holds.
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Covariant[T], U, object)
+    static_assert(constraints.implies_subtype_of(Covariant[int], U))
+    static_assert(constraints.implies_subtype_of(Covariant[bool], U))
+    static_assert(not constraints.implies_subtype_of(Covariant[str], U))
+```
+
+### Transitivity can propagate through nested contravariant typevars
+
+The previous section also works for contravariant generic types, though one of the antecedent
+constraints is flipped.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Contravariant[T]:
+    def set(self, value: T):
+        pass
+
+def upper_bound[T, U]():
+    # If (int ≤ T ∧ U ≤ Contravariant[T]), then by contravariance,
+    # Contravariant[T] ≤ Contravariant[int], and by transitivity, U ≤ Contravariant[int].
+    # Note: we need the *lower* bound on T (not the upper) because contravariance flips.
+    # Since bool ≤ int, Contravariant[int] ≤ Contravariant[bool], so U ≤ Contravariant[bool]
+    # also holds.
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[T])
+    static_assert(constraints.implies_subtype_of(U, Contravariant[int]))
+    static_assert(constraints.implies_subtype_of(U, Contravariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Contravariant[str]))
+
+def lower_bound[T, U]():
+    # If (T ≤ int ∧ Contravariant[T] ≤ U), then by contravariance,
+    # Contravariant[int] ≤ Contravariant[T], and by transitivity, Contravariant[int] ≤ U.
+    # Contravariant[bool] is a supertype of Contravariant[int] (since bool ≤ int), so
+    # Contravariant[bool] ≤ U does NOT hold.
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object)
+    static_assert(constraints.implies_subtype_of(Contravariant[int], U))
+    static_assert(not constraints.implies_subtype_of(Contravariant[bool], U))
+    static_assert(not constraints.implies_subtype_of(Contravariant[str], U))
+
+# Repeat with reversed typevar ordering to verify BDD-ordering independence.
+def upper_bound[U, T]():
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[T])
+    static_assert(constraints.implies_subtype_of(U, Contravariant[int]))
+    static_assert(constraints.implies_subtype_of(U, Contravariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Contravariant[str]))
+
+def lower_bound[U, T]():
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Contravariant[T], U, object)
+    static_assert(constraints.implies_subtype_of(Contravariant[int], U))
+    static_assert(not constraints.implies_subtype_of(Contravariant[bool], U))
+    static_assert(not constraints.implies_subtype_of(Contravariant[str], U))
+```
+
+### Transitivity can propagate through nested invariant typevars
+
+For invariant type parameters, only an equality constraint on the typevar allows propagation. A
+one-sided bound (upper or lower only) is not sufficient.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Invariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+    def set(self, value: T):
+        pass
+
+def equality_constraint[T, U]():
+    # (T = int ∧ U ≤ Invariant[T]) should imply U ≤ Invariant[int].
+    constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(Never, U, Invariant[T])
+    static_assert(constraints.implies_subtype_of(U, Invariant[int]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[str]))
+
+def upper_bound_only[T, U]():
+    # (T ≤ int ∧ U ≤ Invariant[T]) should NOT imply U ≤ Invariant[int], because T is invariant
+    # and we only have an upper bound, not equality.
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(Never, U, Invariant[T])
+    static_assert(not constraints.implies_subtype_of(U, Invariant[int]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[str]))
+
+def lower_bound_only[T, U]():
+    # (int ≤ T ∧ Invariant[T] ≤ U) should NOT imply Invariant[int] ≤ U, because T is invariant
+    # and we only have a lower bound, not equality.
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Invariant[T], U, object)
+    static_assert(not constraints.implies_subtype_of(Invariant[int], U))
+    static_assert(not constraints.implies_subtype_of(Invariant[bool], U))
+    static_assert(not constraints.implies_subtype_of(Invariant[str], U))
+
+# Repeat with reversed typevar ordering.
+def equality_constraint[U, T]():
+    constraints = ConstraintSet.range(int, T, int) & ConstraintSet.range(Never, U, Invariant[T])
+    static_assert(constraints.implies_subtype_of(U, Invariant[int]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[bool]))
+    static_assert(not constraints.implies_subtype_of(U, Invariant[str]))
+```
+
+### Transitivity propagates through composed variance
+
+When a typevar is nested inside multiple layers of generics, variances compose. For instance, a
+covariant type inside a contravariant type yields contravariant overall.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+class Contravariant[T]:
+    def set(self, value: T):
+        pass
+
+def covariant_of_contravariant[T, U]():
+    # Covariant[Contravariant[T]]: T is contravariant overall (covariant × contravariant).
+    # So a lower bound on T should propagate (flipped).
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Covariant[Contravariant[T]])
+    static_assert(constraints.implies_subtype_of(U, Covariant[Contravariant[int]]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[Contravariant[str]]))
+
+def contravariant_of_covariant[T, U]():
+    # Contravariant[Covariant[T]]: T is contravariant overall (contravariant × covariant).
+    # So a lower bound on T should propagate (flipped).
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[Covariant[T]])
+    static_assert(constraints.implies_subtype_of(U, Contravariant[Covariant[int]]))
+    static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]]))
+
+# Repeat with reversed typevar ordering.
+def covariant_of_contravariant[U, T]():
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Covariant[Contravariant[T]])
+    static_assert(constraints.implies_subtype_of(U, Covariant[Contravariant[int]]))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[Contravariant[str]]))
+
+def contravariant_of_covariant[U, T]():
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(Never, U, Contravariant[Covariant[T]])
+    static_assert(constraints.implies_subtype_of(U, Contravariant[Covariant[int]]))
+    static_assert(not constraints.implies_subtype_of(U, Contravariant[Covariant[str]]))
+```
+
+### Typevar bound substitution into nested generic types
+
+When a typevar B has a bare typevar S as one of its bounds, and S appears nested inside another
+constraint's bound, we can substitute B for S to create a cross-typevar link. The derived constraint
+is weaker (less restrictive), but introduces a useful relationship between the typevars.
+
+For example, `(Covariant[S] ≤ C) ∧ (S ≤ B)` should imply `Covariant[B] ≤ C`: we are given that
+`S ≤ B`, covariance tells us that `Covariant[S] ≤ Covariant[B]`, and transitivity gives
+`Covariant[B] ≤ C`. (We can infer similar weakened constraints for contravariant and invariant
+typevars.)
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+class Contravariant[T]:
+    def set(self, value: T):
+        pass
+
+class Invariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+    def set(self, value: T):
+        pass
+
+def covariant_upper_bound_into_lower[S, B, C]():
+    # (Covariant[S] ≤ C) ∧ (B ≤ S) → (Covariant[B] ≤ C)
+    # B ≤ S, so Covariant[B] ≤ Covariant[S], and Covariant[S] ≤ C gives Covariant[B] ≤ C.
+    constraints = ConstraintSet.range(Covariant[S], C, object) & ConstraintSet.range(Never, B, S)
+    static_assert(constraints.implies_subtype_of(Covariant[B], C))
+
+def covariant_lower_bound_into_upper[S, B, C]():
+    # (C ≤ Covariant[S]) ∧ (S ≤ B) → (C ≤ Covariant[B])
+    # S ≤ B, so Covariant[S] ≤ Covariant[B], and C ≤ Covariant[S] ≤ Covariant[B].
+    constraints = ConstraintSet.range(Never, C, Covariant[S]) & ConstraintSet.range(S, B, object)
+    static_assert(constraints.implies_subtype_of(C, Covariant[B]))
+
+def contravariant_upper_bound_into_lower[S, B, C]():
+    # (Contravariant[S] ≤ C) ∧ (S ≤ B) → (Contravariant[B] ≤ C)
+    # S ≤ B gives Contravariant[B] ≤ Contravariant[S], so Contravariant[B] ≤ Contravariant[S] ≤ C.
+    constraints = ConstraintSet.range(Contravariant[S], C, object) & ConstraintSet.range(S, B, object)
+    static_assert(constraints.implies_subtype_of(Contravariant[B], C))
+
+def contravariant_lower_bound_into_upper[S, B, C]():
+    # (C ≤ Contravariant[S]) ∧ (B ≤ S) → (C ≤ Contravariant[B])
+    # B ≤ S gives Contravariant[S] ≤ Contravariant[B], so C ≤ Contravariant[S] ≤ Contravariant[B].
+    constraints = ConstraintSet.range(Never, C, Contravariant[S]) & ConstraintSet.range(Never, B, S)
+    static_assert(constraints.implies_subtype_of(C, Contravariant[B]))
+
+# Repeat with reversed typevar ordering.
+def covariant_upper_bound_into_lower[C, B, S]():
+    constraints = ConstraintSet.range(Covariant[S], C, object) & ConstraintSet.range(Never, B, S)
+    static_assert(constraints.implies_subtype_of(Covariant[B], C))
+
+def covariant_lower_bound_into_upper[C, B, S]():
+    constraints = ConstraintSet.range(Never, C, Covariant[S]) & ConstraintSet.range(S, B, object)
+    static_assert(constraints.implies_subtype_of(C, Covariant[B]))
+
+def contravariant_upper_bound_into_lower[C, B, S]():
+    constraints = ConstraintSet.range(Contravariant[S], C, object) & ConstraintSet.range(S, B, object)
+    static_assert(constraints.implies_subtype_of(Contravariant[B], C))
+
+def contravariant_lower_bound_into_upper[C, B, S]():
+    constraints = ConstraintSet.range(Never, C, Contravariant[S]) & ConstraintSet.range(Never, B, S)
+    static_assert(constraints.implies_subtype_of(C, Contravariant[B]))
+```
+
+### Concrete bound substitution into nested generic types (future extension)
+
+When B's bound _contains_ a typevar (but is not a bare typevar), the same logic as above applies.
+
+TODO: This is not implemented yet, since it requires different detection machinery.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+def upper_bound_into_lower[B, C]():
+    # (Covariant[int] ≤ C) ∧ (B ≤ int) → (Covariant[B] ≤ C)
+    constraints = ConstraintSet.range(Covariant[int], C, object) & ConstraintSet.range(Never, B, int)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.implies_subtype_of(Covariant[B], C))
+
+def lower_bound_into_upper[B, C]():
+    # (C ≤ Covariant[int]) ∧ (int ≤ B) → (C ≤ Covariant[B])
+    constraints = ConstraintSet.range(Never, C, Covariant[int]) & ConstraintSet.range(int, B, object)
+    # TODO: no error
+    # error: [static-assert-error]
+    static_assert(constraints.implies_subtype_of(C, Covariant[B]))
+```
+
+### Nested typevar propagation also works when the replacement is a bare typevar
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+class Contravariant[T]:
+    def set(self, value: T):
+        pass
+
+class Invariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+    def set(self, value: T):
+        pass
+
+def covariant_upper[B, S, U]():
+    # (B ≤ S) ∧ (U ≤ Covariant[B]) -> (U ≤ Covariant[S])
+    constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Covariant[B])
+    static_assert(constraints.implies_subtype_of(U, Covariant[S]))
+
+def covariant_lower[B, S, U]():
+    # (S ≤ B) ∧ (Covariant[B] ≤ U) -> (Covariant[S] ≤ U)
+    constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Covariant[B], U, object)
+    static_assert(constraints.implies_subtype_of(Covariant[S], U))
+
+def contravariant_upper[B, S, U]():
+    # (S ≤ B) ∧ (U ≤ Contravariant[B]) -> (U ≤ Contravariant[S])
+    constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Never, U, Contravariant[B])
+    static_assert(constraints.implies_subtype_of(U, Contravariant[S]))
+
+def contravariant_lower[B, S, U]():
+    # (B ≤ S) ∧ (Contravariant[B] ≤ U) -> (Contravariant[S] ≤ U)
+    constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Contravariant[B], U, object)
+    static_assert(constraints.implies_subtype_of(Contravariant[S], U))
+
+def invariant_upper_requires_equality[B, S, U]():
+    # Invariant replacement only holds under equality constraints on B.
+    constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Never, U, Invariant[B])
+    static_assert(constraints.implies_subtype_of(U, Invariant[S]))
+
+def invariant_lower_requires_equality[B, S, U]():
+    constraints = ConstraintSet.range(S, B, S) & ConstraintSet.range(Invariant[B], U, object)
+    static_assert(constraints.implies_subtype_of(Invariant[S], U))
+
+def invariant_upper_one_sided_is_not_enough[B, S, U]():
+    constraints = ConstraintSet.range(Never, B, S) & ConstraintSet.range(Never, U, Invariant[B])
+    static_assert(not constraints.implies_subtype_of(U, Invariant[S]))
+
+def invariant_lower_one_sided_is_not_enough[B, S, U]():
+    constraints = ConstraintSet.range(S, B, object) & ConstraintSet.range(Invariant[B], U, object)
+    static_assert(not constraints.implies_subtype_of(Invariant[S], U))
+```
+
+### Reverse decomposition: bounds on a typevar can be decomposed via variance
+
+When a constraint has lower and upper bounds that are parameterizations of the same generic type, we
+can decompose the bounds to extract constraints on the nested typevar. For instance, the constraint
+`Covariant[int] ≤ A ≤ Covariant[T]` implies `int ≤ T`, because `Covariant` is covariant and
+`Covariant[int] ≤ Covariant[T]` requires `int ≤ T`.
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+class Covariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+class Contravariant[T]:
+    def set(self, value: T):
+        pass
+
+class Invariant[T]:
+    def get(self) -> T:
+        raise ValueError
+
+    def set(self, value: T):
+        pass
+
+def covariant_decomposition[A, T]():
+    # Covariant[int] ≤ A ≤ Covariant[T] implies int ≤ T.
+    constraints = ConstraintSet.range(Covariant[int], A, Covariant[T])
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(str, T))
+
+def contravariant_decomposition[A, T]():
+    # Contravariant[int] ≤ A ≤ Contravariant[T] implies T ≤ int (flipped).
+    # Because contravariance reverses: Contravariant[int] ≤ Contravariant[T] means T ≤ int.
+    constraints = ConstraintSet.range(Contravariant[int], A, Contravariant[T])
+    static_assert(constraints.implies_subtype_of(T, int))
+    static_assert(not constraints.implies_subtype_of(T, str))
+
+def invariant_decomposition[A, T]():
+    # Invariant[int] ≤ A ≤ Invariant[T] implies T = int.
+    constraints = ConstraintSet.range(Invariant[int], A, Invariant[T])
+    static_assert(constraints.implies_subtype_of(T, int))
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(T, str))
+
+def bare_typevar_decomposition[A, S, T]():
+    # S ≤ A ≤ T implies S ≤ T. This is existing behavior (bare typevar transitivity)
+    # that should continue to work.
+    constraints = ConstraintSet.range(S, A, T)
+    static_assert(constraints.implies_subtype_of(S, T))
+
+# Repeat with reversed typevar ordering.
+def covariant_decomposition[T, A]():
+    constraints = ConstraintSet.range(Covariant[int], A, Covariant[T])
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(str, T))
+
+def contravariant_decomposition[T, A]():
+    constraints = ConstraintSet.range(Contravariant[int], A, Contravariant[T])
+    static_assert(constraints.implies_subtype_of(T, int))
+    static_assert(not constraints.implies_subtype_of(T, str))
+
+def invariant_decomposition[T, A]():
+    constraints = ConstraintSet.range(Invariant[int], A, Invariant[T])
+    static_assert(constraints.implies_subtype_of(T, int))
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(T, str))
+
+# The lower and upper bounds don't need to be parameterizations of the same type — our inference
+# logic handles subtyping naturally.
+class Sub(Covariant[int]): ...
+
+def subclass_lower_bound[A, T]():
+    # Sub ≤ Covariant[int], so Sub ≤ A ≤ Covariant[T] implies int ≤ T.
+    constraints = ConstraintSet.range(Sub, A, Covariant[T])
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(str, T))
+
+def subclass_lower_bound[T, A]():
+    constraints = ConstraintSet.range(Sub, A, Covariant[T])
+    static_assert(constraints.implies_subtype_of(int, T))
+    static_assert(not constraints.implies_subtype_of(str, T))
+```
+
 [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index fc7250c65e97f..64ed20c65cea2 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -1336,6 +1336,10 @@ impl<'db> Type<'db> {
         self.as_union().expect("Expected a Type::Union variant")
     }
 
+    pub(crate) const fn is_intersection(self) -> bool {
+        matches!(self, Type::Intersection(_))
+    }
+
     /// Returns whether this is a "real" intersection type. (Negated types are represented by an
     /// intersection containing a single negative branch, which this method does _not_ consider a
     /// "real" intersection.)
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 7e410aea6f836..556771c6c30e7 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -102,6 +102,7 @@ use smallvec::SmallVec;
 use crate::types::class::GenericAlias;
 use crate::types::generics::InferableTypeVars;
 use crate::types::typevar::{BoundTypeVarIdentity, walk_bound_type_var_type};
+use crate::types::variance::VarianceInferable;
 use crate::types::visitor::{
     TypeCollector, TypeVisitor, any_over_type, walk_type_with_recursion_guard,
 };
@@ -794,9 +795,9 @@ impl<'db> ConstraintSetBuilder<'db> {
         // `OwnedConstraintSet` is only used in mdtests, and not in type inference of user code.
 
         fn rebuild_node<'db>(
-            db: &'db dyn Db,
             builder: &ConstraintSetBuilder<'db>,
             other: &OwnedConstraintSet<'db>,
+            constraints: &IndexVec<ConstraintId, NodeId>,
             cache: &mut FxHashMap<NodeId, NodeId>,
             old_node: NodeId,
         ) -> NodeId {
@@ -807,36 +808,52 @@ impl<'db> ConstraintSetBuilder<'db> {
                 return *remapped;
             }
 
-            let old_interior = other.nodes[old_node];
-            let old_constraint = other.constraints[old_interior.constraint];
-            let condition = Constraint::new_node(
-                db,
-                builder,
-                old_constraint.typevar,
-                old_constraint.lower,
-                old_constraint.upper,
-            );
-
             // Absorb the uncertain branch into both true and false branches. This collapses
             // the TDD back to a binary structure, which is correct but loses the TDD laziness for
             // unions. This is acceptable since `load` is only used for `OwnedConstraintSet` in
             // mdtests.
             // TODO: A 4-arg `ite_uncertain` could preserve TDD structure if `load` ever becomes
             // performance-sensitive.
-            let if_true = rebuild_node(db, builder, other, cache, old_interior.if_true);
-            let if_uncertain = rebuild_node(db, builder, other, cache, old_interior.if_uncertain);
-            let if_false = rebuild_node(db, builder, other, cache, old_interior.if_false);
+            let old_interior = other.nodes[old_node];
+            let if_true = rebuild_node(builder, other, constraints, cache, old_interior.if_true);
+            let if_uncertain = rebuild_node(
+                builder,
+                other,
+                constraints,
+                cache,
+                old_interior.if_uncertain,
+            );
+            let if_false = rebuild_node(builder, other, constraints, cache, old_interior.if_false);
             let if_true_merged = if_true.or(builder, if_uncertain);
             let if_false_merged = if_false.or(builder, if_uncertain);
+            let condition = constraints[old_interior.constraint];
             let remapped = condition.ite(builder, if_true_merged, if_false_merged);
 
             cache.insert(old_node, remapped);
             remapped
         }
 
+        // Load all of the constraints into the this builder first, to maximize the chance that the
+        // constraints and typevars will appear in the same order. (This is important because many
+        // of our mdtests try to force a particular ordering, to test that our algorithms are all
+        // order-independent.)
+        let constraints = other
+            .constraints
+            .iter()
+            .map(|old_constraint| {
+                Constraint::new_node(
+                    db,
+                    self,
+                    old_constraint.typevar,
+                    old_constraint.lower,
+                    old_constraint.upper,
+                )
+            })
+            .collect();
+
         // Maps NodeIds in the OwnedConstraintSet to the corresponding NodeIds in this builder.
         let mut cache = FxHashMap::default();
-        let node = rebuild_node(db, self, other, &mut cache, other.node);
+        let node = rebuild_node(self, other, &constraints, &mut cache, other.node);
         ConstraintSet::from_node(self, node)
     }
 
@@ -1118,9 +1135,15 @@ impl<'db> Constraint<'db> {
             _ => {}
         }
 
-        // If `lower ≰ upper`, then the constraint cannot be satisfied, since there is no type that
-        // is both greater than `lower`, and less than `upper`.
-        if !lower.is_constraint_set_assignable_to(db, upper) {
+        // If `lower ≰ upper` for every possible assignment of typevars, then the constraint cannot
+        // be satisfied, since there is no type that is both greater than `lower`, and less than
+        // `upper`. We use an existential check here ("is there *some* assignment where
+        // `lower ≤ upper`?") rather than a universal check, because the bounds may mention
+        // typevars — e.g., `Sequence[int] ≤ A ≤ Sequence[T]` is satisfiable when `int ≤ T`.
+        if lower
+            .when_constraint_set_assignable_to(db, upper, builder)
+            .is_never_satisfied(db)
+        {
             return ALWAYS_FALSE;
         }
 
@@ -1313,9 +1336,16 @@ impl ConstraintId {
         let upper =
             IntersectionType::from_two_elements(db, self_constraint.upper, other_constraint.upper);
 
-        // If `lower ≰ upper`, then the intersection is empty, since there is no type that is both
-        // greater than `lower`, and less than `upper`.
-        if !lower.is_constraint_set_assignable_to(db, upper) {
+        // If `lower ≰ upper` for every possible assignment of typevars, then the intersection is
+        // empty, since there is no type that is both greater than `lower`, and less than `upper`.
+        // We use an existential check here ("is there *some* assignment where `lower ≤ upper`?")
+        // rather than a universal check ("is `lower ≤ upper` for *all* assignments?"), because the
+        // bounds may mention typevars — e.g., `Sequence[int] ≤ A ≤ Sequence[T]` is satisfiable
+        // when `int ≤ T`, even though it's not universally true for all `T`.
+        if lower
+            .when_constraint_set_assignable_to(db, upper, builder)
+            .is_never_satisfied(db)
+        {
             return IntersectionResult::Disjoint;
         }
 
@@ -1573,6 +1603,50 @@ impl NodeId {
         }
     }
 
+    /// Checks whether this BDD represents a single conjunction (of an arbitrary number of
+    /// positive or negative constraints).
+    fn is_single_conjunction(self, builder: &ConstraintSetBuilder<'_>) -> bool {
+        // A BDD can be viewed as an encoding of the formula's DNF representation (OR of ANDs).
+        // Each path from the root node to the `always` terminals represents one of the disjoints.
+        // The constraints that we encounter on the path represent the conjoints. That means that a
+        // BDD can only represent a single conjunction if there is precisely one path from the root
+        // node to the `always` terminal.
+        //
+        // We can take advantage of quasi-reduction. We never create an interior node with both
+        // outgoing edges leading to `never`; those are collapsed to `never`. That means that if we
+        // ever encounter a node with both outgoing edges pointing to something other than `never`,
+        // that node must have at least two paths to the `always` terminal.
+        let mut current = self.node();
+        loop {
+            match current {
+                Node::AlwaysTrue => return true,
+                Node::AlwaysFalse => return false,
+                Node::Interior(interior) => {
+                    let data = builder.interior_node_data(interior.node());
+
+                    // If both if_true and if_false point to non-never, there are multiple paths to
+                    // `always`, so this cannot be a simple conjunction.
+                    if data.if_true != ALWAYS_FALSE && data.if_false != ALWAYS_FALSE {
+                        return false;
+                    }
+
+                    // The uncertain branch must also be never for a simple conjunction, since it
+                    // contributes to all paths.
+                    if data.if_uncertain != ALWAYS_FALSE {
+                        return false;
+                    }
+
+                    // Follow the non-never branch.
+                    current = if data.if_true != ALWAYS_FALSE {
+                        data.if_true.node()
+                    } else {
+                        data.if_false.node()
+                    };
+                }
+            }
+        }
+    }
+
     fn for_each_path<'db>(
         self,
         db: &'db dyn Db,
@@ -3139,12 +3213,9 @@ impl InteriorNode {
             db,
             builder,
             // Remove any node that constrains `bound_typevar`, or that has a lower/upper bound
-            // that mentions `bound_typevar`.
-            // TODO: This will currently remove constraints that mention a typevar, but the sequent
-            // map is not yet propagating all derived facts about those constraints. For instance,
-            // removing `T` from `T ≤ int ∧ U ≤ Sequence[T]` should produce `U ≤ Sequence[int]`.
-            // But that requires `T ≤ int ∧ U ≤ Sequence[T] → U ≤ Sequence[int]` to exist in the
-            // sequent map. It doesn't, and so we currently produce `U ≤ Unknown` in this case.
+            // that mentions `bound_typevar`. The sequent map ensures that derived facts are
+            // propagated for nested typevar references, using the variance of the typevar's
+            // position to determine the correct substitution.
             &mut |constraint| {
                 let constraint = builder.constraint_data(constraint);
                 if constraint.typevar.identity(db) == bound_typevar {
@@ -4382,58 +4453,111 @@ impl SequentMap {
             return;
         }
 
-        // If the lower or upper bound of this constraint is a typevar, we can propagate the
-        // constraint:
+        // Given a constraint `L ≤ T ≤ U`, `L ≤ U` must also hold. If those bounds contain other
+        // typevars, we can infer additional constraints. This is easiest to see when the bounds
+        // _are_ typevars:
         //
         //   1. `(S ≤ T ≤ U) → (S ≤ U)`
         //   2. `(S ≤ T ≤ τ) → (S ≤ τ)`
         //   3. `(τ ≤ T ≤ U) → (τ ≤ U)`
         //
-        // 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.
+        // but it also holds when the bounds _contain_ typevars:
+        //
+        //   4. `(Covariant[S] ≤ T ≤ Covariant[U]) → (S ≤ U)`
+        //      `(Covariant[S] ≤ T ≤ Covariant[τ]) → (S ≤ τ)`
+        //      `(Covariant[τ] ≤ T ≤ Covariant[U]) → (τ ≤ U)`
+        //
+        //   5. `(Contravariant[S] ≤ T ≤ Contravariant[U]) → (U ≤ S)`
+        //      `(Contravariant[S] ≤ T ≤ Contravariant[τ]) → (τ ≤ S)`
+        //      `(Contravariant[τ] ≤ T ≤ Contravariant[U]) → (U ≤ τ)`
+        //
+        //   6. `(Invariant[S] ≤ T ≤ Invariant[U]) → (S = U)`
+        //      `(Invariant[S] ≤ T ≤ Invariant[τ]) → (S = τ)`
+        //      `(Invariant[τ] ≤ T ≤ Invariant[U]) → (τ = U)`
+        //
+        // and whenever the bounds are assignable, even if they don't mention exactly the same
+        // types:
+        //
+        //   class Sub(Covariant[int]): ...
+        //
+        //   7. `(Covariant[S] ≤ T ≤ Sub) → (S ≤ int)`
+        //      `(Sub ≤ T ≤ Covariant[U]) → (int ≤ U)`
+        //
+        // To handle all of these cases, we perform a constraint set assignability check to see
+        // when `L ≤ U`. This gives us a constraint set, which should be the rhs of the sequent
+        // implication. (That is, this check directly encodes `(L ≤ T ≤ U) → (L ≤ U)` as an
+        // implication.)
 
-        let post_constraint = match (lower, upper) {
-            // Case 1
-            (Type::TypeVar(lower_typevar), Type::TypeVar(upper_typevar)) => {
-                if lower_typevar.is_same_typevar_as(db, upper_typevar) {
-                    return;
-                }
+        // Skip trivial cases where the assignability check won't produce useful results.
+        if lower.is_never() || upper.is_object() {
+            return;
+        }
 
-                // We always want to propagate `lower ≤ upper`, but we must do so using a
-                // canonical top-level typevar ordering.
-                //
-                // Example: if we learn `(A ≤ [T] ≤ B)`, this single-constraint propagation step
-                // should infer `A ≤ B`. Depending on ordering, we might need to encode that as
-                // either `(Never ≤ [A] ≤ B)` or `(A ≤ [B] ≤ object)`. Both render as `A ≤ B`,
-                // but they constrain different typevars and must be created in the orientation
-                // allowed by `can_be_bound_for`.
-                if upper_typevar.can_be_bound_for(db, builder, lower_typevar) {
-                    ConstraintId::new(db, builder, lower_typevar, Type::Never, upper)
-                } else {
-                    ConstraintId::new(
-                        db,
-                        builder,
-                        upper_typevar,
-                        Type::TypeVar(lower_typevar),
-                        Type::object(),
-                    )
-                }
-            }
+        let when = lower.when_constraint_set_assignable_to(db, upper, builder);
 
-            // Case 2
-            (Type::TypeVar(lower_typevar), _) => {
-                ConstraintId::new(db, builder, lower_typevar, Type::Never, upper)
-            }
+        // If L is _never_ assignable to U, this constraint would violate transitivity, and should
+        // never have been added.
+        debug_assert!(!when.is_never_satisfied(db));
 
-            // Case 3
-            (_, Type::TypeVar(upper_typevar)) => {
-                ConstraintId::new(db, builder, upper_typevar, lower, Type::object())
-            }
+        // Fast path: If L is trivially always assignable to U, there are no derived constraints
+        // that we can infer. (This would be handled correctly by the logic below, but this is a
+        // useful early return.)
+        if when.node == ALWAYS_TRUE {
+            return;
+        }
 
-            _ => return,
-        };
+        // Technically, we've just calculated a _constraint set_ as the rhs of this implication.
+        // Unfortunately, our sequent map can currently only store implications where the rhs is a
+        // single constraint.
+        //
+        // If the constraint set that we get represents a single conjunction, we can still shoehorn
+        // it into this shape, since we can "break apart" a conjunction on the rhs of an
+        // implication:
+        //
+        //   a → b ∧ c ∧ d
+        //
+        // becomes
+        //
+        //   a → b
+        //   a → c
+        //   a → d
+        //
+        // That takes care of breaking apart the rhs conjunction: we can add each positive
+        // constraint as a separate single_implication.
+        //
+        // We can also handle _negative_ constraints, because those turn into impossibilities:
+        //
+        //   a → ¬b
+        //
+        // becomes
+        //
+        //   a ∧ b → false
+        //
+        // TODO: This should handle the most common cases. In the future, we could handle arbitrary
+        // rhs constraint sets by moving this logic into PathAssignments::walk_path, and performing
+        // it once for _every_ root→always path in the BDD. (That would require resetting the
+        // PathAssignments state for each of those paths, which is why the logic would have to
+        // move.)
+        let mut node = when.node;
+        if !node.is_single_conjunction(builder) {
+            return;
+        }
 
-        self.add_single_implication(db, builder, constraint, post_constraint);
+        loop {
+            match node.node() {
+                Node::AlwaysTrue | Node::AlwaysFalse => break,
+                Node::Interior(interior) => {
+                    let interior = builder.interior_node_data(interior.node());
+                    if interior.if_true != ALWAYS_FALSE {
+                        self.add_single_implication(db, builder, constraint, interior.constraint);
+                        node = interior.if_true;
+                    } else {
+                        self.add_pair_impossibility(db, builder, constraint, interior.constraint);
+                        node = interior.if_false;
+                    }
+                }
+            }
+        }
     }
 
     fn add_sequents_for_pair<'db>(
@@ -4475,6 +4599,7 @@ impl SequentMap {
                 left_constraint,
                 right_constraint,
             );
+            self.add_nested_typevar_sequents(db, builder, left_constraint, right_constraint);
         } else if left_constraint_data.lower.is_type_var()
             || left_constraint_data.upper.is_type_var()
             || right_constraint_data.lower.is_type_var()
@@ -4646,6 +4771,307 @@ impl SequentMap {
         }
     }
 
+    /// Adds sequents for the case where one constraint's lower or upper bound contains another
+    /// constraint's typevar nested inside a parameterized type (e.g., `U ≤ Covariant[T]`).
+    ///
+    /// This is distinct from `add_mutual_sequents_for_different_typevars`, which handles the case
+    /// where a typevar appears _directly_ as a top-level lower/upper bound (e.g., `U ≤ T`). A
+    /// bare `Type::TypeVar` is technically a special case of covariant nesting (since the variance
+    /// of `T` in `T` itself is covariant), but the existing direct-typevar logic handles it
+    /// separately because it requires careful canonical ordering of typevar-to-typevar constraints
+    /// that the generic nested-typevar logic here does not need to worry about.
+    fn add_nested_typevar_sequents<'db>(
+        &mut self,
+        db: &'db dyn Db,
+        builder: &ConstraintSetBuilder<'db>,
+        left_constraint: ConstraintId,
+        right_constraint: ConstraintId,
+    ) {
+        let mut try_tightening =
+            |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| {
+                let bound_data = builder.constraint_data(bound_constraint);
+                let bound_typevar = bound_data.typevar;
+                let constrained_data = builder.constraint_data(constrained_constraint);
+                let constrained_typevar = constrained_data.typevar;
+
+                // If the replacement contains the bound typevar itself (e.g., the bound
+                // constraint is `_V ≤ G[_V]`), or the constrained typevar (e.g., the bound
+                // constraint is `_T ≤ G[_V]` and we're about to substitute into `_V ≤ G[_T]`),
+                // substituting would create a deeper nesting of the same recursive pattern
+                // that triggers the same substitution again ad infinitum. Skip in both cases.
+                //
+                // Fast-path bare typevar replacements (`Type::TypeVar`) using equality checks
+                // instead of calling `variance_of` on them. This avoids a large number of tiny
+                // tracked `variance_of` queries in hot paths.
+                let replacement_mentions_bound_or_constrained = |replacement: Type<'db>| {
+                    replacement.variance_of(db, bound_typevar) != TypeVarVariance::Bivariant
+                        || replacement.variance_of(db, constrained_typevar)
+                            != TypeVarVariance::Bivariant
+                };
+
+                // Check the upper bound of the constrained constraint for nested occurrences of
+                // the bound typevar. We use `variance_of` as our combined presence + variance
+                // check: `Bivariant` means the typevar doesn't appear in the type (or is genuinely
+                // bivariant, which is semantically equivalent — no implication is needed in either
+                // case).
+                //
+                // Note: if `Bivariant` is ever removed from the `TypeVarVariance` enum, we would
+                // need an alternative representation for "typevar not present"
+                // (e.g., `Option<TypeVarVariance>`).
+                let upper_replacement = match constrained_data.upper.variance_of(db, bound_typevar)
+                {
+                    TypeVarVariance::Bivariant => None,
+                    // Skip bare typevars — those are handled by
+                    // `add_mutual_sequents_for_different_typevars`.
+                    _ if constrained_data.upper.is_type_var() => None,
+                    // Covariance preserves direction: upper bound on T substitutes into upper
+                    // bound. A ≤ B → G[A] ≤ G[B], so (T ≤ u_B) gives G[T] ≤ G[u_B].
+                    TypeVarVariance::Covariant if !bound_data.upper.is_object() => {
+                        Some(bound_data.upper)
+                    }
+                    // Contravariance flips direction: lower bound on T substitutes into upper
+                    // bound. A ≤ B → G[B] ≤ G[A], so (l_B ≤ T) gives G[T] ≤ G[l_B].
+                    TypeVarVariance::Contravariant if !bound_data.lower.is_never() => {
+                        Some(bound_data.lower)
+                    }
+                    // Invariance requires equality: only substitute if l_B = u_B.
+                    TypeVarVariance::Invariant
+                        if bound_data.lower == bound_data.upper && !bound_data.lower.is_never() =>
+                    {
+                        Some(bound_data.lower)
+                    }
+                    _ => None,
+                };
+                let upper_replacement = upper_replacement.filter(|replacement| {
+                    // Substituting one typevar for another into large unions can generate many
+                    // very-weak derived constraints and cause severe performance regressions.
+                    // Keep the common/non-union case enabled; skip union upper bounds for this
+                    // specific typevar-to-typevar replacement shape.
+                    if replacement.is_type_var() && constrained_data.upper.is_union() {
+                        return false;
+                    }
+                    !replacement_mentions_bound_or_constrained(*replacement)
+                });
+                if let Some(replacement) = upper_replacement {
+                    let new_upper = constrained_data.upper.substitute_one_typevar(
+                        db,
+                        bound_typevar,
+                        replacement,
+                    );
+                    if new_upper != constrained_data.upper {
+                        let post = ConstraintId::new(
+                            db,
+                            builder,
+                            constrained_typevar,
+                            constrained_data.lower,
+                            new_upper,
+                        );
+                        self.add_pair_implication(
+                            db,
+                            builder,
+                            bound_constraint,
+                            constrained_constraint,
+                            post,
+                        );
+                    }
+                }
+
+                // Check the lower bound of the constrained constraint for nested occurrences.
+                let lower_replacement = match constrained_data.lower.variance_of(db, bound_typevar)
+                {
+                    TypeVarVariance::Bivariant => None,
+                    _ if constrained_data.lower.is_type_var() => None,
+                    // Covariance preserves direction: lower bound on T substitutes into lower
+                    // bound. A ≤ B → G[A] ≤ G[B], so (l_B ≤ T) gives G[l_B] ≤ G[T].
+                    TypeVarVariance::Covariant if !bound_data.lower.is_never() => {
+                        Some(bound_data.lower)
+                    }
+                    // Contravariance flips direction: upper bound on T substitutes into lower
+                    // bound. A ≤ B → G[B] ≤ G[A], so (T ≤ u_B) gives G[u_B] ≤ G[T].
+                    TypeVarVariance::Contravariant if !bound_data.upper.is_object() => {
+                        Some(bound_data.upper)
+                    }
+                    // Invariance requires equality: only substitute if l_B = u_B.
+                    TypeVarVariance::Invariant
+                        if bound_data.lower == bound_data.upper && !bound_data.lower.is_never() =>
+                    {
+                        Some(bound_data.lower)
+                    }
+                    _ => None,
+                };
+                let lower_replacement = lower_replacement.filter(|replacement| {
+                    // Substituting one typevar for another into large intersections can generate
+                    // many very-weak derived constraints and cause severe performance regressions.
+                    // Keep the common/non-intersection case enabled; skip intersection lower
+                    // bounds for this specific typevar-to-typevar replacement shape.
+                    if replacement.is_type_var() && constrained_data.lower.is_intersection() {
+                        return false;
+                    }
+                    !replacement_mentions_bound_or_constrained(*replacement)
+                });
+                if let Some(replacement) = lower_replacement {
+                    let new_lower = constrained_data.lower.substitute_one_typevar(
+                        db,
+                        bound_typevar,
+                        replacement,
+                    );
+                    if new_lower != constrained_data.lower {
+                        let post = ConstraintId::new(
+                            db,
+                            builder,
+                            constrained_typevar,
+                            new_lower,
+                            constrained_data.upper,
+                        );
+                        self.add_pair_implication(
+                            db,
+                            builder,
+                            bound_constraint,
+                            constrained_constraint,
+                            post,
+                        );
+                    }
+                }
+            };
+
+        try_tightening(left_constraint, right_constraint);
+        try_tightening(right_constraint, left_constraint);
+
+        // Additionally, check if one constraint's bare typevar *bound* appears nested in the other
+        // constraint's bounds. This handles the "dual" direction: instead of substituting a
+        // typevar's concrete bounds into another constraint (tightening), we substitute the
+        // typevar itself for one of its bare typevar bounds (weakening), creating a cross-typevar
+        // link.
+        //
+        // For example, given `(Covariant[S] ≤ C) ∧ (Never ≤ B ≤ S)`, S is B's upper bound and
+        // appears covariantly in C's lower bound. Since `B ≤ S`, covariance tells us that
+        // `Covariant[B] ≤ Covariant[S]`. Transitivity then lets us derive `Covariant[B] ≤ C`.
+        //
+        // The derived constraint is weaker than the original, but it introduces a relationship
+        // between B and C that we need to remember and propagate if we ever existentially quantify
+        // away S.
+        //
+        // TODO: This only handles the case where the bound (in this case, S) is a bare typevar. A
+        // future extension could handle arbitrary types by pattern-matching on generic alias
+        // structure.
+        //
+        // This is defined as a separate closure because it iterates over the bound constraint's
+        // bare typevar bounds, which is a different axis than `try_tightening`'s check on the
+        // bound constraint's typevar.
+        let mut try_weakening =
+            |bound_constraint: ConstraintId, constrained_constraint: ConstraintId| {
+                let bound_data = builder.constraint_data(bound_constraint);
+                let bound_typevar = bound_data.typevar;
+                let constrained_data = builder.constraint_data(constrained_constraint);
+                let constrained_typevar = constrained_data.typevar;
+
+                let mut try_one_bound = |bound: Type<'db>, is_upper_bound: bool| {
+                    let Some(nested_typevar) = bound.as_typevar() else {
+                        return;
+                    };
+
+                    // Skip if the nested typevar is the same as the constrained typevar — that
+                    // case is handled by `add_mutual_sequents_for_different_typevars`.
+                    if nested_typevar.is_same_typevar_as(db, constrained_typevar)
+                        || nested_typevar.is_same_typevar_as(db, bound_typevar)
+                    {
+                        return;
+                    }
+
+                    let replacement = Type::TypeVar(bound_typevar);
+
+                    // Check the constrained constraint's upper bound for nested occurrences of
+                    // nested_typevar (S). We want to *weaken* (relax) the upper bound by making it
+                    // larger:
+                    //   - Covariant + S is B's lower bound (S ≤ B): G[S] ≤ G[B] → weaker. Emit.
+                    //   - Contravariant + S is B's upper bound (B ≤ S): G[S] ≤ G[B] → weaker. Emit.
+                    //   - Other combinations tighten rather than weaken. Skip.
+                    let should_weaken_upper = !constrained_data.upper.is_type_var()
+                        && !constrained_data.upper.is_never()
+                        && !constrained_data.upper.is_object()
+                        && !constrained_data.upper.is_dynamic()
+                        && match constrained_data.upper.variance_of(db, nested_typevar) {
+                            TypeVarVariance::Bivariant => false,
+                            TypeVarVariance::Covariant => !is_upper_bound,
+                            TypeVarVariance::Contravariant => is_upper_bound,
+                            TypeVarVariance::Invariant => {
+                                bound_data.lower == bound_data.upper && !bound_data.lower.is_never()
+                            }
+                        };
+                    if should_weaken_upper {
+                        let new_upper = constrained_data.upper.substitute_one_typevar(
+                            db,
+                            nested_typevar,
+                            replacement,
+                        );
+                        if new_upper != constrained_data.upper {
+                            let post = ConstraintId::new(
+                                db,
+                                builder,
+                                constrained_typevar,
+                                constrained_data.lower,
+                                new_upper,
+                            );
+                            self.add_pair_implication(
+                                db,
+                                builder,
+                                bound_constraint,
+                                constrained_constraint,
+                                post,
+                            );
+                        }
+                    }
+
+                    // Ditto for the lower bound.
+                    let should_weaken_lower = !constrained_data.lower.is_type_var()
+                        && !constrained_data.lower.is_never()
+                        && !constrained_data.lower.is_object()
+                        && !constrained_data.lower.is_dynamic()
+                        && match constrained_data.lower.variance_of(db, nested_typevar) {
+                            TypeVarVariance::Bivariant => false,
+                            TypeVarVariance::Covariant => is_upper_bound,
+                            TypeVarVariance::Contravariant => !is_upper_bound,
+                            TypeVarVariance::Invariant => {
+                                bound_data.lower == bound_data.upper && !bound_data.lower.is_never()
+                            }
+                        };
+                    if should_weaken_lower {
+                        let new_lower = constrained_data.lower.substitute_one_typevar(
+                            db,
+                            nested_typevar,
+                            replacement,
+                        );
+                        if new_lower != constrained_data.lower {
+                            let post = ConstraintId::new(
+                                db,
+                                builder,
+                                constrained_typevar,
+                                new_lower,
+                                constrained_data.upper,
+                            );
+                            self.add_pair_implication(
+                                db,
+                                builder,
+                                bound_constraint,
+                                constrained_constraint,
+                                post,
+                            );
+                        }
+                    }
+                };
+
+                // For each bare typevar bound S of the bound constraint, check if S appears
+                // nested in the constrained constraint's bounds. If so, we can substitute B
+                // (the bound constraint's typevar) for S, producing a weaker but useful
+                // constraint.
+                try_one_bound(bound_data.upper, true);
+                try_one_bound(bound_data.lower, false);
+            };
+
+        try_weakening(left_constraint, right_constraint);
+        try_weakening(right_constraint, left_constraint);
+    }
+
     fn add_mutual_sequents_for_same_typevars<'db>(
         &mut self,
         db: &'db dyn Db,
@@ -5792,16 +6218,16 @@ mod tests {
             &builder,
             loaded,
             indoc! {r#"
-                <0> (T = int) 1/1
-                ┡━₁ <1> (U = str) 1/1
+                <0> (U = str) 1/1
+                ┡━₁ <1> (T = int) 1/1
                 │   ┡━₁ never
-                │   ├─? never
-                │   └─₀ always
-                ├─? <2> (U = str) 1/1
-                │   ┡━₁ always
-                │   ├─? never
+                │   ├─? always
                 │   └─₀ never
-                └─₀ never
+                ├─? never
+                └─₀ <2> (T = int) 1/1
+                    ┡━₁ always
+                    ├─? never
+                    └─₀ never
             "#},
         );
     }
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 4df1ebcd2e2e7..eae4880640996 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1581,6 +1581,9 @@ pub enum ApplySpecialization<'a, 'db> {
         skip: Option<usize>,
     },
     ReturnCallables(&'a FxIndexMap<BoundTypeVarInstance<'db>, BoundTypeVarInstance<'db>>),
+    /// Maps a single typevar to a concrete type. Used by the constraint set's sequent map to
+    /// substitute a typevar nested inside another constraint's bound.
+    Single(BoundTypeVarInstance<'db>, Type<'db>),
 }
 
 impl<'db> ApplySpecialization<'_, 'db> {
@@ -1611,10 +1614,35 @@ impl<'db> ApplySpecialization<'_, 'db> {
             ApplySpecialization::ReturnCallables(replacements) => {
                 replacements.get(&bound_typevar).copied().map(Type::TypeVar)
             }
+            ApplySpecialization::Single(typevar, ty) => {
+                if bound_typevar.is_same_typevar_as(db, *typevar) {
+                    Some(*ty)
+                } else {
+                    None
+                }
+            }
         }
     }
 }
 
+impl<'db> Type<'db> {
+    pub(crate) fn substitute_one_typevar(
+        self,
+        db: &'db dyn Db,
+        bound_typevar: BoundTypeVarInstance<'db>,
+        replacement: Type<'db>,
+    ) -> Type<'db> {
+        self.apply_type_mapping(
+            db,
+            &TypeMapping::ApplySpecialization(ApplySpecialization::Single(
+                bound_typevar,
+                replacement,
+            )),
+            TypeContext::default(),
+        )
+    }
+}
+
 /// Performs type inference between parameter annotations and argument types, producing a
 /// specialization of a generic function.
 pub(crate) struct SpecializationBuilder<'db, 'c> {