[ty] Respect type variables in top/bottom materializations of invariant generics

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

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 -->

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)

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)
 ```
 

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

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

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

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,

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