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/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 4d9ccf1d0719d..ef13cdb1b9552 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/isinstance.md
@@ -1453,8 +1453,9 @@ Narrowing must therefore preserve the original type argument instead of substitu
 default.
 
 ```py
-from typing import assert_never
+from typing import assert_never, final
 
+@final
 class Box[T: str = str]:
     value: T
 
@@ -1466,7 +1467,7 @@ def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
         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 e075ea939175b..a4b1afed22ab7 100644
--- a/crates/ty_python_semantic/resources/mdtest/narrow/match.md
+++ b/crates/ty_python_semantic/resources/mdtest/narrow/match.md
@@ -189,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,7 +203,7 @@ def box_with_default[T: str = str](value: Box[T] | T) -> Box[T]:
             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/resources/mdtest/type_properties/is_disjoint_from.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_disjoint_from.md
index 360d525b9fbfc..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
@@ -1186,6 +1186,63 @@ 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 typing import Never
+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]]))
+    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
+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 `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]]))
+```
+
 ### 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/resources/mdtest/type_properties/materialization.md b/crates/ty_python_semantic/resources/mdtest/type_properties/materialization.md
index 9de848e9f478e..a6a01b5ab0035 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]():
+    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.
@@ -1391,6 +1422,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.
 
@@ -1463,6 +1499,24 @@ 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. Conversely,
+`Top[list[Unknown]]` includes specializations that do not match an arbitrary fixed `T`.
+
+```pyi
+from ty_extensions._internal import Unknown
+
+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]))
+```
+
+A declared upper bound on `T` can make this relation true:
+
+```pyi
+def bounded[T: int]():
+    static_assert(is_subtype_of(list[T], Top[list[int & Any]]))
+```
+
 ## Assignability
 
 ### General
diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs
index fa4895159fbe2..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,20 +2903,27 @@ impl<'db> Type<'db> {
 
     /// If the type is a union, removes union elements that are disjoint from `target`.
     ///
-    /// Otherwise, returns the type unchanged.
-    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();
-        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.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/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index 0c394fbfa9f9f..280f1addcd7ff 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -509,13 +509,47 @@ 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 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();
         self.node
             .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/generics.rs b/crates/ty_python_semantic/src/types/generics.rs
index 2ee5fa20f054c..111887f82322b 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,7 @@ 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)
-        };
+        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`.
@@ -2199,15 +2173,23 @@ impl<'c, 'db> DisjointnessChecker<'_, 'c, 'db> {
                     // `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 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(
+                        db,
+                        left_type,
+                        MaterializationKind::Bottom,
+                        right_type,
+                        MaterializationKind::Top,
+                    );
+                    ConstraintSet::from_bool(
+                        self.constraints,
+                        overlap.has_no_valid_solutions(db, self.env),
+                    )
                 }
 
                 // If `Foo[T]` is covariant in `T`, `Foo[Never]` is a subtype of `Foo[A]` and `Foo[B]`
@@ -3808,8 +3790,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/relation.rs b/crates/ty_python_semantic/src/types/relation.rs
index c1653d9187b57..0af9be2cdc2ff 100644
--- a/crates/ty_python_semantic/src/types/relation.rs
+++ b/crates/ty_python_semantic/src/types/relation.rs
@@ -1755,14 +1755,19 @@ 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 with the endpoints 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
+                    && other.signatures(db).iter().all(|signature| {
+                        signature.parameters().is_top() || signature.parameters().is_bottom()
+                    }) =>
             {
-                self.always()
+                let other_is_top = Self::is_top_paramspec_value(db, other);
+                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 f1bfb0ab95183..2912c175b0258 100644
--- a/crates/ty_python_semantic/src/types/signatures.rs
+++ b/crates/ty_python_semantic/src/types/signatures.rs
@@ -4707,6 +4707,23 @@ impl<'db> Parameters<'db> {
         matches!(self.data.kind, ParametersKind::Top)
     }
 
+    /// Returns whether this is the bottom parameter list, `(*args: object, **kwargs: object)`,
+    /// which accepts every call.
+    pub(crate) fn is_bottom(&self) -> bool {
+        // `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(),
+                [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 {