Thanks everyone for your input. It sounds like most of you (including all of the representatives of the major type checkers) prefer option 2. This is also the behavior that most typed Python code bases today assume, since it’s the behavior that mypy and pyright implement today.
Before I formally write up this proposal for consideration by the full Typing Council, we need to pin down the meaning of tuple[Any, ...] and tuple (with no type arguments). Here are three options:
2a: tuple[Any, ...] follows the same rules as tuple[T, ...]. It implies a union of tuple[()] | tuple[Any] | tuple[Any, Any] | .... tuple is a synonym for tuple[Any, ...].
2b: Unlike the general case of tuple[T, ...], tuple[Any, ...] is considered a gradual type. It is bidirectionally type compatible with any tuple regardless of length. tuple is a synonym for tuple[Any, ...].
2c: We introduce a new form tuple[...], a gradual type that is bidirectionally type compatible with any tuple of any length. The type tuple[Any, ...] is treated as described in option 2a. tuple is a synonym of tuple[...].
Currently, mypy implements option 2b and pyright implements option 2a.
Option 2b would probably be the least disruptive, but I dislike the inconsistency it implies. Inconsistencies like this almost always create problems when composing typing features. For example, how would this be interpreted: tuple[int, *tuple[Any, ...], int]?
Option 2a is consistent but would be potentially disruptive for mypy users. It also leaves the type system without a way to spell “any tuple regardless of its length”.
Option 2c is the most flexible, but it’s also the most disruptive in the short term.
Thoughts?