[ty] Reject fixed tuples for non-inferable TypeVarTuples

crates/ty_python_semantic/resources/mdtest/generics/pep695/typevartuple.md

@@ -362,6 +362,32 @@ class Outer[*Ts]:
         return values  # error: [invalid-return-type]
 ```
 
+A fixed-length tuple cannot replace an arbitrary type variable tuple either. The caller determines
+the pack's length and element types, so even an empty tuple is not a valid return for every pack.
+The same restriction applies to annotated assignments inside the function.
+
+```py
+def reject_empty[*Ts](values: tuple[*Ts]) -> tuple[*Ts]:
+    return ()  # error: [invalid-return-type]
+
+def reject_fixed[*Ts](values: tuple[*Ts]) -> tuple[*Ts]:
+    return (1, "a")  # error: [invalid-return-type]
+
+def reject_fixed_assignment[*Ts]() -> None:
+    fixed: tuple[*Ts] = (1,)  # error: [invalid-assignment]
+```
+
+Matching fixed elements before or after a pack do not establish what the pack contains. The
+remaining elements still cannot replace an arbitrary type variable tuple.
+
+```py
+def reject_empty_middle[*Ts](values: tuple[*Ts]) -> tuple[int, *Ts, str]:
+    return (1, "a")  # error: [invalid-return-type]
+
+def reject_fixed_middle[*Ts](values: tuple[*Ts]) -> tuple[int, *Ts, str]:
+    return (1, True, "a")  # error: [invalid-return-type]
+```
+
 Materializing a type variable tuple can change its default without changing the identity of the
 bound type variable occurrence.
 
@@ -379,6 +405,20 @@ def materialized_default[*Ts = *tuple[Any, ...]]() -> None:
     static_assert(is_assignable_to(tuple[*Ts], Top[tuple[*Ts]]))
 ```
 
+Fixed-length tuples are not subtypes of an arbitrary pack either. An `Any` or `Never` element does
+not change a fixed tuple's length.
+
+```py
+from typing import Never
+from ty_extensions._internal import is_subtype_of
+
+def fixed_tuple_relations[*Ts]() -> None:
+    static_assert(not is_subtype_of(tuple[()], tuple[*Ts]))
+    static_assert(not is_subtype_of(tuple[int], tuple[*Ts]))
+    static_assert(not is_assignable_to(tuple[Any], tuple[*Ts]))
+    static_assert(not is_assignable_to(tuple[Never], tuple[*Ts]))
+```
+
 ### Starred variadic parameters
 
 An unpacked `TypeVarTuple` can annotate `*args`. Call binding infers the pack from direct arguments

crates/ty_python_semantic/resources/mdtest/narrow/len.md

@@ -250,6 +250,73 @@ def _(value: TrueLength | FalseLength):
         reveal_type(value)  # revealed: FalseLength
 ```
 
+Length narrowing preserves a tuple's shape when a required element has type `Never`:
+
+```py
+from typing import Never
+
+def _(value: tuple[Never, *tuple[int, ...]]) -> None:
+    if len(value) == 1:
+        reveal_type(value)  # revealed: tuple[Never]
+```
+
+## Exact length comparisons with type variable tuples
+
+Narrowing a tuple's length preserves its type variable tuple, so a function can still return its
+input after checking for an empty or nonempty tuple.
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+def identity[*Ts](value: tuple[*Ts]) -> tuple[*Ts]:
+    if len(value) == 0:
+        reveal_type(value)  # revealed: tuple[*Ts@identity] & tuple[()]
+        return value
+    elif len(value) == 1:
+        reveal_type(value)  # revealed: tuple[*Ts@identity] & tuple[object]
+        return value
+    return value
+```
+
+Fixed prefix and suffix elements retain their types while the original pack is preserved.
+
+```py
+def with_boundaries[*Ts](value: tuple[int, *Ts, str]) -> tuple[int, *Ts, str]:
+    if len(value) == 2:
+        reveal_type(value)  # revealed: tuple[int, *Ts@with_boundaries, str] & tuple[int, str]
+        return value
+    return value
+```
+
+An alias for the tuple preserves the same pack identity when its length is narrowed.
+
+```py
+type Pack[*Ts] = tuple[*Ts]
+
+def aliased_identity[*Ts](value: Pack[*Ts]) -> Pack[*Ts]:
+    if len(value) == 1:
+        reveal_type(value)  # revealed: tuple[*Ts@aliased_identity] & tuple[object]
+        return value
+    return value
+```
+
+With a required `Never` element, the refined type should be `tuple[Never, *Ts] & tuple[Never]`.
+TODO: [#27920](https://github.com/astral-sh/ruff/pull/27920) addresses the tuple-disjointness checks
+that currently collapse this to `Never` and suppress the invalid-return diagnostic.
+
+```py
+from typing import Never
+
+def never_prefix[*Ts](value: tuple[Never, *Ts]) -> str:
+    if len(value) == 1:
+        reveal_type(value)  # revealed: Never
+        return value
+    return ""
+```
+
 ## Regression tests
 
 Length constraints must not become stale after mutating a value that does not encode its length:

crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md

@@ -246,9 +246,25 @@ def mutually_constrained[U, T]():
     static_assert(not given_int.implies_subtype_of(T, str))
 ```
 
+## Type variable tuples
+
+A concrete tuple is not a subtype of an arbitrary type variable tuple. A constraint relating the two
+can establish that relationship without admitting incompatible tuple elements.
+
+```py
+from ty_extensions import static_assert
+from ty_extensions._internal import ConstraintSet, is_constraint_set_assignable_to
+
+def tuple_assumptions[*Ts]() -> None:
+    given = is_constraint_set_assignable_to(tuple[int], tuple[*Ts])
+    static_assert(given.implies_subtype_of(tuple[int], tuple[*Ts]))
+    static_assert(not given.implies_subtype_of(tuple[str], tuple[*Ts]))
+    static_assert(not ConstraintSet.always().implies_subtype_of(tuple[int], tuple[*Ts]))
+```
+
 ## Compound types
 
-All of the relationships in the above section also apply when a typevar appears in a compound type.
+The relationships for [type variables](#type-variables) also apply within compound types.
 
 ```py
 from ty_extensions import static_assert

crates/ty_python_semantic/src/types/narrow.rs

@@ -3404,7 +3404,18 @@ impl<'db> NarrowingConstraintsBuilder<'db, '_> {
             _ => {
                 if is_equality && let Some(tuple) = resolved.exact_tuple_instance_spec(db) {
                     match tuple.resize(db, env, TupleLength::Fixed(length)) {
-                        Ok(tuple) => Type::tuple(TupleType::new(db, env, &tuple)),
+                        Ok(resized) => {
+                            let narrowed = Type::tuple(TupleType::new(db, env, &resized));
+                            if let TupleSpec::Variable(variable) = tuple.as_ref()
+                                && variable.variable().typevartuple().is_some()
+                            {
+                                // Resizing forgets which TypeVarTuple these elements came from.
+                                // Retain that identity alongside the observed length and elements.
+                                IntersectionType::from_two_elements(db, env, resolved, narrowed)
+                            } else {
+                                narrowed
+                            }
+                        }
                         Err(_) => Type::Never,
                     }
                 } else {

crates/ty_python_semantic/src/types/relation.rs

@@ -1717,10 +1717,15 @@ impl<'a, 'c, 'db> TypeRelationChecker<'a, 'c, 'db> {
                     target,
                 )
             }
+            // A fixed tuple cannot satisfy every specialization of a non-inferable TypeVarTuple.
+            // Let it reach the ordinary rejection below; expanding the target would repeat the
+            // same tuple comparison and cause the recursion guard to accept it.
             (source, Type::TypeVar(bound_typevar))
                 if !bound_typevar.is_inferable(db, self.inferable)
                     && bound_typevar.is_typevartuple(db)
-                    && source.exact_tuple_instance_spec(db).is_some() =>
+                    && source
+                        .exact_tuple_instance_spec(db)
+                        .is_some_and(|spec| spec.is_variadic()) =>
             {
                 self.check_type_pair(
                     db,