[ty] Homogeneous and mixed tuples (#18600)

We already had support for homogeneous tuples (`tuple[int, ...]`). This
PR extends this to also support mixed tuples (`tuple[str, str,
*tuple[int, ...], str str]`).

A mixed tuple consists of a fixed-length (possibly empty) prefix and
suffix, and a variable-length portion in the middle. Every element of
the variable-length portion must be of the same type. A homogeneous
tuple is then just a mixed tuple with an empty prefix and suffix.

The new data representation uses different Rust types for a fixed-length
(aka heterogeneous) tuple. Another option would have been to use the
`VariableLengthTuple` representation for all tuples, and to wrap the
"variable + suffix" portion in an `Option`. I don't think that would
simplify the method implementations much, though, since we would still
have a 2×2 case analysis for most of them.

One wrinkle is that the definition of the `tuple` class in the typeshed
has a single typevar, and canonically represents a homogeneous tuple.
When getting the class of a tuple instance, that means that we have to
summarize our detailed mixed tuple type information into its
"homogeneous supertype". (We were already doing this for heterogeneous
types.)

A similar thing happens when concatenating two mixed tuples: the
variable-length portion and suffix of the LHS, and the prefix and
variable-length portion of the RHS, all get unioned into the
variable-length portion of the result. The LHS prefix and RHS suffix
carry through unchanged.

---------

Co-authored-by: Alex Waygood <Alex.Waygood@Gmail.com>

crates/ty_python_semantic/resources/mdtest/assignment/annotations.md

@@ -58,7 +58,7 @@ reveal_type(c)  # revealed: tuple[str, int]
 reveal_type(d)  # revealed: tuple[tuple[str, str], tuple[int, int]]
 reveal_type(e)  # revealed: tuple[str, ...]
 
-reveal_type(f)  # revealed: @Todo(PEP 646)
+reveal_type(f)  # revealed: tuple[str, *tuple[int, ...], bytes]
 reveal_type(g)  # revealed: @Todo(PEP 646)
 
 reveal_type(h)  # revealed: tuple[list[int], list[int]]

crates/ty_python_semantic/resources/mdtest/attributes.md

@@ -1722,7 +1722,7 @@ d = True
 reveal_type(d.__class__)  # revealed: <class 'bool'>
 
 e = (42, 42)
-reveal_type(e.__class__)  # revealed: <class 'tuple'>
+reveal_type(e.__class__)  # revealed: <class 'tuple[Literal[42], Literal[42]]'>
 
 def f(a: int, b: typing_extensions.LiteralString, c: int | str, d: type[str]):
     reveal_type(a.__class__)  # revealed: type[int]

crates/ty_python_semantic/resources/mdtest/binary/tuples.md

@@ -17,6 +17,32 @@ def _(x: tuple[int, str], y: tuple[None, tuple[int]]):
 
 ```py
 def _(x: tuple[int, ...], y: tuple[str, ...]):
+    reveal_type(x + x)  # revealed: tuple[int, ...]
     reveal_type(x + y)  # revealed: tuple[int | str, ...]
-    reveal_type(x + (1, 2))  # revealed: tuple[int, ...]
+    reveal_type((1, 2) + x)  # revealed: tuple[Literal[1], Literal[2], *tuple[int, ...]]
+    reveal_type(x + (3, 4))  # revealed: tuple[*tuple[int, ...], Literal[3], Literal[4]]
+    reveal_type((1, 2) + x + (3, 4))  # revealed: tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[3], Literal[4]]
+    reveal_type((1, 2) + y + (3, 4) + x)  # revealed: tuple[Literal[1], Literal[2], *tuple[int | str, ...]]
+```
+
+We get the same results even when we use a legacy type alias, even though this involves first
+inferring the `tuple[...]` expression as a value form. (Doing so gives a generic alias of the
+`tuple` type, but as a special case, we include the full detailed tuple element specification in
+specializations of `tuple`.)
+
+```py
+from typing import Literal
+
+OneTwo = tuple[Literal[1], Literal[2]]
+ThreeFour = tuple[Literal[3], Literal[4]]
+IntTuple = tuple[int, ...]
+StrTuple = tuple[str, ...]
+
+def _(one_two: OneTwo, x: IntTuple, y: StrTuple, three_four: ThreeFour):
+    reveal_type(x + x)  # revealed: tuple[int, ...]
+    reveal_type(x + y)  # revealed: tuple[int | str, ...]
+    reveal_type(one_two + x)  # revealed: tuple[Literal[1], Literal[2], *tuple[int, ...]]
+    reveal_type(x + three_four)  # revealed: tuple[*tuple[int, ...], Literal[3], Literal[4]]
+    reveal_type(one_two + x + three_four)  # revealed: tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[3], Literal[4]]
+    reveal_type(one_two + y + three_four + x)  # revealed: tuple[Literal[1], Literal[2], *tuple[int | str, ...]]
 ```

crates/ty_python_semantic/resources/mdtest/generics/legacy/functions.md

@@ -130,6 +130,44 @@ reveal_type(takes_in_protocol(ExplicitSub()))  # revealed: int
 reveal_type(takes_in_protocol(ExplicitGenericSub[str]()))  # revealed: str
 ```
 
+## Inferring tuple parameter types
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from typing import TypeVar
+
+T = TypeVar("T")
+
+def takes_mixed_tuple_suffix(x: tuple[int, bytes, *tuple[str, ...], T, int]) -> T:
+    return x[-2]
+
+# TODO: revealed: Literal[True]
+reveal_type(takes_mixed_tuple_suffix((1, b"foo", "bar", "baz", True, 42)))  # revealed: Unknown
+
+def takes_mixed_tuple_prefix(x: tuple[int, T, *tuple[str, ...], bool, int]) -> T:
+    return x[1]
+
+# TODO: revealed: Literal[b"foo"]
+reveal_type(takes_mixed_tuple_prefix((1, b"foo", "bar", "baz", True, 42)))  # revealed: Unknown
+
+def takes_fixed_tuple(x: tuple[T, int]) -> T:
+    return x[0]
+
+reveal_type(takes_fixed_tuple((True, 42)))  # revealed: Literal[True]
+
+def takes_homogeneous_tuple(x: tuple[T, ...]) -> T:
+    return x[0]
+
+# TODO: revealed: Literal[42]
+reveal_type(takes_homogeneous_tuple((42,)))  # revealed: Unknown
+# TODO: revealed: Literal[42, 43]
+reveal_type(takes_homogeneous_tuple((42, 43)))  # revealed: Unknown
+```
+
 ## Inferring a bound typevar
 
 <!-- snapshot-diagnostics -->

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

@@ -125,6 +125,35 @@ reveal_type(takes_in_protocol(ExplicitSub()))  # revealed: int
 reveal_type(takes_in_protocol(ExplicitGenericSub[str]()))  # revealed: str
 ```
 
+## Inferring tuple parameter types
+
+```py
+def takes_mixed_tuple_suffix[T](x: tuple[int, bytes, *tuple[str, ...], T, int]) -> T:
+    return x[-2]
+
+# TODO: revealed: Literal[True]
+reveal_type(takes_mixed_tuple_suffix((1, b"foo", "bar", "baz", True, 42)))  # revealed: Unknown
+
+def takes_mixed_tuple_prefix[T](x: tuple[int, T, *tuple[str, ...], bool, int]) -> T:
+    return x[1]
+
+# TODO: revealed: Literal[b"foo"]
+reveal_type(takes_mixed_tuple_prefix((1, b"foo", "bar", "baz", True, 42)))  # revealed: Unknown
+
+def takes_fixed_tuple[T](x: tuple[T, int]) -> T:
+    return x[0]
+
+reveal_type(takes_fixed_tuple((True, 42)))  # revealed: Literal[True]
+
+def takes_homogeneous_tuple[T](x: tuple[T, ...]) -> T:
+    return x[0]
+
+# TODO: revealed: Literal[42]
+reveal_type(takes_homogeneous_tuple((42,)))  # revealed: Unknown
+# TODO: revealed: Literal[42, 43]
+reveal_type(takes_homogeneous_tuple((42, 43)))  # revealed: Unknown
+```
+
 ## Inferring a bound typevar
 
 <!-- snapshot-diagnostics -->

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

@@ -192,10 +192,9 @@ def _(t1: tuple[int | None, int | None], t2: tuple[int, int] | tuple[None, None]
         reveal_type(t1[1])  # revealed: int | None
 
     if t2[0] is not None:
+        reveal_type(t2[0])  # revealed: int
         # TODO: should be int
-        reveal_type(t2[0])  # revealed: Unknown & ~None
-        # TODO: should be int
-        reveal_type(t2[1])  # revealed: Unknown
+        reveal_type(t2[1])  # revealed: int | None
 ```
 
 ### String subscript

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

@@ -215,12 +215,12 @@ def _(a: tuple[str, int] | tuple[int, str], c: C[Any]):
         # TODO: Should be `tuple[int, str]`
         reveal_type(a)  # revealed: tuple[str, int] | tuple[int, str]
         # TODO: Should be `str`
-        reveal_type(a[1])  # revealed: Unknown
+        reveal_type(a[1])  # revealed: str | int
 
     if reveal_type(is_int(a[0])):  # revealed: TypeIs[int @ a[0]]
         # TODO: Should be `tuple[int, str]`
         reveal_type(a)  # revealed: tuple[str, int] | tuple[int, str]
-        reveal_type(a[0])  # revealed: Unknown & int
+        reveal_type(a[0])  # revealed: int
 
     # TODO: Should be `TypeGuard[str @ c.v]`
     if reveal_type(guard_str(c.v)):  # revealed: @Todo(`TypeGuard[]` special form)

crates/ty_python_semantic/resources/mdtest/subscript/tuple.md

@@ -69,8 +69,64 @@ def _(m: int, n: int):
     t[::0]  # error: [zero-stepsize-in-slice]
 
     tuple_slice = t[m:n]
-    # TODO: Should be `tuple[Literal[1, 'a', b"b"] | None, ...]`
-    reveal_type(tuple_slice)  # revealed: tuple[Unknown, ...]
+    reveal_type(tuple_slice)  # revealed: tuple[Literal[1, "a", b"b"] | None, ...]
+```
+
+## Slices of homogeneous and mixed tuples
+
+```toml
+[environment]
+python-version = "3.11"
+```
+
+```py
+from typing import Literal
+
+def homogeneous(t: tuple[str, ...]) -> None:
+    reveal_type(t[0])  # revealed: str
+    reveal_type(t[1])  # revealed: str
+    reveal_type(t[2])  # revealed: str
+    reveal_type(t[3])  # revealed: str
+
+    reveal_type(t[-1])  # revealed: str
+    reveal_type(t[-2])  # revealed: str
+    reveal_type(t[-3])  # revealed: str
+    reveal_type(t[-4])  # revealed: str
+
+def mixed(s: tuple[str, ...]) -> None:
+    t = (1, 2, 3) + s + (8, 9, 10)
+
+    reveal_type(t[0])  # revealed: Literal[1]
+    reveal_type(t[1])  # revealed: Literal[2]
+    reveal_type(t[2])  # revealed: Literal[3]
+    reveal_type(t[3])  # revealed: str | Literal[8]
+    reveal_type(t[4])  # revealed: str | Literal[8, 9]
+    reveal_type(t[5])  # revealed: str | Literal[8, 9, 10]
+
+    reveal_type(t[-1])  # revealed: Literal[10]
+    reveal_type(t[-2])  # revealed: Literal[9]
+    reveal_type(t[-3])  # revealed: Literal[8]
+    reveal_type(t[-4])  # revealed: Literal[3] | str
+    reveal_type(t[-5])  # revealed: Literal[2, 3] | str
+    reveal_type(t[-6])  # revealed: Literal[1, 2, 3] | str
+```
+
+## `tuple` as generic alias
+
+For tuple instances, we can track more detailed information about the length and element types of
+the tuple. This information carries over to the generic alias that the tuple is an instance of.
+
+```py
+def _(a: tuple, b: tuple[int], c: tuple[int, str], d: tuple[int, ...]) -> None:
+    reveal_type(a)  # revealed: tuple[Unknown, ...]
+    reveal_type(b)  # revealed: tuple[int]
+    reveal_type(c)  # revealed: tuple[int, str]
+    reveal_type(d)  # revealed: tuple[int, ...]
+
+reveal_type(tuple)  # revealed: <class 'tuple'>
+reveal_type(tuple[int])  # revealed: <class 'tuple[int]'>
+reveal_type(tuple[int, str])  # revealed: <class 'tuple[int, str]'>
+reveal_type(tuple[int, ...])  # revealed: <class 'tuple[int, ...]'>
 ```
 
 ## Inheritance
@@ -83,8 +139,13 @@ python-version = "3.9"
 ```py
 class A(tuple[int, str]): ...
 
-# revealed: tuple[<class 'A'>, <class 'tuple[@Todo(Generic tuple specializations), ...]'>, <class 'Sequence[@Todo(Generic tuple specializations)]'>, <class 'Reversible[@Todo(Generic tuple specializations)]'>, <class 'Collection[@Todo(Generic tuple specializations)]'>, <class 'Iterable[@Todo(Generic tuple specializations)]'>, <class 'Container[@Todo(Generic tuple specializations)]'>, typing.Protocol, typing.Generic, <class 'object'>]
+# revealed: tuple[<class 'A'>, <class 'tuple[int, str]'>, <class 'Sequence[int | str]'>, <class 'Reversible[int | str]'>, <class 'Collection[int | str]'>, <class 'Iterable[int | str]'>, <class 'Container[int | str]'>, typing.Protocol, typing.Generic, <class 'object'>]
 reveal_type(A.__mro__)
+
+class C(tuple): ...
+
+# revealed: tuple[<class 'C'>, <class 'tuple[Unknown, ...]'>, <class 'Sequence[Unknown]'>, <class 'Reversible[Unknown]'>, <class 'Collection[Unknown]'>, <class 'Iterable[Unknown]'>, <class 'Container[Unknown]'>, typing.Protocol, typing.Generic, <class 'object'>]
+reveal_type(C.__mro__)
 ```
 
 ## `typing.Tuple`
@@ -109,9 +170,19 @@ def _(c: Tuple, d: Tuple[int, A], e: Tuple[Any, ...]):
 Inheriting from `Tuple` results in a MRO with `builtins.tuple` and `typing.Generic`. `Tuple` itself
 is not a class.
 
+```toml
+[environment]
+python-version = "3.9"
+```
+
 ```py
 from typing import Tuple
 
+class A(Tuple[int, str]): ...
+
+# revealed: tuple[<class 'A'>, <class 'tuple[int, str]'>, <class 'Sequence[int | str]'>, <class 'Reversible[int | str]'>, <class 'Collection[int | str]'>, <class 'Iterable[int | str]'>, <class 'Container[int | str]'>, typing.Protocol, typing.Generic, <class 'object'>]
+reveal_type(A.__mro__)
+
 class C(Tuple): ...
 
 # revealed: tuple[<class 'C'>, <class 'tuple[Unknown, ...]'>, <class 'Sequence[Unknown]'>, <class 'Reversible[Unknown]'>, <class 'Collection[Unknown]'>, <class 'Iterable[Unknown]'>, <class 'Container[Unknown]'>, typing.Protocol, typing.Generic, <class 'object'>]

crates/ty_python_semantic/resources/mdtest/type_compendium/tuple.md

@@ -16,6 +16,28 @@ def _(p: P, q: Q):
     assert_type((p, q), tuple[P, Q])
 ```
 
+## Instantiating tuples
+
+Like all classes, tuples can be instantiated by invoking the `tuple` class. When instantiating a
+specialization of `tuple` we (TODO: should) check that the values passed in match the element types
+defined in the specialization.
+
+```py
+# TODO: revealed: tuple[()]
+reveal_type(tuple())  # revealed: tuple[Unknown, ...]
+# TODO: revealed: tuple[Literal[1]]
+reveal_type(tuple([1]))  # revealed: tuple[Unknown, ...]
+reveal_type(tuple[int]([1]))  # revealed: tuple[int]
+# TODO: error for invalid arguments
+reveal_type(tuple[int, str]([1]))  # revealed: tuple[int, str]
+
+reveal_type(().__class__())  # revealed: tuple[()]
+# TODO: error for invalid arguments
+reveal_type((1,).__class__())  # revealed: tuple[Literal[1]]
+# TODO: error for invalid arguments
+reveal_type((1, 2).__class__())  # revealed: tuple[Literal[1], Literal[2]]
+```
+
 ## Subtyping relationships
 
 The type `tuple[S1, S2]` is a subtype of `tuple[T1, T2]` if and only if `S1` is a subtype of `T1`
@@ -60,10 +82,7 @@ class AnotherEmptyTuple(tuple[()]): ...
 
 static_assert(not is_equivalent_to(AnotherEmptyTuple, tuple[()]))
 
-# TODO: These should not be errors
-# error: [static-assert-error]
 static_assert(is_subtype_of(AnotherEmptyTuple, tuple[()]))
-# error: [static-assert-error]
 static_assert(is_assignable_to(AnotherEmptyTuple, tuple[()]))
 ```
 
@@ -158,8 +177,6 @@ class NotAlwaysTruthyTuple(tuple[int]):
     def __bool__(self) -> bool:
         return False
 
-# TODO: This assignment should be allowed
-# error: [invalid-assignment]
 t: tuple[int] = NotAlwaysTruthyTuple((1,))
 ```
 

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

@@ -303,6 +303,11 @@ static_assert(not is_assignable_to(tuple[Any, Literal[2]], tuple[int, str]))
 
 ## Assignability of heterogeneous tuple types to homogeneous tuple types
 
+```toml
+[environment]
+python-version = "3.12"
+```
+
 While a homogeneous tuple type is not assignable to any heterogeneous tuple types, a heterogeneous
 tuple type can be assignable to a homogeneous tuple type, and homogeneous tuple types can be
 assignable to `Sequence`:
@@ -312,6 +317,11 @@ from typing import Literal, Any, Sequence
 from ty_extensions import static_assert, is_assignable_to, Not, AlwaysFalsy
 
 static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[Literal[1, 2], ...]))
+static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[Literal[1], *tuple[Literal[2], ...]]))
+static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[*tuple[Literal[1], ...], Literal[2]]))
+static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[Literal[1], *tuple[str, ...], Literal[2]]))
+static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[Literal[1], Literal[2], *tuple[str, ...]]))
+static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[*tuple[str, ...], Literal[1], Literal[2]]))
 static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[int, ...]))
 static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[int | str, ...]))
 static_assert(is_assignable_to(tuple[Literal[1], Literal[2]], tuple[Any, ...]))
@@ -330,6 +340,218 @@ static_assert(is_assignable_to(tuple[()], Sequence[int]))
 static_assert(not is_assignable_to(tuple[int, int], tuple[str, ...]))
 ```
 
+## Assignability of two mixed tuple types
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+```py
+from typing import Literal, Any, Sequence
+from ty_extensions import static_assert, is_assignable_to, Not, AlwaysFalsy
+
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...]],
+    )
+)
+
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...]],
+    )
+)
+
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...]],
+    )
+)
+
+static_assert(
+    not is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_assignable_to(
+        tuple[Literal[1], Literal[2], *tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+
+static_assert(
+    not is_assignable_to(
+        tuple[Literal[1], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_assignable_to(
+        tuple[Literal[1], *tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_assignable_to(
+        tuple[Literal[1], *tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+
+static_assert(
+    not is_assignable_to(
+        tuple[*tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_assignable_to(
+        tuple[*tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_assignable_to(
+        tuple[*tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+```
+
+## Assignability of the gradual tuple
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+As a [special case][gradual tuple], `tuple[Any, ...]` is a [gradual][gradual form] tuple type, which
+is assignable to every tuple of any length.
+
+```py
+from typing import Any
+from ty_extensions import static_assert, is_assignable_to
+
+static_assert(is_assignable_to(tuple[Any, ...], tuple[Any, ...]))
+static_assert(is_assignable_to(tuple[Any, ...], tuple[Any]))
+static_assert(is_assignable_to(tuple[Any, ...], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[Any, ...], tuple[int, ...]))
+static_assert(is_assignable_to(tuple[Any, ...], tuple[int]))
+static_assert(is_assignable_to(tuple[Any, ...], tuple[int, int]))
+```
+
+This also applies when `tuple[Any, ...]` is unpacked into a mixed tuple.
+
+```py
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[Any, ...]]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[Any, ...]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[int, ...]]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[int, ...]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[int]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], tuple[int, int]))
+
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[*tuple[Any, ...], int]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[Any, ...]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[Any]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[*tuple[int, ...], int]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[int, ...]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[int]))
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], tuple[int, int]))
+
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[Any, ...], int]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[Any, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[int, ...], int]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[int, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[int]))
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], tuple[int, int]))
+```
+
+The same is not true of fully static tuple types, since an unbounded homogeneous tuple is defined to
+be the _union_ of all tuple lengths, not the _gradual choice_ of them.
+
+```py
+static_assert(is_assignable_to(tuple[int, ...], tuple[Any, ...]))
+static_assert(not is_assignable_to(tuple[int, ...], tuple[Any]))
+static_assert(not is_assignable_to(tuple[int, ...], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[int, ...], tuple[int, ...]))
+static_assert(not is_assignable_to(tuple[int, ...], tuple[int]))
+static_assert(not is_assignable_to(tuple[int, ...], tuple[int, int]))
+
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...]], tuple[int, *tuple[Any, ...]]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...]], tuple[Any, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...]], tuple[Any]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...]], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...]], tuple[int, *tuple[int, ...]]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...]], tuple[int, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...]], tuple[int]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...]], tuple[int, int]))
+
+static_assert(is_assignable_to(tuple[*tuple[int, ...], int], tuple[*tuple[Any, ...], int]))
+static_assert(is_assignable_to(tuple[*tuple[int, ...], int], tuple[Any, ...]))
+static_assert(not is_assignable_to(tuple[*tuple[int, ...], int], tuple[Any]))
+static_assert(not is_assignable_to(tuple[*tuple[int, ...], int], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[*tuple[int, ...], int], tuple[*tuple[int, ...], int]))
+static_assert(is_assignable_to(tuple[*tuple[int, ...], int], tuple[int, ...]))
+static_assert(not is_assignable_to(tuple[*tuple[int, ...], int], tuple[int]))
+static_assert(not is_assignable_to(tuple[*tuple[int, ...], int], tuple[int, int]))
+
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[int, *tuple[Any, ...], int]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[Any, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[Any]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[Any, Any]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[int, *tuple[int, ...], int]))
+static_assert(is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[int, ...]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[int]))
+static_assert(not is_assignable_to(tuple[int, *tuple[int, ...], int], tuple[int, int]))
+```
+
 ## Union types
 
 ```py
@@ -828,8 +1050,8 @@ sets of possible materializations -- if they represent the same sets of possible
 sets of sets of possible runtime objects). By this principle `int | Any` is gradually equivalent to
 `Unknown | int`, since they have exactly the same sets of posisble materializations. But
 `bool | Any` is not equivalent to `int`, since there are many possible materializations of
-`bool | Any` that are not assignable to `int`. It is therefore *not* necessary for `X` to be
-gradually equivalent to `Y` in order for `Foo[X]` to be assignable to `Foo[Y]`; it is *only*
+`bool | Any` that are not assignable to `int`. It is therefore _not_ necessary for `X` to be
+gradually equivalent to `Y` in order for `Foo[X]` to be assignable to `Foo[Y]`; it is _only_
 necessary for `X` and `Y` to be mutually assignable.
 
 ```py
@@ -887,4 +1109,6 @@ static_assert(not is_assignable_to(TypeGuard[Unknown], str))  # error: [static-a
 static_assert(not is_assignable_to(TypeIs[Any], str))
 ```
 
+[gradual form]: https://typing.python.org/en/latest/spec/glossary.html#term-gradual-form
+[gradual tuple]: https://typing.python.org/en/latest/spec/tuples.html#tuple-type-form
 [typing documentation]: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation

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

@@ -48,8 +48,7 @@ static_assert(not is_fully_static(Any | str))
 static_assert(not is_fully_static(str | Unknown))
 static_assert(not is_fully_static(Intersection[Any, Not[LiteralString]]))
 
-# TODO: should pass
-static_assert(not is_fully_static(tuple[Any, ...]))  # error: [static-assert-error]
+static_assert(not is_fully_static(tuple[Any, ...]))
 
 static_assert(not is_fully_static(tuple[int, Any]))
 static_assert(not is_fully_static(type[Any]))

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

@@ -159,6 +159,11 @@ from typing import Literal, Any, Sequence
 from ty_extensions import static_assert, is_subtype_of, Not, AlwaysFalsy
 
 static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[Literal[1, 2], ...]))
+static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[Literal[1], *tuple[Literal[2], ...]]))
+static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[*tuple[Literal[1], ...], Literal[2]]))
+static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[Literal[1], *tuple[str, ...], Literal[2]]))
+static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[Literal[1], Literal[2], *tuple[str, ...]]))
+static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[*tuple[str, ...], Literal[1], Literal[2]]))
 static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[int, ...]))
 static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[int | str, ...]))
 static_assert(is_subtype_of(tuple[Literal[1], Literal[2]], tuple[Not[AlwaysFalsy], ...]))
@@ -177,6 +182,215 @@ static_assert(not is_subtype_of(tuple[int, ...], Sequence[Any]))
 static_assert(not is_subtype_of(tuple[Any, ...], Sequence[int]))
 ```
 
+## Subtyping of two mixed tuple types
+
+```py
+from typing import Literal, Any, Sequence
+from ty_extensions import static_assert, is_subtype_of, Not, AlwaysFalsy
+
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...]],
+    )
+)
+
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], *tuple[int, ...]],
+    )
+)
+
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...], Literal[10]],
+    )
+)
+static_assert(
+    is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[*tuple[int, ...]],
+    )
+)
+
+static_assert(
+    not is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_subtype_of(
+        tuple[Literal[1], Literal[2], *tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+
+static_assert(
+    not is_subtype_of(
+        tuple[Literal[1], *tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_subtype_of(
+        tuple[Literal[1], *tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_subtype_of(
+        tuple[Literal[1], *tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+
+static_assert(
+    not is_subtype_of(
+        tuple[*tuple[int, ...], Literal[9], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_subtype_of(
+        tuple[*tuple[int, ...], Literal[10]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+static_assert(
+    not is_subtype_of(
+        tuple[*tuple[int, ...]],
+        tuple[Literal[1], Literal[2], *tuple[int, ...], Literal[9], Literal[10]],
+    )
+)
+```
+
+## Subtyping of the gradual tuple
+
+```toml
+[environment]
+python-version = "3.12"
+```
+
+As a [special case][gradual tuple], `tuple[Any, ...]` is a [gradual][gradual form] tuple type.
+However, the special-case behavior of assignability does not also apply to subtyping, since gradual
+types to not participate in subtyping.
+
+```py
+from typing import Any
+from ty_extensions import static_assert, is_subtype_of
+
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[Any, Any]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[int]))
+static_assert(not is_subtype_of(tuple[Any, ...], tuple[int, int]))
+```
+
+Subtyping also does not apply when `tuple[Any, ...]` is unpacked into a mixed tuple.
+
+```py
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[Any, Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, *tuple[int, ...]]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...]], tuple[int, int]))
+
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[*tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[Any, Any]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[*tuple[int, ...], int]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int]))
+static_assert(not is_subtype_of(tuple[*tuple[Any, ...], int], tuple[int, int]))
+
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[Any, Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, *tuple[int, ...], int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[Any, ...], int], tuple[int, int]))
+```
+
+Subtyping does apply to unbounded homogeneous tuples of a fully static type. However, such tuples
+are defined to be the _union_ of all tuple lengths, not the _gradual choice_ of them, so no
+variable-length tuples are a subtyping of _any_ fixed-length tuple.
+
+```py
+static_assert(not is_subtype_of(tuple[int, ...], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[int, ...], tuple[Any]))
+static_assert(not is_subtype_of(tuple[int, ...], tuple[Any, Any]))
+static_assert(is_subtype_of(tuple[int, ...], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[int, ...], tuple[int]))
+static_assert(not is_subtype_of(tuple[int, ...], tuple[int, int]))
+
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[int, *tuple[Any, ...]]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[Any, Any]))
+static_assert(is_subtype_of(tuple[int, *tuple[int, ...]], tuple[int, *tuple[int, ...]]))
+static_assert(is_subtype_of(tuple[int, *tuple[int, ...]], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...]], tuple[int, int]))
+
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[*tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[Any]))
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[Any, Any]))
+static_assert(is_subtype_of(tuple[*tuple[int, ...], int], tuple[*tuple[int, ...], int]))
+static_assert(is_subtype_of(tuple[*tuple[int, ...], int], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[int]))
+static_assert(not is_subtype_of(tuple[*tuple[int, ...], int], tuple[int, int]))
+
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[int, *tuple[Any, ...], int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[Any, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[Any]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[Any, Any]))
+static_assert(is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[int, *tuple[int, ...], int]))
+static_assert(is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[int, ...]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[int]))
+static_assert(not is_subtype_of(tuple[int, *tuple[int, ...], int], tuple[int, int]))
+```
+
 ## Union types
 
 ```py
@@ -1639,5 +1853,7 @@ static_assert(is_subtype_of(CallableTypeOf[overload_ab], CallableTypeOf[overload
 static_assert(is_subtype_of(CallableTypeOf[overload_ba], CallableTypeOf[overload_ab]))
 ```
 
+[gradual form]: https://typing.python.org/en/latest/spec/glossary.html#term-gradual-form
+[gradual tuple]: https://typing.python.org/en/latest/spec/tuples.html#tuple-type-form
 [special case for float and complex]: https://typing.python.org/en/latest/spec/special-types.html#special-cases-for-float-and-complex
 [typing documentation]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence