From 26fa5c208014c671d6a8fd29f0d17e4abab18216 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Wed, 26 Aug 2026 17:19:35 +0200
Subject: [PATCH 01/11] [ty] Preserve type variables in invariant
 materialization subtyping

---
 .../resources/mdtest/narrow/isinstance.md     |  8 +++-
 .../resources/mdtest/narrow/match.md          |  7 +++-
 .../type_properties/is_disjoint_from.md       |  2 +
 .../mdtest/type_properties/materialization.md | 25 ++++++++++++
 .../ty_python_semantic/src/types/generics.rs  | 39 ++++++-------------
 .../ty_python_semantic/src/types/relation.rs  | 28 ++++++-------
 6 files changed, 64 insertions(+), 45 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
index 4d9ccf1d0719d..6bfbcc25000b0 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1452,6 +1452,10 @@ def _(x: object):
 Narrowing must therefore preserve the original type argument instead of substituting `Box`'s
 default.
 
+The `T` alternative can itself be a subclass of both `str` and `Box`, with a different type
+argument. That alternative remains possible in the positive branch, so returning `value` as `Box[T]`
+is unsafe.
+
 ```py
 from typing import assert_never
 
@@ -1462,8 +1466,8 @@ class Box[T: str = str]:
 
 def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
     if isinstance(value, Box):
-        reveal_type(value)  # revealed: Box[T@box_with_default]
-        return value
+        reveal_type(value)  # revealed: Box[T@box_with_default] | (T@box_with_default & Top[Box[Unknown]])
+        return value  # error: [invalid-return-type]
 
     if not isinstance(value, Box):
         reveal_type(value)  # revealed: T@box_with_default & ~Top[Box[Unknown]]
diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/match.md b/crates/ty_python_semantic/resources/mdtest/narrow/match.md
index e075ea939175b..af91108f909ca 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/match.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/match.md
@@ -180,6 +180,9 @@ def narrow_sequence_to_list(value: Sequence[int]) -> None:
 A generic class pattern matches every runtime specialization, not only the specialization described
 by its type parameter's default.
 
+The `T` alternative can itself be a subclass of both `str` and `Box`, with a different type
+argument. Matching `Box()` does not establish that this alternative is a `Box[T]`.
+
 ```toml
 [environment]
 python-version = "3.13"
@@ -199,8 +202,8 @@ class Box[T: str = str]:
 def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
     match value:
         case Box():
-            reveal_type(value)  # revealed: Box[T@box_with_default]
-            return value
+            reveal_type(value)  # revealed: Box[T@box_with_default] | (T@box_with_default & Top[Box[Unknown]])
+            return value  # error: [invalid-return-type]
         case remaining:
             reveal_type(remaining)  # revealed: T@box_with_default & ~Top[Box[Unknown]]
             return Box[T](remaining)
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 360d525b9fbfc..1a1426ff5b6c0 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
@@ -1169,6 +1169,8 @@ type Id[V] = V
 def _[U]():
     static_assert(not is_disjoint_from(Invariant[U], Invariant[int]))
     static_assert(not is_disjoint_from(Invariant[Id[U]], Invariant[int]))
+    static_assert(not is_disjoint_from(Invariant[list[U]], Invariant[list[int]]))
+    static_assert(not is_disjoint_from(Invariant[U], Invariant[Never]))
 
 static_assert(not is_disjoint_from(Invariant[Id[int]], Invariant[int]))
 static_assert(is_disjoint_from(Invariant[Id[int]], Invariant[str]))
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index 9de848e9f478e..1cf82ca861b76 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
@@ -1463,6 +1463,31 @@ static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[bool | Any]
 static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[Any]]))
 ```
 
+An unresolved type variable does not necessarily satisfy a materialization's bounds. In particular,
+`list[T]` is not always a subtype of a list whose elements are integers, so both alternatives remain
+in their union.
+
+```pyi
+from typing import TypeVar
+
+T = TypeVar("T")
+
+def unresolved(values: list[T] | Top[list[int & Any]]):
+    static_assert(not is_subtype_of(list[T], Top[list[int & Any]]))
+    static_assert(not is_subtype_of(Top[list[Any]], list[T]))
+    reveal_type(values)  # revealed: list[T@unresolved] | Top[list[int & Any]]
+```
+
+A declared upper bound can establish the required relation without fixing the type variable to one
+particular specialization.
+
+```pyi
+IntT = TypeVar("IntT", bound=int)
+
+def bounded(values: list[IntT]):
+    static_assert(is_subtype_of(list[IntT], Top[list[int & Any]]))
+```
+
 ## Assignability
 
 ### General
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 2ee5fa20f054c..18e50591ee51a 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -1707,15 +1707,6 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
                     ty.is_dynamic() || matches!(ty, Type::TypeAlias(_))
                 })
             })
-        ) && (
-            // Avoid the `self.always()` type-variable shortcut in
-            // `check_subtyping_in_invariant_position`: it would incorrectly conclude
-            // that `Top[Inv[Any]] <: Inv[T]` for an unresolved `T`.
-            // TODO: remove this once that shortcut is removed.
-            target
-                .types(db)
-                .iter()
-                .all(|ty| !ty.has_typevar_or_typevar_instance(db, env))
         ) && (
             // Only non-pure redundancy needs a target already equal to its top.
             // Materializing the source otherwise loses the bottom needed to
@@ -2087,24 +2078,10 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
             self.materialization_visitor,
         );
 
-        let is_subtype_of = |source: Type<'db>, target: Type<'db>| {
-            // Lazy comparisons must record the bounds imposed on a type variable by each
-            // materialization. Otherwise, for example, `Top[Inv[Any]] <: Top[Inv[T]]` loses
-            // the incompatible requirements `object <: T` and `T <: Never`.
-            // TODO: Remove the eager workaround and handle it in the respective
-            // `(Type::TypeVar(_), _) | (_, Type::TypeVar(_))` branch of
-            // `TypeRelationChecker::check_type_pair`. Right now, we cannot generally
-            // return `self.always()` from that branch, as that leads to union
-            // simplification, which means that we lose track of type variables
-            // without recording the constraints under which the relation holds.
-            if self.typevar_evaluation == TypeVarEvaluation::Eager
-                && (target.is_type_var() || source.is_type_var())
-            {
-                return self.always();
-            }
-
-            self.check_type_pair(db, source, target)
-        };
+        // Lazy comparisons record the bounds imposed by each materialization. Eager comparisons
+        // must also respect type variables: treating them as unconditional matches can discard
+        // valid alternatives from unions such as `list[T] | Top[list[Any & int]]`.
+        let is_subtype_of = |source, target| self.check_type_pair(db, source, target);
         match (source_materialization, target_materialization) {
             // `source` is a subtype of `target` if the range of materializations covered by `source`
             // is a subset of the range covered by `target`.
@@ -2196,6 +2173,14 @@ impl<'c, 'db> DisjointnessChecker<'_, 'c, 'db> {
                     let left_type = left_type.resolve_type_alias(db);
                     let right_type = right_type.resolve_type_alias(db);
 
+                    // Failing to prove equality does not establish disjointness when an argument
+                    // contains a type variable: `list[T]` and `list[int]` overlap if `T = int`.
+                    // Even `Never` is a possible specialization, so argument disjointness alone
+                    // cannot rule out overlap between the enclosing generic types.
+                    if left_type.has_typevar(db, self.env) || right_type.has_typevar(db, self.env) {
+                        return self.never();
+                    }
+
                     // `Bottom[L] <: Top[R]` asks whether the materialization ranges for `L`
                     // and `R` have any common materialization, so this is symmetric despite
                     // using a directional subtyping checker.
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index c1653d9187b57..cf154116c9bf5 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -14,7 +14,7 @@ use crate::types::cyclic::{HasIdentity, PairVisitor, TypeIdentity};
 use crate::types::enums::is_single_member_enum;
 use crate::types::function::FunctionDecorators;
 use crate::types::set_theoretic::RecursivelyDefined;
-use crate::types::signatures::{ParametersKind, SignatureRelationVisitor};
+use crate::types::signatures::{Parameters, ParametersKind, SignatureRelationVisitor};
 use crate::types::tuple::TupleType;
 use crate::types::{
     ApplyTypeMappingVisitor, CallableType, ClassBase, ClassLiteral, ClassType, CycleDetector,
@@ -1755,14 +1755,23 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                 self.always()
             }
 
-            // Any concrete specialization of a `ParamSpec` is a subtype of the top
-            // materialization of a `ParamSpec` value.
+            // Compare fixed `ParamSpec`s through their callable-shaped parameter values. This
+            // preserves both ends of the materialization range of `...`: its bottom is below
+            // every `ParamSpec`, and its top is above every `ParamSpec`.
             (Type::TypeVar(bound_typevar), Type::Callable(other))
+            | (Type::Callable(other), Type::TypeVar(bound_typevar))
                 if !bound_typevar.is_inferable(db, self.inferable)
                     && bound_typevar.is_paramspec(db)
-                    && Self::is_top_paramspec_value(db, other) =>
+                    && other.kind(db) == CallableTypeKind::ParamSpecValue =>
             {
-                self.always()
+                let paramspec =
+                    Type::paramspec_value_callable(db, Parameters::paramspec(db, bound_typevar));
+                let (source, target) = if source.is_type_var() {
+                    (paramspec, target)
+                } else {
+                    (source, paramspec)
+                };
+                self.check_type_pair(db, source, target)
             }
 
             // A fully static typevar is a subtype of its upper bound, and to something similar to
@@ -2757,15 +2766,6 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                 .iter()
                 .all(|signature| signature.parameters().kind() == ParametersKind::Gradual)
     }
-
-    /// Returns `true` if `callable` is the top materialization of a `ParamSpec` value.
-    fn is_top_paramspec_value(db: &'db dyn Db, callable: CallableType<'db>) -> bool {
-        callable.kind(db) == CallableTypeKind::ParamSpecValue
-            && callable
-                .signatures(db)
-                .iter()
-                .all(|signature| signature.parameters().kind() == ParametersKind::Top)
-    }
 }
 
 pub(super) struct EquivalenceChecker<'a, 'c, 'db> {

From 55aa8f40b65a717299e2bc6fe6a4981490dbc8b0 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Thu, 27 Aug 2026 09:02:15 +0200
Subject: [PATCH 02/11] [ty] Match invariant materialization regression to
 issue 4201

---
 .../mdtest/type_properties/materialization.md   | 17 ++++++++++++++++-
 1 file changed, 16 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index 1cf82ca861b76..294f1c1bb9fab 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
@@ -1391,6 +1391,11 @@ def generic_recursive_materialization(value: Top[Covariant[GenericRecursive[int]
 
 ## Subtyping
 
+```toml
+[environment]
+python-version = "3.12"
+```
+
 Any `list[T]` is a subtype of `Top[list[Any]]`, but with more restrictive gradual types, not all
 other specializations are subtypes.
 
@@ -1474,10 +1479,20 @@ T = TypeVar("T")
 
 def unresolved(values: list[T] | Top[list[int & Any]]):
     static_assert(not is_subtype_of(list[T], Top[list[int & Any]]))
-    static_assert(not is_subtype_of(Top[list[Any]], list[T]))
     reveal_type(values)  # revealed: list[T@unresolved] | Top[list[int & Any]]
 ```
 
+Likewise, `Top[list[Unknown]]` includes lists with any element type, so it is not a subtype of
+`list[T]` for an arbitrary `T`. This is a regression test for
+[ty#4201](https://github.com/astral-sh/ty/issues/4201).
+
+```pyi
+from ty_extensions._internal import Unknown
+
+def _[T](value: T):
+    static_assert(not is_subtype_of(Top[list[Unknown]], list[T]))
+```
+
 A declared upper bound can establish the required relation without fixing the type variable to one
 particular specialization.
 

From 37ec0a8f93451f1c6e86304ff126d0ced0497420 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Thu, 27 Aug 2026 10:48:56 +0200
Subject: [PATCH 03/11] Preserve fixed prefixes in ParamSpec assignability

---
 .../mdtest/type_properties/materialization.md | 31 +++++++++++++++++++
 .../ty_python_semantic/src/types/relation.rs  |  8 ++++-
 2 files changed, 38 insertions(+), 1 deletion(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index 294f1c1bb9fab..a3749490c6390 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
@@ -279,6 +279,37 @@ def takes_objects(*args: object, **kwargs: object) -> object:
 static_assert(not is_subtype_of(TopCallable, RegularCallableTypeOf[takes_objects]))
 ```
 
+## `ParamSpec` specializations
+
+For a class invariant in a `ParamSpec`, every fixed specialization lies between the bottom and top
+materializations of its `...` specialization. This holds for both subtyping and assignability. The
+reverse relations do not hold for an arbitrary fixed specialization.
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from typing import Callable
+from ty_extensions import Bottom, Top, static_assert
+from ty_extensions._internal import is_assignable_to, is_subtype_of
+
+class Box[**P]:
+    callback: Callable[P, None]
+
+def _[**P](value: Box[P]):
+    static_assert(is_subtype_of(Box[P], Top[Box[...]]))
+    static_assert(is_subtype_of(Bottom[Box[...]], Box[P]))
+    static_assert(not is_subtype_of(Top[Box[...]], Box[P]))
+    static_assert(not is_subtype_of(Box[P], Bottom[Box[...]]))
+
+    static_assert(is_assignable_to(Box[P], Top[Box[...]]))
+    static_assert(is_assignable_to(Bottom[Box[...]], Box[P]))
+    static_assert(not is_assignable_to(Top[Box[...]], Box[P]))
+    static_assert(not is_assignable_to(Box[P], Bottom[Box[...]]))
+```
+
 ## Tuple
 
 All positions in a tuple are covariant.
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index cf154116c9bf5..03fed07519688 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -1758,11 +1758,17 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
             // Compare fixed `ParamSpec`s through their callable-shaped parameter values. This
             // preserves both ends of the materialization range of `...`: its bottom is below
             // every `ParamSpec`, and its top is above every `ParamSpec`.
+            // Gradual `Concatenate` values still require a fixed prefix, so they cannot stand in
+            // for an arbitrary fixed `ParamSpec`. Bare `...` assignability is handled above.
             (Type::TypeVar(bound_typevar), Type::Callable(other))
             | (Type::Callable(other), Type::TypeVar(bound_typevar))
                 if !bound_typevar.is_inferable(db, self.inferable)
                     && bound_typevar.is_paramspec(db)
-                    && other.kind(db) == CallableTypeKind::ParamSpecValue =>
+                    && other.kind(db) == CallableTypeKind::ParamSpecValue
+                    && other
+                        .signatures(db)
+                        .iter()
+                        .all(|signature| !signature.parameters().is_gradual()) =>
             {
                 let paramspec =
                     Type::paramspec_value_callable(db, Parameters::paramspec(db, bound_typevar));

From a30f83ade9d8cbc6cbe58cddf3498c520bfa473b Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 10:25:13 +0200
Subject: [PATCH 04/11] [ty] Fix ParamSpec erasure and nested generic
 disjointness

---
 .../mdtest/generics/pep695/paramspec.md       | 19 +++++++++++
 .../resources/mdtest/narrow/isinstance.md     | 24 ++++++++++++++
 .../type_properties/is_disjoint_from.md       | 32 ++++++++++++++++++
 .../ty_python_semantic/src/types/generics.rs  | 33 +++++++++----------
 .../ty_python_semantic/src/types/relation.rs  | 17 +++++-----
 .../src/types/signatures.rs                   | 13 ++++++++
 6 files changed, 112 insertions(+), 26 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/paramspec.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/paramspec.md
index 2e79e36d72e79..2951c2687c244 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/paramspec.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/paramspec.md
@@ -463,6 +463,25 @@ takes_int_job(defaulted_job)
 takes_int_job(wrong_job)  # error: [invalid-argument-type]
 ```
 
+A fixed `ParamSpec` can contain required parameters. A wrapper around such a callback cannot be used
+as a wrapper around a callback that accepts no arguments.
+
+```py
+def erase_parameters[**P](job: Job[P]) -> Job[[]]:
+    return job  # error: [invalid-return-type]
+```
+
+The same restriction applies in the other direction when a class consumes callbacks. A consumer of
+callbacks with no parameters cannot accept a callback with arbitrary required parameters.
+
+```py
+class CallbackConsumer[**P]:
+    def consume(self, callback: Callable[P, None]) -> None: ...
+
+def broaden_parameters[**P](consumer: CallbackConsumer[[]]) -> CallbackConsumer[P]:
+    return consumer  # error: [invalid-return-type]
+```
+
 ## `ParamSpec` cannot specialize a `TypeVar`, and vice versa
 
 <!-- snapshot-diagnostics -->
diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
index 6bfbcc25000b0..65d776b76256d 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1312,6 +1312,30 @@ def _(xs: list[str] | set[str]) -> str:
         return "it's a set!"
 ```
 
+## Narrowing incompatible invariant specializations
+
+Subclasses of the same invariant generic class are disjoint when their type arguments cannot be
+equal. A nested type variable does not prevent this proof: `list[T]` cannot equal `int` for any `T`.
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from typing import assert_never
+
+class Box[T]:
+    value: T
+
+class Nested[T](Box[list[T]]): ...
+class IntBox(Box[int]): ...
+
+def narrow[T](value: Nested[T]):
+    if isinstance(value, IntBox):
+        assert_never(value)
+```
+
 ## Narrowing recursively bounded generics (strict mode)
 
 An `isinstance()` check must not recurse indefinitely when a generic bound refers to its own class.
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 1a1426ff5b6c0..48129664c4a68 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
@@ -1188,6 +1188,38 @@ class Both(Left, Right): ...
 static_assert(not is_disjoint_from(Left, Right))
 ```
 
+### Nested type variables in invariant arguments
+
+An invariant argument can contain a type variable and still be incompatible with another argument.
+For example, `list[T]` cannot equal `int`, regardless of the specialization of `T`.
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from ty_extensions import static_assert
+from ty_extensions._internal import is_disjoint_from
+
+def incompatible[T]():
+    static_assert(is_disjoint_from(list[list[T]], list[int]))
+    static_assert(is_disjoint_from(list[int], list[list[T]]))
+    static_assert(is_disjoint_from(list[tuple[T, int]], list[tuple[T, str]]))
+    static_assert(is_disjoint_from(list[tuple[T, str]], list[tuple[T, int]]))
+```
+
+When the surrounding structure matches, the arguments can instead be equal for some specialization.
+Aliases preserve that possibility, including aliases nested inside the argument.
+
+```py
+type Id[T] = T
+
+def compatible[T]():
+    static_assert(not is_disjoint_from(list[list[T]], list[list[int]]))
+    static_assert(not is_disjoint_from(list[list[Id[T]]], list[list[int]]))
+```
+
 ### NewTypes and overlapping types
 
 A `NewType` overlaps with any nominal or structural type that overlaps its concrete base. This
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 18e50591ee51a..907fd6c4b5c06 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -2173,26 +2173,25 @@ impl<'c, 'db> DisjointnessChecker<'_, 'c, 'db> {
                     let left_type = left_type.resolve_type_alias(db);
                     let right_type = right_type.resolve_type_alias(db);
 
-                    // Failing to prove equality does not establish disjointness when an argument
-                    // contains a type variable: `list[T]` and `list[int]` overlap if `T = int`.
-                    // Even `Never` is a possible specialization, so argument disjointness alone
-                    // cannot rule out overlap between the enclosing generic types.
-                    if left_type.has_typevar(db, self.env) || right_type.has_typevar(db, self.env) {
-                        return self.never();
-                    }
-
                     // `Bottom[L] <: Top[R]` asks whether the materialization ranges for `L`
                     // and `R` have any common materialization, so this is symmetric despite
                     // using a directional subtyping checker.
-                    self.as_relation_checker(TypeRelation::Subtyping)
-                        .check_subtyping_in_invariant_position(
-                            db,
-                            left_type,
-                            MaterializationKind::Bottom,
-                            right_type,
-                            MaterializationKind::Top,
-                        )
-                        .negate(db, self.constraints)
+                    // Keep type-variable comparisons as constraints: `list[T]` can equal
+                    // `list[int]` when `T = int`, but cannot equal `int` for any `T`. Disjointness
+                    // requires that no specialization satisfies the overlap constraints.
+                    let mut checker = self.as_relation_checker(TypeRelation::Subtyping);
+                    checker.typevar_evaluation = TypeVarEvaluation::Lazy;
+                    let overlap = checker.check_subtyping_in_invariant_position(
+                        db,
+                        left_type,
+                        MaterializationKind::Bottom,
+                        right_type,
+                        MaterializationKind::Top,
+                    );
+                    ConstraintSet::from_bool(
+                        self.constraints,
+                        overlap.is_never_satisfied(db, self.env),
+                    )
                 }
 
                 // If `Foo[T]` is covariant in `T`, `Foo[Never]` is a subtype of `Foo[A]` and `Foo[B]`
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index 03fed07519688..cf569b3c99b45 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -1755,20 +1755,19 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                 self.always()
             }
 
-            // Compare fixed `ParamSpec`s through their callable-shaped parameter values. This
-            // preserves both ends of the materialization range of `...`: its bottom is below
-            // every `ParamSpec`, and its top is above every `ParamSpec`.
-            // Gradual `Concatenate` values still require a fixed prefix, so they cannot stand in
-            // for an arbitrary fixed `ParamSpec`. Bare `...` assignability is handled above.
+            // Compare fixed `ParamSpec`s with the endpoints of the materialization range of `...`:
+            // its bottom is below every `ParamSpec`, and its top is above every `ParamSpec`.
+            // Do not expand a fixed `ParamSpec` for ordinary parameter lists. The eager signature
+            // comparison treats `P.args` and `P.kwargs` as optional variadics, but `P` can contain
+            // required parameters, so `P` is not necessarily compatible with an empty list.
             (Type::TypeVar(bound_typevar), Type::Callable(other))
             | (Type::Callable(other), Type::TypeVar(bound_typevar))
                 if !bound_typevar.is_inferable(db, self.inferable)
                     && bound_typevar.is_paramspec(db)
                     && other.kind(db) == CallableTypeKind::ParamSpecValue
-                    && other
-                        .signatures(db)
-                        .iter()
-                        .all(|signature| !signature.parameters().is_gradual()) =>
+                    && other.signatures(db).iter().all(|signature| {
+                        signature.parameters().is_top() || signature.parameters().is_bottom()
+                    }) =>
             {
                 let paramspec =
                     Type::paramspec_value_callable(db, Parameters::paramspec(db, bound_typevar));
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index f1bfb0ab95183..08e81e290388e 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -4707,6 +4707,19 @@ impl<'db> Parameters<'db> {
         matches!(self.data.kind, ParametersKind::Top)
     }
 
+    /// Returns whether the parameters are `(*object, **object)`, which accepts every call.
+    pub(crate) fn is_bottom(&self) -> bool {
+        self.is_standard()
+            && matches!(
+                self.as_slice(),
+                [variadic, keyword_variadic]
+                    if variadic.is_variadic()
+                        && variadic.annotated_type().is_object()
+                        && keyword_variadic.is_keyword_variadic()
+                        && keyword_variadic.annotated_type().is_object()
+            )
+    }
+
     /// Returns `true` if the parameters are a standard parameter list (not gradual, top,
     /// `ParamSpec`, or `Concatenate`).
     pub(crate) fn is_standard(&self) -> bool {

From a48e5bd9307d9366de470bd2202f50b4aa5450b3 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 11:27:32 +0200
Subject: [PATCH 05/11] [ty] Respect TypeVar declarations in invariant
 disjointness

Validate possible overlap against TypeVar bounds and constraints, while retaining incompatible union alternatives so inference can still report argument errors. Add coverage for bounded and constrained nested type variables.

Compare fixed ParamSpecs directly with materialization endpoints and clarify the parameter kind distinction between top and bottom.
---
 .../resources/mdtest/narrow/isinstance.md     | 16 ++++++++
 .../type_properties/is_disjoint_from.md       | 24 ++++++++++++
 crates/ty_python_semantic/src/types.rs        |  9 +++--
 .../src/types/constraints.rs                  |  3 +-
 .../src/types/constraints/projection.rs       | 29 +++++++++++++++
 .../src/types/constraints/projection/tests.rs | 37 ++++++++++++++++++-
 .../ty_python_semantic/src/types/generics.rs  |  5 ++-
 .../ty_python_semantic/src/types/relation.rs  | 15 +++-----
 .../src/types/signatures.rs                   |  1 +
 9 files changed, 122 insertions(+), 17 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
index 65d776b76256d..b38b6f8cb6b0e 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1336,6 +1336,22 @@ def narrow[T](value: Nested[T]):
         assert_never(value)
 ```
 
+Bounds and constraints can also make two nested arguments incompatible. If `T` is bounded by `str`
+or constrained to `str` and `bytes`, `list[T]` cannot equal `list[int]`, so the positive branch is
+unreachable.
+
+```py
+class IntListBox(Box[list[int]]): ...
+
+def narrow_bounded[T: str](value: Nested[T]):
+    if isinstance(value, IntListBox):
+        assert_never(value)
+
+def narrow_constrained[T: (str, bytes)](value: Nested[T]):
+    if isinstance(value, IntListBox):
+        assert_never(value)
+```
+
 ## Narrowing recursively bounded generics (strict mode)
 
 An `isinstance()` check must not recurse indefinitely when a generic bound refers to its own class.
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 48129664c4a68..27498a6095f27 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
@@ -1220,6 +1220,30 @@ def compatible[T]():
     static_assert(not is_disjoint_from(list[list[Id[T]]], list[list[int]]))
 ```
 
+An upper bound can rule out equality even when the surrounding structure matches. A type variable
+bounded by `str` cannot specialize to `int`, but it can specialize to `str` or `Never`.
+
+```py
+from typing import Never
+
+def bounded[T: str]():
+    static_assert(is_disjoint_from(list[list[T]], list[list[int]]))
+    static_assert(is_disjoint_from(list[list[int]], list[list[T]]))
+    static_assert(not is_disjoint_from(list[list[T]], list[list[str]]))
+    static_assert(not is_disjoint_from(list[list[T]], list[list[Never]]))
+```
+
+A constrained type variable can only specialize to one of its constraints. Neither `str` nor `bytes`
+equals `int`; matching either constraint is enough to preserve a possible overlap.
+
+```py
+def constrained[T: (str, bytes)]():
+    static_assert(is_disjoint_from(list[list[T]], list[list[int]]))
+    static_assert(is_disjoint_from(list[list[int]], list[list[T]]))
+    static_assert(not is_disjoint_from(list[list[T]], list[list[str]]))
+    static_assert(not is_disjoint_from(list[list[T]], list[list[bytes]]))
+```
+
 ### NewTypes and overlapping types
 
 A `NewType` overlaps with any nominal or structural type that overlaps its concrete base. This
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index fa4895159fbe2..dc24b6e3eaca1 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -2876,7 +2876,9 @@ impl<'db> Type<'db> {
 
     /// If the type is a union, removes union elements that are disjoint from `target`.
     ///
-    /// Otherwise, returns the type unchanged.
+    /// Returns the type unchanged if it is not a union or every alternative is disjoint. Inference
+    /// must still visit incompatible alternatives to report bound errors instead of inferring from
+    /// `Never` and losing the failure.
     fn filter_disjoint_elements(
         self,
         db: &'db dyn Db,
@@ -2885,11 +2887,12 @@ impl<'db> Type<'db> {
         inferable: TypeVarSet<'db>,
     ) -> Type<'db> {
         let constraints = ConstraintSetBuilder::new();
-        self.filter_union(db, env, |elem| {
+        let filtered = self.filter_union(db, env, |elem| {
             !elem
                 .when_disjoint_from(db, env, target, &constraints, inferable)
                 .is_always_satisfied(db, env)
-        })
+        });
+        if filtered.is_never() { self } else { filtered }
     }
 
     /// Returns the fallback instance type that a literal is an instance of, or `None` if the type
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 0c394fbfa9f9f..c2ea866ef0a1d 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -509,7 +509,8 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         debug_assert!(std::ptr::eq(self.builder, builder));
     }
 
-    /// Returns whether this constraint set never holds.
+    /// Returns whether this constraint set never holds, without applying the type variables'
+    /// declared bounds or constraints. Use [`Self::has_no_valid_solutions`] to include those.
     pub(crate) fn is_never_satisfied(self, db: &'db dyn Db, env: &ProgramEnvironment<'db>) -> bool {
         let mut storage = self.builder.storage.borrow_mut();
         self.node
diff --git a/crates/ty_python_semantic/src/types/constraints/projection.rs b/crates/ty_python_semantic/src/types/constraints/projection.rs
index 86ad764a68072..de787090f86eb 100644
--- a/crates/ty_python_semantic/src/types/constraints/projection.rs
+++ b/crates/ty_python_semantic/src/types/constraints/projection.rs
@@ -108,6 +108,35 @@ impl ProjectionTypeBudget {
 }
 
 impl<'db> ConstraintSet<'db, '_> {
+    /// Returns whether no specialization satisfying the type variables' declared bounds and
+    /// constraints can satisfy this constraint set.
+    ///
+    /// Unlike [`Self::is_never_satisfied`], this validates the solutions against their declarations.
+    /// Exhausting the solution budget does not prove that the set is unsatisfiable.
+    pub(crate) fn has_no_valid_solutions(
+        self,
+        db: &'db dyn Db,
+        env: &ProgramEnvironment<'db>,
+    ) -> bool {
+        if self.is_never_satisfied(db, env) {
+            return true;
+        }
+
+        let inferable = {
+            let storage = self.builder.storage.borrow();
+            let Some(support) = storage.node_support(self.node) else {
+                return false;
+            };
+            // For overlap, every mentioned type variable can choose a valid specialization.
+            TypeVarSet::from_typevars(db, support.iter().map(|id| storage.typevar_data(id)))
+        };
+
+        matches!(
+            self.solutions(db, env, inferable),
+            Ok(Solutions::Unsatisfiable)
+        )
+    }
+
     /// Computes default solutions for each BDD path within the default projection budget.
     pub(crate) fn solutions(
         self,
diff --git a/crates/ty_python_semantic/src/types/constraints/projection/tests.rs b/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
index 7d636a791f819..fbd3680684b16 100644
--- a/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
+++ b/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
@@ -12,9 +12,10 @@ use crate::types::constraints::{
     ConstraintSet, ConstraintSetBuilder, IteratorConstraintsExtension, PathBound,
     PathBoundSolution, PathBounds, Solution, SolutionPaths, Solutions, TypeVarSolution,
 };
-use crate::types::typevar::TypeVarSet;
+use crate::types::typevar::{TypeVarConstraints, TypeVarSet};
 use crate::types::{
-    BoundTypeVarInstance, IntersectionType, KnownClass, Type, TypeVarVariance, UnionType,
+    BoundTypeVarInstance, IntersectionType, KnownClass, Type, TypeVarBoundOrConstraints,
+    TypeVarVariance, UnionType,
 };
 
 type Paths<'db> = FxHashSet<Solution<'db>>;
@@ -140,6 +141,38 @@ fn path_limit_is_checked_before_solving() {
     }
 }
 
+#[test]
+fn satisfiability_respects_declared_bounds_and_constraints() {
+    let db = setup_db();
+    let db = &db;
+    let env = db.program_environment();
+    let int = known_instance(db, KnownClass::Int);
+    let str = known_instance(db, KnownClass::Str);
+    let bytes = known_instance(db, KnownClass::Bytes);
+    let bounded = create_typevar(db, "Bounded")
+        .map_bound_or_constraints(db, |_| Some(TypeVarBoundOrConstraints::UpperBound(str)));
+    let constrained = create_typevar(db, "Constrained").map_bound_or_constraints(db, |_| {
+        Some(TypeVarBoundOrConstraints::Constraints(
+            TypeVarConstraints::new(db, [str, bytes].as_slice()),
+        ))
+    });
+    let builder = ConstraintSetBuilder::new();
+
+    assert!(!ConstraintSet::always(&builder).has_no_valid_solutions(db, &env));
+    assert!(ConstraintSet::never(&builder).has_no_valid_solutions(db, &env));
+
+    for typevar in [bounded, constrained] {
+        let invalid = exact(db, &builder, typevar, int);
+        assert!(!invalid.is_never_satisfied(db, &env));
+        assert!(invalid.has_no_valid_solutions(db, &env));
+        assert!(!exact(db, &builder, typevar, str).has_no_valid_solutions(db, &env));
+    }
+
+    assert!(!exact(db, &builder, bounded, Type::Never).has_no_valid_solutions(db, &env));
+    assert!(!exact(db, &builder, constrained, bytes).has_no_valid_solutions(db, &env));
+    assert!(exact(db, &builder, constrained, Type::Never).has_no_valid_solutions(db, &env));
+}
+
 #[test]
 fn terminal_projections_need_no_paths_or_types() {
     let db = setup_db();
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 907fd6c4b5c06..045edb7cd6043 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -2178,7 +2178,8 @@ impl<'c, 'db> DisjointnessChecker<'_, 'c, 'db> {
                     // using a directional subtyping checker.
                     // Keep type-variable comparisons as constraints: `list[T]` can equal
                     // `list[int]` when `T = int`, but cannot equal `int` for any `T`. Disjointness
-                    // requires that no specialization satisfies the overlap constraints.
+                    // requires that no valid specialization satisfies the overlap constraints,
+                    // including the type variables' declared bounds and constraints.
                     let mut checker = self.as_relation_checker(TypeRelation::Subtyping);
                     checker.typevar_evaluation = TypeVarEvaluation::Lazy;
                     let overlap = checker.check_subtyping_in_invariant_position(
@@ -2190,7 +2191,7 @@ impl<'c, 'db> DisjointnessChecker<'_, 'c, 'db> {
                     );
                     ConstraintSet::from_bool(
                         self.constraints,
-                        overlap.is_never_satisfied(db, self.env),
+                        overlap.has_no_valid_solutions(db, self.env),
                     )
                 }
 
diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index cf569b3c99b45..5fbb48a16aa7a 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -14,7 +14,7 @@ use crate::types::cyclic::{HasIdentity, PairVisitor, TypeIdentity};
 use crate::types::enums::is_single_member_enum;
 use crate::types::function::FunctionDecorators;
 use crate::types::set_theoretic::RecursivelyDefined;
-use crate::types::signatures::{Parameters, ParametersKind, SignatureRelationVisitor};
+use crate::types::signatures::{ParametersKind, SignatureRelationVisitor};
 use crate::types::tuple::TupleType;
 use crate::types::{
     ApplyTypeMappingVisitor, CallableType, ClassBase, ClassLiteral, ClassType, CycleDetector,
@@ -1769,14 +1769,11 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                         signature.parameters().is_top() || signature.parameters().is_bottom()
                     }) =>
             {
-                let paramspec =
-                    Type::paramspec_value_callable(db, Parameters::paramspec(db, bound_typevar));
-                let (source, target) = if source.is_type_var() {
-                    (paramspec, target)
-                } else {
-                    (source, paramspec)
-                };
-                self.check_type_pair(db, source, target)
+                let other_is_top = other
+                    .signatures(db)
+                    .iter()
+                    .all(|signature| signature.parameters().is_top());
+                ConstraintSet::from_bool(self.constraints, source.is_type_var() == other_is_top)
             }
 
             // A fully static typevar is a subtype of its upper bound, and to something similar to
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index 08e81e290388e..cb8a4aec30d07 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -4709,6 +4709,7 @@ impl<'db> Parameters<'db> {
 
     /// Returns whether the parameters are `(*object, **object)`, which accepts every call.
     pub(crate) fn is_bottom(&self) -> bool {
+        // Top parameters store the same variadics; their kind distinguishes them from bottom.
         self.is_standard()
             && matches!(
                 self.as_slice(),

From 06d1fa6a552d3d46c2d701ceb2cc4fe9444cd393 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 13:08:48 +0200
Subject: [PATCH 06/11] [ty] Restore the top ParamSpec value helper

---
 crates/ty_python_semantic/src/types/relation.rs | 14 ++++++++++----
 1 file changed, 10 insertions(+), 4 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index 5fbb48a16aa7a..c099be91a88ad 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -1769,10 +1769,7 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                         signature.parameters().is_top() || signature.parameters().is_bottom()
                     }) =>
             {
-                let other_is_top = other
-                    .signatures(db)
-                    .iter()
-                    .all(|signature| signature.parameters().is_top());
+                let other_is_top = Self::is_top_paramspec_value(db, other);
                 ConstraintSet::from_bool(self.constraints, source.is_type_var() == other_is_top)
             }
 
@@ -2768,6 +2765,15 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                 .iter()
                 .all(|signature| signature.parameters().kind() == ParametersKind::Gradual)
     }
+
+    /// Returns `true` if `callable` is the top materialization of a `ParamSpec` value.
+    fn is_top_paramspec_value(db: &'db dyn Db, callable: CallableType<'db>) -> bool {
+        callable.kind(db) == CallableTypeKind::ParamSpecValue
+            && callable
+                .signatures(db)
+                .iter()
+                .all(|signature| signature.parameters().kind() == ParametersKind::Top)
+    }
 }
 
 pub(super) struct EquivalenceChecker<'a, 'c, 'db> {

From 413d4dce3a0b9e71172ad24c15b29323d0ebffb0 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 14:18:59 +0200
Subject: [PATCH 07/11] [ty] Consolidate invariant materialization regression
 tests

---
 .../resources/mdtest/narrow/isinstance.md     | 21 ++---------
 .../type_properties/is_disjoint_from.md       | 11 +++---
 .../mdtest/type_properties/materialization.md | 33 +++++------------
 .../src/types/constraints/projection/tests.rs | 37 +------------------
 4 files changed, 20 insertions(+), 82 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
index b38b6f8cb6b0e..423e7a5c56507 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1315,7 +1315,8 @@ def _(xs: list[str] | set[str]) -> str:
 ## Narrowing incompatible invariant specializations
 
 Subclasses of the same invariant generic class are disjoint when their type arguments cannot be
-equal. A nested type variable does not prevent this proof: `list[T]` cannot equal `int` for any `T`.
+equal. Here, `T` is bounded by `str`, so `list[T]` cannot equal `list[int]` and the positive branch
+is unreachable.
 
 ```toml
 [environment]
@@ -1329,25 +1330,9 @@ class Box[T]:
     value: T
 
 class Nested[T](Box[list[T]]): ...
-class IntBox(Box[int]): ...
-
-def narrow[T](value: Nested[T]):
-    if isinstance(value, IntBox):
-        assert_never(value)
-```
-
-Bounds and constraints can also make two nested arguments incompatible. If `T` is bounded by `str`
-or constrained to `str` and `bytes`, `list[T]` cannot equal `list[int]`, so the positive branch is
-unreachable.
-
-```py
 class IntListBox(Box[list[int]]): ...
 
-def narrow_bounded[T: str](value: Nested[T]):
-    if isinstance(value, IntListBox):
-        assert_never(value)
-
-def narrow_constrained[T: (str, bytes)](value: Nested[T]):
+def narrow[T: str](value: Nested[T]):
     if isinstance(value, IntListBox):
         assert_never(value)
 ```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 27498a6095f27..71bd22cbb9471 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
@@ -1169,8 +1169,6 @@ type Id[V] = V
 def _[U]():
     static_assert(not is_disjoint_from(Invariant[U], Invariant[int]))
     static_assert(not is_disjoint_from(Invariant[Id[U]], Invariant[int]))
-    static_assert(not is_disjoint_from(Invariant[list[U]], Invariant[list[int]]))
-    static_assert(not is_disjoint_from(Invariant[U], Invariant[Never]))
 
 static_assert(not is_disjoint_from(Invariant[Id[int]], Invariant[int]))
 static_assert(is_disjoint_from(Invariant[Id[int]], Invariant[str]))
@@ -1199,6 +1197,7 @@ python-version = "3.12"
 ```
 
 ```py
+from typing import Never
 from ty_extensions import static_assert
 from ty_extensions._internal import is_disjoint_from
 
@@ -1218,14 +1217,13 @@ type Id[T] = T
 def compatible[T]():
     static_assert(not is_disjoint_from(list[list[T]], list[list[int]]))
     static_assert(not is_disjoint_from(list[list[Id[T]]], list[list[int]]))
+    static_assert(not is_disjoint_from(list[list[T]], list[list[Never]]))
 ```
 
 An upper bound can rule out equality even when the surrounding structure matches. A type variable
 bounded by `str` cannot specialize to `int`, but it can specialize to `str` or `Never`.
 
 ```py
-from typing import Never
-
 def bounded[T: str]():
     static_assert(is_disjoint_from(list[list[T]], list[list[int]]))
     static_assert(is_disjoint_from(list[list[int]], list[list[T]]))
@@ -1233,13 +1231,14 @@ def bounded[T: str]():
     static_assert(not is_disjoint_from(list[list[T]], list[list[Never]]))
 ```
 
-A constrained type variable can only specialize to one of its constraints. Neither `str` nor `bytes`
-equals `int`; matching either constraint is enough to preserve a possible overlap.
+A constrained type variable can only specialize to one of its constraints. Neither `int` nor `Never`
+is a valid specialization, while matching either `str` or `bytes` preserves a possible overlap.
 
 ```py
 def constrained[T: (str, bytes)]():
     static_assert(is_disjoint_from(list[list[T]], list[list[int]]))
     static_assert(is_disjoint_from(list[list[int]], list[list[T]]))
+    static_assert(is_disjoint_from(list[list[T]], list[list[Never]]))
     static_assert(not is_disjoint_from(list[list[T]], list[list[str]]))
     static_assert(not is_disjoint_from(list[list[T]], list[list[bytes]]))
 ```
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index a3749490c6390..2be3257fd1e3d 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
@@ -298,7 +298,7 @@ from ty_extensions._internal import is_assignable_to, is_subtype_of
 class Box[**P]:
     callback: Callable[P, None]
 
-def _[**P](value: Box[P]):
+def _[**P]():
     static_assert(is_subtype_of(Box[P], Top[Box[...]]))
     static_assert(is_subtype_of(Bottom[Box[...]], Box[P]))
     static_assert(not is_subtype_of(Top[Box[...]], Box[P]))
@@ -1499,39 +1499,26 @@ static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[bool | Any]
 static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[Any]]))
 ```
 
-An unresolved type variable does not necessarily satisfy a materialization's bounds. In particular,
-`list[T]` is not always a subtype of a list whose elements are integers, so both alternatives remain
-in their union.
-
-```pyi
-from typing import TypeVar
-
-T = TypeVar("T")
-
-def unresolved(values: list[T] | Top[list[int & Any]]):
-    static_assert(not is_subtype_of(list[T], Top[list[int & Any]]))
-    reveal_type(values)  # revealed: list[T@unresolved] | Top[list[int & Any]]
-```
-
-Likewise, `Top[list[Unknown]]` includes lists with any element type, so it is not a subtype of
-`list[T]` for an arbitrary `T`. This is a regression test for
-[ty#4201](https://github.com/astral-sh/ty/issues/4201).
+An unresolved type variable does not necessarily satisfy a materialization's bounds. Conversely,
+`Top[list[Unknown]]` includes specializations that do not match an arbitrary fixed `T`, as in
+[ty#4201](https://github.com/astral-sh/ty/issues/4201). Neither comparison below holds for every
+`T`, and the union retains both alternatives.
 
 ```pyi
 from ty_extensions._internal import Unknown
 
-def _[T](value: T):
+def unresolved[T](values: list[T] | Top[list[int & Any]]):
+    static_assert(not is_subtype_of(list[T], Top[list[int & Any]]))
     static_assert(not is_subtype_of(Top[list[Unknown]], list[T]))
+    reveal_type(values)  # revealed: list[T@unresolved] | Top[list[int & Any]]
 ```
 
 A declared upper bound can establish the required relation without fixing the type variable to one
 particular specialization.
 
 ```pyi
-IntT = TypeVar("IntT", bound=int)
-
-def bounded(values: list[IntT]):
-    static_assert(is_subtype_of(list[IntT], Top[list[int & Any]]))
+def bounded[T: int]():
+    static_assert(is_subtype_of(list[T], Top[list[int & Any]]))
 ```
 
 ## Assignability
diff --git a/crates/ty_python_semantic/src/types/constraints/projection/tests.rs b/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
index fbd3680684b16..7d636a791f819 100644
--- a/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
+++ b/crates/ty_python_semantic/src/types/constraints/projection/tests.rs
@@ -12,10 +12,9 @@ use crate::types::constraints::{
     ConstraintSet, ConstraintSetBuilder, IteratorConstraintsExtension, PathBound,
     PathBoundSolution, PathBounds, Solution, SolutionPaths, Solutions, TypeVarSolution,
 };
-use crate::types::typevar::{TypeVarConstraints, TypeVarSet};
+use crate::types::typevar::TypeVarSet;
 use crate::types::{
-    BoundTypeVarInstance, IntersectionType, KnownClass, Type, TypeVarBoundOrConstraints,
-    TypeVarVariance, UnionType,
+    BoundTypeVarInstance, IntersectionType, KnownClass, Type, TypeVarVariance, UnionType,
 };
 
 type Paths<'db> = FxHashSet<Solution<'db>>;
@@ -141,38 +140,6 @@ fn path_limit_is_checked_before_solving() {
     }
 }
 
-#[test]
-fn satisfiability_respects_declared_bounds_and_constraints() {
-    let db = setup_db();
-    let db = &db;
-    let env = db.program_environment();
-    let int = known_instance(db, KnownClass::Int);
-    let str = known_instance(db, KnownClass::Str);
-    let bytes = known_instance(db, KnownClass::Bytes);
-    let bounded = create_typevar(db, "Bounded")
-        .map_bound_or_constraints(db, |_| Some(TypeVarBoundOrConstraints::UpperBound(str)));
-    let constrained = create_typevar(db, "Constrained").map_bound_or_constraints(db, |_| {
-        Some(TypeVarBoundOrConstraints::Constraints(
-            TypeVarConstraints::new(db, [str, bytes].as_slice()),
-        ))
-    });
-    let builder = ConstraintSetBuilder::new();
-
-    assert!(!ConstraintSet::always(&builder).has_no_valid_solutions(db, &env));
-    assert!(ConstraintSet::never(&builder).has_no_valid_solutions(db, &env));
-
-    for typevar in [bounded, constrained] {
-        let invalid = exact(db, &builder, typevar, int);
-        assert!(!invalid.is_never_satisfied(db, &env));
-        assert!(invalid.has_no_valid_solutions(db, &env));
-        assert!(!exact(db, &builder, typevar, str).has_no_valid_solutions(db, &env));
-    }
-
-    assert!(!exact(db, &builder, bounded, Type::Never).has_no_valid_solutions(db, &env));
-    assert!(!exact(db, &builder, constrained, bytes).has_no_valid_solutions(db, &env));
-    assert!(exact(db, &builder, constrained, Type::Never).has_no_valid_solutions(db, &env));
-}
-
 #[test]
 fn terminal_projections_need_no_paths_or_types() {
     let db = setup_db();

From 26b2c0f72ae6d961a503d9e3f736185b7c22344f Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 15:48:28 +0200
Subject: [PATCH 08/11] [ty] Make disjoint union fallback handling explicit

---
 .../resources/mdtest/narrow/isinstance.md     | 38 +++-------------
 .../resources/mdtest/narrow/match.md          | 12 +++---
 crates/ty_python_semantic/src/types.rs        | 43 ++++++++++++++++---
 .../ty_python_semantic/src/types/call/bind.rs | 15 +++++--
 .../ty_python_semantic/src/types/generics.rs  | 11 ++++-
 .../src/types/infer/builder.rs                | 18 +++++---
 .../src/types/signatures.rs                   |  7 ++-
 7 files changed, 83 insertions(+), 61 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
index 423e7a5c56507..ef13cdb1b9552 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1312,31 +1312,6 @@ def _(xs: list[str] | set[str]) -> str:
         return "it's a set!"
 ```
 
-## Narrowing incompatible invariant specializations
-
-Subclasses of the same invariant generic class are disjoint when their type arguments cannot be
-equal. Here, `T` is bounded by `str`, so `list[T]` cannot equal `list[int]` and the positive branch
-is unreachable.
-
-```toml
-[environment]
-python-version = "3.12"
-```
-
-```py
-from typing import assert_never
-
-class Box[T]:
-    value: T
-
-class Nested[T](Box[list[T]]): ...
-class IntListBox(Box[list[int]]): ...
-
-def narrow[T: str](value: Nested[T]):
-    if isinstance(value, IntListBox):
-        assert_never(value)
-```
-
 ## Narrowing recursively bounded generics (strict mode)
 
 An `isinstance()` check must not recurse indefinitely when a generic bound refers to its own class.
@@ -1477,13 +1452,10 @@ def _(x: object):
 Narrowing must therefore preserve the original type argument instead of substituting `Box`'s
 default.
 
-The `T` alternative can itself be a subclass of both `str` and `Box`, with a different type
-argument. That alternative remains possible in the positive branch, so returning `value` as `Box[T]`
-is unsafe.
-
 ```py
-from typing import assert_never
+from typing import assert_never, final
 
+@final
 class Box[T: str = str]:
     value: T
 
@@ -1491,11 +1463,11 @@ class Box[T: str = str]:
 
 def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
     if isinstance(value, Box):
-        reveal_type(value)  # revealed: Box[T@box_with_default] | (T@box_with_default & Top[Box[Unknown]])
-        return value  # error: [invalid-return-type]
+        reveal_type(value)  # revealed: Box[T@box_with_default]
+        return value
 
     if not isinstance(value, Box):
-        reveal_type(value)  # revealed: T@box_with_default & ~Top[Box[Unknown]]
+        reveal_type(value)  # revealed: T@box_with_default
         return Box[T](value)
 
     assert_never(value)
diff --git a/crates/ty_python_semantic/resources/mdtest/narrow/match.md b/crates/ty_python_semantic/resources/mdtest/narrow/match.md
index af91108f909ca..a4b1afed22ab7 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/match.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/match.md
@@ -180,9 +180,6 @@ def narrow_sequence_to_list(value: Sequence[int]) -> None:
 A generic class pattern matches every runtime specialization, not only the specialization described
 by its type parameter's default.
 
-The `T` alternative can itself be a subclass of both `str` and `Box`, with a different type
-argument. Matching `Box()` does not establish that this alternative is a `Box[T]`.
-
 ```toml
 [environment]
 python-version = "3.13"
@@ -192,8 +189,9 @@ strict-generic-narrowing = true
 ```
 
 ```py
-from typing import Any
+from typing import Any, final
 
+@final
 class Box[T: str = str]:
     value: T
 
@@ -202,10 +200,10 @@ class Box[T: str = str]:
 def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
     match value:
         case Box():
-            reveal_type(value)  # revealed: Box[T@box_with_default] | (T@box_with_default & Top[Box[Unknown]])
-            return value  # error: [invalid-return-type]
+            reveal_type(value)  # revealed: Box[T@box_with_default]
+            return value
         case remaining:
-            reveal_type(remaining)  # revealed: T@box_with_default & ~Top[Box[Unknown]]
+            reveal_type(remaining)  # revealed: T@box_with_default
             return Box[T](remaining)
 ```
 
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index dc24b6e3eaca1..11567782cb19a 100644
--- a/crates/ty_python_semantic/src/types.rs
+++ b/crates/ty_python_semantic/src/types.rs
@@ -1673,6 +1673,33 @@ pub enum Type<'db> {
     NewTypeInstance(NewType<'db>),
 }
 
+/// The result of discarding disjoint elements from a union.
+#[derive(Copy, Clone, Debug, PartialEq, Eq)]
+enum DiscardDisjointUnionElementsResult<'db> {
+    /// The remaining type, or the unchanged input if it is not a union.
+    Retained(Type<'db>),
+    /// Every union element is disjoint from the target.
+    AllDisjoint,
+}
+
+impl<'db> DiscardDisjointUnionElementsResult<'db> {
+    /// Returns the retained type, or `Never` if every union element was disjoint.
+    fn or_never(self) -> Type<'db> {
+        match self {
+            Self::Retained(ty) => ty,
+            Self::AllDisjoint => Type::Never,
+        }
+    }
+
+    /// Returns the retained type, or `original` if every union element was disjoint.
+    fn unless_all_disjoint(self, original: Type<'db>) -> Type<'db> {
+        match self {
+            Self::Retained(ty) => ty,
+            Self::AllDisjoint => original,
+        }
+    }
+}
+
 /// The result of projecting class-object types into the corresponding instance types.
 ///
 /// An exact projection preserves all class-object constraints relevant to a `type[T]` relation;
@@ -2876,23 +2903,27 @@ impl<'db> Type<'db> {
 
     /// If the type is a union, removes union elements that are disjoint from `target`.
     ///
-    /// Returns the type unchanged if it is not a union or every alternative is disjoint. Inference
-    /// must still visit incompatible alternatives to report bound errors instead of inferring from
-    /// `Never` and losing the failure.
-    fn filter_disjoint_elements(
+    /// Returns [`DiscardDisjointUnionElementsResult::AllDisjoint`] if every union element is removed.
+    /// Non-union inputs, including `Never`, are returned unchanged as
+    /// [`DiscardDisjointUnionElementsResult::Retained`].
+    fn discard_disjoint_union_elements(
         self,
         db: &'db dyn Db,
         env: &ProgramEnvironment<'db>,
         target: Type<'db>,
         inferable: TypeVarSet<'db>,
-    ) -> Type<'db> {
+    ) -> DiscardDisjointUnionElementsResult<'db> {
         let constraints = ConstraintSetBuilder::new();
         let filtered = self.filter_union(db, env, |elem| {
             !elem
                 .when_disjoint_from(db, env, target, &constraints, inferable)
                 .is_always_satisfied(db, env)
         });
-        if filtered.is_never() { self } else { filtered }
+        if filtered.is_never() && !self.is_never() {
+            DiscardDisjointUnionElementsResult::AllDisjoint
+        } else {
+            DiscardDisjointUnionElementsResult::Retained(filtered)
+        }
     }
 
     /// Returns the fallback instance type that a literal is an instance of, or `None` if the type
diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs
index 90bf28180de93..6aa5509780ca0 100644
--- a/crates/ty_python_semantic/src/types/call/bind.rs
+++ b/crates/ty_python_semantic/src/types/call/bind.rs
@@ -5874,10 +5874,17 @@ impl<'a, 'db> ArgumentTypeChecker<'a, 'db> {
                     return None;
                 }
 
-                let return_ty =
-                    return_ty.filter_disjoint_elements(db, self.env, tcx, self.inferable_typevars);
-                let tcx =
-                    tcx.filter_disjoint_elements(db, self.env, return_ty, self.inferable_typevars);
+                let return_ty = return_ty
+                    .discard_disjoint_union_elements(db, self.env, tcx, self.inferable_typevars)
+                    .or_never();
+                let tcx = tcx
+                    .discard_disjoint_union_elements(
+                        db,
+                        self.env,
+                        return_ty,
+                        self.inferable_typevars,
+                    )
+                    .or_never();
                 let path_bounds = return_ty.assignable_solutions_with_inferable(
                     db,
                     self.env,
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 045edb7cd6043..9d4fee4e2504f 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -3793,8 +3793,15 @@ impl<'db, 'c> SpecializationBuilder<'db, 'c> {
         //
         // For example, if `formal` is `list[T]` and `actual` is `list[int] | None`, we want to
         // specialize `T` to `int`, and so ignore the `None`.
-        let actual = actual.filter_disjoint_elements(db, self.env, formal, self.inferable);
-        let formal = formal.filter_disjoint_elements(db, self.env, actual, self.inferable);
+        //
+        // If no elements survive, keep the original union: inferring from `Never` would discard
+        // its type variables and skip the bound checks that reject the argument.
+        let actual = actual
+            .discard_disjoint_union_elements(db, self.env, formal, self.inferable)
+            .unless_all_disjoint(actual);
+        let formal = formal
+            .discard_disjoint_union_elements(db, self.env, actual, self.inferable)
+            .unless_all_disjoint(formal);
 
         // ParamSpecs and TypeVarTuples still use the forward-only legacy mapping table. Keep
         // their entire inference context on the existing signature path, and use forward
diff --git a/crates/ty_python_semantic/src/types/infer/builder.rs b/crates/ty_python_semantic/src/types/infer/builder.rs
index f61f059f3bd48..9e383c0a560d2 100644
--- a/crates/ty_python_semantic/src/types/infer/builder.rs
+++ b/crates/ty_python_semantic/src/types/infer/builder.rs
@@ -7013,12 +7013,14 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 .and_then(|class| class.generic_context(db))
                 .map(|generic_context| generic_context.inferable_typevars(db))
                 .unwrap_or(TypeVarSet::None);
-            annotation.filter_disjoint_elements(
-                db,
-                env,
-                Type::homogeneous_tuple(db, env, Type::unknown()),
-                inferable,
-            )
+            annotation
+                .discard_disjoint_union_elements(
+                    db,
+                    env,
+                    Type::homogeneous_tuple(db, env, Type::unknown()),
+                    inferable,
+                )
+                .or_never()
         });
 
         let mut is_homogeneous_tuple_annotation = false;
@@ -7463,7 +7465,9 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
         // `collection_ty` is `list`.
         let tcx = tcx.map(|annotation| {
             let collection_ty = collection_class.to_instance(db, env);
-            annotation.filter_disjoint_elements(db, env, collection_ty, inferable)
+            annotation
+                .discard_disjoint_union_elements(db, env, collection_ty, inferable)
+                .or_never()
         });
 
         // Collect type constraints from the declared element types.
diff --git a/crates/ty_python_semantic/src/types/signatures.rs b/crates/ty_python_semantic/src/types/signatures.rs
index cb8a4aec30d07..2912c175b0258 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -4707,9 +4707,12 @@ impl<'db> Parameters<'db> {
         matches!(self.data.kind, ParametersKind::Top)
     }
 
-    /// Returns whether the parameters are `(*object, **object)`, which accepts every call.
+    /// Returns whether this is the bottom parameter list, `(*args: object, **kwargs: object)`,
+    /// which accepts every call.
     pub(crate) fn is_bottom(&self) -> bool {
-        // Top parameters store the same variadics; their kind distinguishes them from bottom.
+        // `Parameters::top()` stores the same parameter list, but `ParametersKind::Top`
+        // makes it reject every call. Bottom parameters use `ParametersKind::Standard`,
+        // so check the kind before checking the parameter types.
         self.is_standard()
             && matches!(
                 self.as_slice(),

From 6bfe4715fd24dc156f318fe742f856de4082714a Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 15:58:59 +0200
Subject: [PATCH 09/11] [ty] Trim ParamSpec materialization comment

---
 crates/ty_python_semantic/src/types/relation.rs | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index c099be91a88ad..0af9be2cdc2ff 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -1757,9 +1757,6 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
 
             // Compare fixed `ParamSpec`s with the endpoints of the materialization range of `...`:
             // its bottom is below every `ParamSpec`, and its top is above every `ParamSpec`.
-            // Do not expand a fixed `ParamSpec` for ordinary parameter lists. The eager signature
-            // comparison treats `P.args` and `P.kwargs` as optional variadics, but `P` can contain
-            // required parameters, so `P` is not necessarily compatible with an empty list.
             (Type::TypeVar(bound_typevar), Type::Callable(other))
             | (Type::Callable(other), Type::TypeVar(bound_typevar))
                 if !bound_typevar.is_inferable(db, self.inferable)

From 98e7ae3a8fbec12e0497e437071b7bc2d6dcccd5 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 17:44:23 +0200
Subject: [PATCH 10/11] [ty] Refine ParamSpec and materialization regression
 tests

---
 .../mdtest/generics/legacy/paramspec.md       | 21 +++++++++++++++++++
 .../mdtest/type_properties/materialization.md | 10 +++------
 2 files changed, 24 insertions(+), 7 deletions(-)

diff --git a/crates/ty_python_semantic/resources/mdtest/generics/legacy/paramspec.md b/crates/ty_python_semantic/resources/mdtest/generics/legacy/paramspec.md
index 846429959c122..2b11d378a22ad 100644
--- a/crates/ty_python_semantic/resources/mdtest/generics/legacy/paramspec.md
+++ b/crates/ty_python_semantic/resources/mdtest/generics/legacy/paramspec.md
@@ -746,6 +746,27 @@ takes_int_job(defaulted_job)
 takes_int_job(wrong_job)  # error: [invalid-argument-type]
 ```
 
+A fixed `ParamSpec` can contain required parameters. A wrapper around such a callback cannot be used
+as a wrapper around a callback that accepts no arguments.
+
+```py
+def erase_parameters(job: Job[P]) -> Job[[]]:
+    return job  # error: [invalid-return-type]
+```
+
+The same restriction applies in the other direction when a class consumes callbacks. A consumer of
+callbacks with no parameters cannot accept a callback with arbitrary required parameters.
+
+```py
+P_co = ParamSpec("P_co", covariant=True)
+
+class CallbackConsumer(Generic[P_co]):
+    def consume(self, callback: Callable[P_co, None]) -> None: ...
+
+def broaden_parameters(consumer: CallbackConsumer[[]]) -> CallbackConsumer[P_co]:
+    return consumer  # error: [invalid-return-type]
+```
+
 ## Inferring an invariant `ParamSpec` through `Concatenate`
 
 A `Concatenate` prefix is positional-only, so a callback whose first parameter also accepts a
diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index 2be3257fd1e3d..a6a01b5ab0035 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
+++ b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
@@ -1500,21 +1500,17 @@ static_assert(not is_subtype_of(Bottom[list[int | Any]], Bottom[list[Any]]))
 ```
 
 An unresolved type variable does not necessarily satisfy a materialization's bounds. Conversely,
-`Top[list[Unknown]]` includes specializations that do not match an arbitrary fixed `T`, as in
-[ty#4201](https://github.com/astral-sh/ty/issues/4201). Neither comparison below holds for every
-`T`, and the union retains both alternatives.
+`Top[list[Unknown]]` includes specializations that do not match an arbitrary fixed `T`.
 
 ```pyi
 from ty_extensions._internal import Unknown
 
-def unresolved[T](values: list[T] | Top[list[int & Any]]):
+def unresolved[T]():
     static_assert(not is_subtype_of(list[T], Top[list[int & Any]]))
     static_assert(not is_subtype_of(Top[list[Unknown]], list[T]))
-    reveal_type(values)  # revealed: list[T@unresolved] | Top[list[int & Any]]
 ```
 
-A declared upper bound can establish the required relation without fixing the type variable to one
-particular specialization.
+A declared upper bound on `T` can make this relation true:
 
 ```pyi
 def bounded[T: int]():

From 88059dd2de2b7b99a5b86cf3961677095ffa6a94 Mon Sep 17 00:00:00 2001
From: David Peter <mail@david-peter.de>
Date: Fri, 28 Aug 2026 17:57:47 +0200
Subject: [PATCH 11/11] [ty] Clarify and relocate constraint satisfiability
 helper

---
 .../src/types/constraints.rs                  | 35 ++++++++++++++++++-
 .../src/types/constraints/projection.rs       | 29 ---------------
 .../ty_python_semantic/src/types/generics.rs  |  3 --
 3 files changed, 34 insertions(+), 33 deletions(-)

diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index c2ea866ef0a1d..280f1addcd7ff 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -509,7 +509,7 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
         debug_assert!(std::ptr::eq(self.builder, builder));
     }
 
-    /// Returns whether this constraint set never holds, without applying the type variables'
+    /// Returns whether this constraint set never holds, without checking the type variables'
     /// declared bounds or constraints. Use [`Self::has_no_valid_solutions`] to include those.
     pub(crate) fn is_never_satisfied(self, db: &'db dyn Db, env: &ProgramEnvironment<'db>) -> bool {
         let mut storage = self.builder.storage.borrow_mut();
@@ -517,6 +517,39 @@ impl<'db, 'c> ConstraintSet<'db, 'c> {
             .is_never_satisfied(db, env, &mut storage, self.source_order)
     }
 
+    /// Returns whether no specialization satisfying the type variables' upper bounds and
+    /// constraints can satisfy this constraint set.
+    ///
+    /// Unlike [`Self::is_never_satisfied`], this validates solutions against the type variables'
+    /// upper bounds and constraints. For example, `T = int` is not contradictory by itself, but has
+    /// no valid solution if `T` has an upper bound of `str`.
+    ///
+    /// If the solver reaches its computation limit, we do not know whether a valid solution exists.
+    /// This returns `false` in that case: stopping the search is not proof that there is no solution.
+    pub(crate) fn has_no_valid_solutions(
+        self,
+        db: &'db dyn Db,
+        env: &ProgramEnvironment<'db>,
+    ) -> bool {
+        if self.is_never_satisfied(db, env) {
+            return true;
+        }
+
+        let inferable = {
+            let storage = self.builder.storage.borrow();
+            let Some(support) = storage.node_support(self.node) else {
+                return false;
+            };
+            // For overlap, every mentioned type variable can choose a valid specialization.
+            TypeVarSet::from_typevars(db, support.iter().map(|id| storage.typevar_data(id)))
+        };
+
+        matches!(
+            self.solutions(db, env, inferable),
+            Ok(Solutions::Unsatisfiable)
+        )
+    }
+
     /// Returns whether this constraint set is the `never` terminal.
     ///
     /// A nonterminal constraint set can also never be satisfied, so `false` does not prove that
diff --git a/crates/ty_python_semantic/src/types/constraints/projection.rs b/crates/ty_python_semantic/src/types/constraints/projection.rs
index de787090f86eb..86ad764a68072 100644
--- a/crates/ty_python_semantic/src/types/constraints/projection.rs
+++ b/crates/ty_python_semantic/src/types/constraints/projection.rs
@@ -108,35 +108,6 @@ impl ProjectionTypeBudget {
 }
 
 impl<'db> ConstraintSet<'db, '_> {
-    /// Returns whether no specialization satisfying the type variables' declared bounds and
-    /// constraints can satisfy this constraint set.
-    ///
-    /// Unlike [`Self::is_never_satisfied`], this validates the solutions against their declarations.
-    /// Exhausting the solution budget does not prove that the set is unsatisfiable.
-    pub(crate) fn has_no_valid_solutions(
-        self,
-        db: &'db dyn Db,
-        env: &ProgramEnvironment<'db>,
-    ) -> bool {
-        if self.is_never_satisfied(db, env) {
-            return true;
-        }
-
-        let inferable = {
-            let storage = self.builder.storage.borrow();
-            let Some(support) = storage.node_support(self.node) else {
-                return false;
-            };
-            // For overlap, every mentioned type variable can choose a valid specialization.
-            TypeVarSet::from_typevars(db, support.iter().map(|id| storage.typevar_data(id)))
-        };
-
-        matches!(
-            self.solutions(db, env, inferable),
-            Ok(Solutions::Unsatisfiable)
-        )
-    }
-
     /// Computes default solutions for each BDD path within the default projection budget.
     pub(crate) fn solutions(
         self,
diff --git a/crates/ty_python_semantic/src/types/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 9d4fee4e2504f..111887f82322b 100644
--- a/crates/ty_python_semantic/src/types/generics.rs
+++ b/crates/ty_python_semantic/src/types/generics.rs
@@ -2078,9 +2078,6 @@ impl<'c, 'db> TypeRelationChecker<'_, 'c, 'db> {
             self.materialization_visitor,
         );
 
-        // Lazy comparisons record the bounds imposed by each materialization. Eager comparisons
-        // must also respect type variables: treating them as unconditional matches can discard
-        // valid alternatives from unions such as `list[T] | Top[list[Any & int]]`.
         let is_subtype_of = |source, target| self.check_type_pair(db, source, target);
         match (source_materialization, target_materialization) {
             // `source` is a subtype of `target` if the range of materializations covered by `source`