[ty] Add property test generators for variable-length tuples (#18901)

Add property test generators for the new variable-length tuples. This
covers homogeneous tuples as well.

The property tests did their job! This identified several fixes we
needed to make to various type property methods.

cf https://github.com/astral-sh/ruff/pull/18600#issuecomment-2993764471

---------

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

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

@@ -99,13 +99,138 @@ static_assert(is_singleton(None))
 static_assert(not is_singleton(tuple[None]))
 ```
 
+## Tuples containing `Never`
+
+```toml
+[environment]
+python-version = "3.11"
+```
+
+The `Never` type contains no inhabitants, so a tuple type that contains `Never` as a mandatory
+element also contains no inhabitants.
+
+```py
+from typing import Never
+from ty_extensions import static_assert, is_equivalent_to
+
+static_assert(is_equivalent_to(tuple[Never], Never))
+static_assert(is_equivalent_to(tuple[int, Never], Never))
+static_assert(is_equivalent_to(tuple[Never, *tuple[int, ...]], Never))
+```
+
+If the variable-length portion of a tuple is `Never`, then that portion of the tuple must always be
+empty. This means that the tuple is not actually variable-length!
+
+```py
+from typing import Never
+from ty_extensions import static_assert, is_equivalent_to
+
+static_assert(is_equivalent_to(tuple[Never, ...], tuple[()]))
+static_assert(is_equivalent_to(tuple[int, *tuple[Never, ...]], tuple[int]))
+static_assert(is_equivalent_to(tuple[int, *tuple[Never, ...], int], tuple[int, int]))
+static_assert(is_equivalent_to(tuple[*tuple[Never, ...], int], tuple[int]))
+```
+
+## Homogeneous non-empty tuples
+
+```toml
+[environment]
+python-version = "3.11"
+```
+
+A homogeneous tuple can contain zero or more elements of a particular type. You can represent a
+tuple that can contain _one_ or more elements of that type (or any other number of minimum elements)
+using a mixed tuple.
+
+```py
+def takes_zero_or_more(t: tuple[int, ...]) -> None: ...
+def takes_one_or_more(t: tuple[int, *tuple[int, ...]]) -> None: ...
+def takes_two_or_more(t: tuple[int, int, *tuple[int, ...]]) -> None: ...
+
+takes_zero_or_more(())
+takes_zero_or_more((1,))
+takes_zero_or_more((1, 2))
+
+takes_one_or_more(())  # error: [invalid-argument-type]
+takes_one_or_more((1,))
+takes_one_or_more((1, 2))
+
+takes_two_or_more(())  # error: [invalid-argument-type]
+takes_two_or_more((1,))  # error: [invalid-argument-type]
+takes_two_or_more((1, 2))
+```
+
+The required elements can also appear in the suffix of the mixed tuple type.
+
+```py
+def takes_one_or_more_suffix(t: tuple[*tuple[int, ...], int]) -> None: ...
+def takes_two_or_more_suffix(t: tuple[*tuple[int, ...], int, int]) -> None: ...
+def takes_two_or_more_mixed(t: tuple[int, *tuple[int, ...], int]) -> None: ...
+
+takes_one_or_more_suffix(())  # error: [invalid-argument-type]
+takes_one_or_more_suffix((1,))
+takes_one_or_more_suffix((1, 2))
+
+takes_two_or_more_suffix(())  # error: [invalid-argument-type]
+takes_two_or_more_suffix((1,))  # error: [invalid-argument-type]
+takes_two_or_more_suffix((1, 2))
+
+takes_two_or_more_mixed(())  # error: [invalid-argument-type]
+takes_two_or_more_mixed((1,))  # error: [invalid-argument-type]
+takes_two_or_more_mixed((1, 2))
+```
+
+The tuple types are equivalent regardless of whether the required elements appear in the prefix or
+suffix.
+
+```py
+from ty_extensions import static_assert, is_subtype_of, is_equivalent_to
+
+static_assert(is_equivalent_to(tuple[int, *tuple[int, ...]], tuple[*tuple[int, ...], int]))
+
+static_assert(is_equivalent_to(tuple[int, int, *tuple[int, ...]], tuple[*tuple[int, ...], int, int]))
+static_assert(is_equivalent_to(tuple[int, int, *tuple[int, ...]], tuple[int, *tuple[int, ...], int]))
+```
+
+This is true when the prefix/suffix and variable-length types are equivalent, not just identical.
+
+```py
+from ty_extensions import static_assert, is_subtype_of, is_equivalent_to
+
+static_assert(is_equivalent_to(tuple[int | str, *tuple[str | int, ...]], tuple[*tuple[str | int, ...], int | str]))
+
+static_assert(
+    is_equivalent_to(tuple[int | str, str | int, *tuple[str | int, ...]], tuple[*tuple[int | str, ...], str | int, int | str])
+)
+static_assert(
+    is_equivalent_to(tuple[int | str, str | int, *tuple[str | int, ...]], tuple[str | int, *tuple[int | str, ...], int | str])
+)
+```
+
 ## Disjointness
 
-A tuple `tuple[P1, P2]` is disjoint from a tuple `tuple[Q1, Q2]` if either `P1` is disjoint from
+```toml
-`Q1` or if `P2` is disjoint from `Q2`:
+[environment]
+python-version = "3.11"
+```
+
+Two tuples with incompatible minimum lengths are always disjoint, regardless of their element types.
+(The lengths are incompatible if the minimum length of one tuple is larger than the maximum length
+of the other.)
 
 ```py
 from ty_extensions import static_assert, is_disjoint_from
+
+static_assert(is_disjoint_from(tuple[()], tuple[int]))
+static_assert(not is_disjoint_from(tuple[()], tuple[int, ...]))
+static_assert(not is_disjoint_from(tuple[int], tuple[int, ...]))
+static_assert(not is_disjoint_from(tuple[str, ...], tuple[int, ...]))
+```
+
+A tuple that is required to contain elements `P1, P2` is disjoint from a tuple that is required to
+contain elements `Q1, Q2` if either `P1` is disjoint from `Q1` or if `P2` is disjoint from `Q2`.
+
+```py
 from typing import final
 
 @final
@@ -124,9 +249,28 @@ static_assert(is_disjoint_from(tuple[F1, F2], tuple[F2, F1]))
 static_assert(is_disjoint_from(tuple[F1, N1], tuple[F2, N2]))
 static_assert(is_disjoint_from(tuple[N1, F1], tuple[N2, F2]))
 static_assert(not is_disjoint_from(tuple[N1, N2], tuple[N2, N1]))
+
+static_assert(is_disjoint_from(tuple[F1, *tuple[int, ...], F2], tuple[F2, *tuple[int, ...], F1]))
+static_assert(is_disjoint_from(tuple[F1, *tuple[int, ...], N1], tuple[F2, *tuple[int, ...], N2]))
+static_assert(is_disjoint_from(tuple[N1, *tuple[int, ...], F1], tuple[N2, *tuple[int, ...], F2]))
+static_assert(not is_disjoint_from(tuple[N1, *tuple[int, ...], N2], tuple[N2, *tuple[int, ...], N1]))
+
+static_assert(not is_disjoint_from(tuple[F1, F2, *tuple[object, ...]], tuple[*tuple[object, ...], F2, F1]))
+static_assert(not is_disjoint_from(tuple[F1, N1, *tuple[object, ...]], tuple[*tuple[object, ...], F2, N2]))
+static_assert(not is_disjoint_from(tuple[N1, F1, *tuple[object, ...]], tuple[*tuple[object, ...], N2, F2]))
+static_assert(not is_disjoint_from(tuple[N1, N2, *tuple[object, ...]], tuple[*tuple[object, ...], N2, N1]))
 ```
 
-We currently model tuple types to *not* be disjoint from arbitrary instance types, because we allow
+The variable-length portion of a tuple can never cause the tuples to be disjoint, since all
+variable-length tuple types contain the empty tuple. (Note that per above, the variable-length
+portion of a tuple cannot be `Never`; internally we simplify this to a fixed-length tuple.)
+
+```py
+static_assert(not is_disjoint_from(tuple[F1, ...], tuple[F2, ...]))
+static_assert(not is_disjoint_from(tuple[N1, ...], tuple[N2, ...]))
+```
+
+We currently model tuple types to _not_ be disjoint from arbitrary instance types, because we allow
 for the possibility of `tuple` to be subclassed
 
 ```py
@@ -152,21 +296,71 @@ class CommonSubtypeOfTuples(I1, I2): ...
 
 ## Truthiness
 
-The truthiness of the empty tuple is `False`:
+```toml
-
+[environment]
-```py
+python-version = "3.11"
-from typing_extensions import assert_type, Literal
-
-assert_type(bool(()), Literal[False])
 ```
 
-The truthiness of non-empty tuples is always `True`, even if all elements are falsy:
+The truthiness of the empty tuple is `False`.
 
 ```py
 from typing_extensions import assert_type, Literal
+from ty_extensions import static_assert, is_assignable_to, AlwaysFalsy
+
+assert_type(bool(()), Literal[False])
+
+static_assert(is_assignable_to(tuple[()], AlwaysFalsy))
+```
+
+The truthiness of non-empty tuples is always `True`. This is true even if all elements are falsy,
+and even if any element is gradual, since the truthiness of a tuple depends only on its length, not
+its content.
+
+```py
+from typing_extensions import assert_type, Any, Literal
+from ty_extensions import static_assert, is_assignable_to, AlwaysTruthy
 
 assert_type(bool((False,)), Literal[True])
 assert_type(bool((False, False)), Literal[True])
+
+static_assert(is_assignable_to(tuple[Any], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[Any, Any], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[bool], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[bool, bool], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[Literal[False]], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[Literal[False], Literal[False]], AlwaysTruthy))
+```
+
+The truthiness of variable-length tuples is ambiguous, since that type contains both empty and
+non-empty tuples.
+
+```py
+from typing_extensions import Any, Literal
+from ty_extensions import static_assert, is_assignable_to, AlwaysFalsy, AlwaysTruthy
+
+static_assert(not is_assignable_to(tuple[Any, ...], AlwaysFalsy))
+static_assert(not is_assignable_to(tuple[Any, ...], AlwaysTruthy))
+static_assert(not is_assignable_to(tuple[bool, ...], AlwaysFalsy))
+static_assert(not is_assignable_to(tuple[bool, ...], AlwaysTruthy))
+static_assert(not is_assignable_to(tuple[Literal[False], ...], AlwaysFalsy))
+static_assert(not is_assignable_to(tuple[Literal[False], ...], AlwaysTruthy))
+static_assert(not is_assignable_to(tuple[Literal[True], ...], AlwaysFalsy))
+static_assert(not is_assignable_to(tuple[Literal[True], ...], AlwaysTruthy))
+
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...]], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[bool, ...]], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[Literal[False], ...]], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[Literal[True], ...]], AlwaysTruthy))
+
+static_assert(is_assignable_to(tuple[*tuple[Any, ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[*tuple[bool, ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[*tuple[Literal[False], ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[*tuple[Literal[True], ...], int], AlwaysTruthy))
+
+static_assert(is_assignable_to(tuple[int, *tuple[Any, ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[bool, ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[Literal[False], ...], int], AlwaysTruthy))
+static_assert(is_assignable_to(tuple[int, *tuple[Literal[True], ...], int], AlwaysTruthy))
 ```
 
 Both of these results are conflicting with the fact that tuples can be subclassed, and that we

crates/ty_python_semantic/src/types.rs

@@ -3467,7 +3467,14 @@ impl<'db> Type<'db> {
             Type::BooleanLiteral(bool) => Truthiness::from(*bool),
             Type::StringLiteral(str) => Truthiness::from(!str.value(db).is_empty()),
             Type::BytesLiteral(bytes) => Truthiness::from(!bytes.value(db).is_empty()),
-            Type::Tuple(tuple) => Truthiness::from(!tuple.tuple(db).is_empty()),
+            Type::Tuple(tuple) => match tuple.tuple(db).size_hint() {
+                // The tuple type is AlwaysFalse if it contains only the empty tuple
+                (_, Some(0)) => Truthiness::AlwaysFalse,
+                // The tuple type is AlwaysTrue if its inhabitants must always have length >=1
+                (minimum, _) if minimum > 0 => Truthiness::AlwaysTrue,
+                // The tuple type is Ambiguous if its inhabitants could be of any length
+                _ => Truthiness::Ambiguous,
+            },
         };
 
         Ok(truthiness)

crates/ty_python_semantic/src/types/call/bind.rs

@@ -394,7 +394,7 @@ impl<'db> Bindings<'db> {
                                     Some("__constraints__") => {
                                         overload.set_return_type(TupleType::from_elements(
                                             db,
-                                            typevar.constraints(db).into_iter().flatten(),
+                                            typevar.constraints(db).into_iter().flatten().copied(),
                                         ));
                                     }
                                     Some("__default__") => {

crates/ty_python_semantic/src/types/class.rs

@@ -1155,7 +1155,7 @@ impl<'db> ClassLiteral<'db> {
             }
         } else {
             let name = Type::string_literal(db, self.name(db));
-            let bases = TupleType::from_elements(db, self.explicit_bases(db));
+            let bases = TupleType::from_elements(db, self.explicit_bases(db).iter().copied());
             let namespace = KnownClass::Dict
                 .to_specialized_instance(db, [KnownClass::Str.to_instance(db), Type::any()]);
 

crates/ty_python_semantic/src/types/infer.rs

@@ -8200,7 +8200,7 @@ impl<'db, 'ast> TypeInferenceBuilder<'db, 'ast> {
                 };
 
                 if let Ok(new_elements) = tuple.py_slice(self.db(), start, stop, step) {
-                    TupleType::from_elements(self.db(), new_elements)
+                    TupleType::from_elements(self.db(), new_elements.copied())
                 } else {
                     report_slice_step_size_zero(&self.context, value_node.into());
                     Type::unknown()

crates/ty_python_semantic/src/types/property_tests/type_generation.rs

@@ -39,7 +39,8 @@ pub(crate) enum Ty {
         pos: Vec<Ty>,
         neg: Vec<Ty>,
     },
-    Tuple(Vec<Ty>),
+    FixedLengthTuple(Vec<Ty>),
+    VariableLengthTuple(Vec<Ty>, Box<Ty>, Vec<Ty>),
     SubclassOfAny,
     SubclassOfBuiltinClass(&'static str),
     SubclassOfAbcClass(&'static str),
@@ -159,10 +160,16 @@ impl Ty {
                 }
                 builder.build()
             }
-            Ty::Tuple(tys) => {
+            Ty::FixedLengthTuple(tys) => {
                 let elements = tys.into_iter().map(|ty| ty.into_type(db));
                 TupleType::from_elements(db, elements)
             }
+            Ty::VariableLengthTuple(prefix, variable, suffix) => {
+                let prefix = prefix.into_iter().map(|ty| ty.into_type(db));
+                let variable = variable.into_type(db);
+                let suffix = suffix.into_iter().map(|ty| ty.into_type(db));
+                TupleType::mixed(db, prefix, variable, suffix)
+            }
             Ty::SubclassOfAny => SubclassOfType::subclass_of_any(),
             Ty::SubclassOfBuiltinClass(s) => SubclassOfType::from(
                 db,
@@ -268,19 +275,28 @@ fn arbitrary_type(g: &mut Gen, size: u32) -> Ty {
     if size == 0 {
         arbitrary_core_type(g)
     } else {
-        match u32::arbitrary(g) % 5 {
+        match u32::arbitrary(g) % 6 {
             0 => arbitrary_core_type(g),
             1 => Ty::Union(
                 (0..*g.choose(&[2, 3]).unwrap())
                     .map(|_| arbitrary_type(g, size - 1))
                     .collect(),
             ),
-            2 => Ty::Tuple(
+            2 => Ty::FixedLengthTuple(
                 (0..*g.choose(&[0, 1, 2]).unwrap())
                     .map(|_| arbitrary_type(g, size - 1))
                     .collect(),
             ),
-            3 => Ty::Intersection {
+            3 => Ty::VariableLengthTuple(
+                (0..*g.choose(&[0, 1, 2]).unwrap())
+                    .map(|_| arbitrary_type(g, size - 1))
+                    .collect(),
+                Box::new(arbitrary_type(g, size - 1)),
+                (0..*g.choose(&[0, 1, 2]).unwrap())
+                    .map(|_| arbitrary_type(g, size - 1))
+                    .collect(),
+            ),
+            4 => Ty::Intersection {
                 pos: (0..*g.choose(&[0, 1, 2]).unwrap())
                     .map(|_| arbitrary_type(g, size - 1))
                     .collect(),
@@ -288,7 +304,7 @@ fn arbitrary_type(g: &mut Gen, size: u32) -> Ty {
                     .map(|_| arbitrary_type(g, size - 1))
                     .collect(),
             },
-            4 => Ty::Callable {
+            5 => Ty::Callable {
                 params: match u32::arbitrary(g) % 2 {
                     0 => CallableParams::GradualForm,
                     1 => CallableParams::List(arbitrary_parameter_list(g, size)),
@@ -398,11 +414,34 @@ impl Arbitrary for Ty {
                 1 => Some(elts.into_iter().next().unwrap()),
                 _ => Some(Ty::Union(elts)),
             })),
-            Ty::Tuple(types) => Box::new(types.shrink().filter_map(|elts| match elts.len() {
+            Ty::FixedLengthTuple(types) => {
-                0 => None,
+                Box::new(types.shrink().filter_map(|elts| match elts.len() {
-                1 => Some(elts.into_iter().next().unwrap()),
+                    0 => None,
-                _ => Some(Ty::Tuple(elts)),
+                    1 => Some(elts.into_iter().next().unwrap()),
-            })),
+                    _ => Some(Ty::FixedLengthTuple(elts)),
+                }))
+            }
+            Ty::VariableLengthTuple(prefix, variable, suffix) => {
+                // We shrink the suffix first, then the prefix, then the variable-length type.
+                let suffix_shrunk = suffix.shrink().map({
+                    let prefix = prefix.clone();
+                    let variable = variable.clone();
+                    move |suffix| Ty::VariableLengthTuple(prefix.clone(), variable.clone(), suffix)
+                });
+                let prefix_shrunk = prefix.shrink().map({
+                    let variable = variable.clone();
+                    let suffix = suffix.clone();
+                    move |prefix| Ty::VariableLengthTuple(prefix, variable.clone(), suffix.clone())
+                });
+                let variable_shrunk = variable.shrink().map({
+                    let prefix = prefix.clone();
+                    let suffix = suffix.clone();
+                    move |variable| {
+                        Ty::VariableLengthTuple(prefix.clone(), variable, suffix.clone())
+                    }
+                });
+                Box::new(suffix_shrunk.chain(prefix_shrunk).chain(variable_shrunk))
+            }
             Ty::Intersection { pos, neg } => {
                 // Shrinking on intersections is not exhaustive!
                 //

crates/ty_python_semantic/src/types/tuple.rs

@@ -36,8 +36,7 @@ pub struct TupleType<'db> {
 impl<'db> Type<'db> {
     pub(crate) fn tuple(db: &'db dyn Db, tuple: TupleType<'db>) -> Self {
         // If a fixed-length (i.e., mandatory) element of the tuple is `Never`, then it's not
-        // possible to instantiate the tuple as a whole. (This is not true of the variable-length
+        // possible to instantiate the tuple as a whole.
-        // portion of the tuple, since it can contain no elements.)
         if tuple.tuple(db).fixed_elements().any(|ty| ty.is_never()) {
             return Type::Never;
         }
@@ -55,7 +54,7 @@ impl<'db> TupleType<'db> {
 
     pub(crate) fn from_elements(
         db: &'db dyn Db,
-        types: impl IntoIterator<Item = impl Into<Type<'db>>>,
+        types: impl IntoIterator<Item = Type<'db>>,
     ) -> Type<'db> {
         Type::tuple(
             db,
@@ -69,16 +68,13 @@ impl<'db> TupleType<'db> {
     #[cfg(test)]
     pub(crate) fn mixed(
         db: &'db dyn Db,
-        prefix: impl IntoIterator<Item = impl Into<Type<'db>>>,
+        prefix: impl IntoIterator<Item = Type<'db>>,
         variable: Type<'db>,
-        suffix: impl IntoIterator<Item = impl Into<Type<'db>>>,
+        suffix: impl IntoIterator<Item = Type<'db>>,
     ) -> Type<'db> {
         Type::tuple(
             db,
-            TupleType::new(
+            TupleType::new(db, VariableLengthTupleSpec::mixed(prefix, variable, suffix)),
-                db,
-                TupleSpec::from(VariableLengthTupleSpec::mixed(prefix, variable, suffix)),
-            ),
         )
     }
 
@@ -175,15 +171,17 @@ impl<'db> FixedLengthTupleSpec<'db> {
         Self(Vec::with_capacity(capacity))
     }
 
-    pub(crate) fn from_elements(elements: impl IntoIterator<Item = impl Into<Type<'db>>>) -> Self {
+    pub(crate) fn from_elements(elements: impl IntoIterator<Item = Type<'db>>) -> Self {
-        Self(elements.into_iter().map(Into::into).collect())
+        Self(elements.into_iter().collect())
     }
 
     pub(crate) fn elements_slice(&self) -> &[Type<'db>] {
         &self.0
     }
 
-    pub(crate) fn elements(&self) -> impl Iterator<Item = Type<'db>> + '_ {
+    pub(crate) fn elements(
+        &self,
+    ) -> impl DoubleEndedIterator<Item = Type<'db>> + ExactSizeIterator + '_ {
         self.0.iter().copied()
     }
 
@@ -198,23 +196,15 @@ impl<'db> FixedLengthTupleSpec<'db> {
 
     fn concat(&self, other: &TupleSpec<'db>) -> TupleSpec<'db> {
         match other {
-            TupleSpec::Fixed(other) => {
+            TupleSpec::Fixed(other) => TupleSpec::Fixed(FixedLengthTupleSpec::from_elements(
-                let mut elements = Vec::with_capacity(self.0.len() + other.0.len());
+                self.elements().chain(other.elements()),
-                elements.extend_from_slice(&self.0);
+            )),
-                elements.extend_from_slice(&other.0);
-                TupleSpec::Fixed(FixedLengthTupleSpec(elements))
-            }
 
-            TupleSpec::Variable(other) => {
+            TupleSpec::Variable(other) => VariableLengthTupleSpec::mixed(
-                let mut prefix = Vec::with_capacity(self.0.len() + other.prefix.len());
+                self.elements().chain(other.prefix_elements()),
-                prefix.extend_from_slice(&self.0);
+                other.variable,
-                prefix.extend_from_slice(&other.prefix);
+                other.suffix_elements(),
-                TupleSpec::Variable(VariableLengthTupleSpec {
+            ),
-                    prefix,
-                    variable: other.variable,
-                    suffix: other.suffix.clone(),
-                })
-            }
         }
     }
 
@@ -228,24 +218,18 @@ impl<'db> FixedLengthTupleSpec<'db> {
 
     #[must_use]
     fn normalized(&self, db: &'db dyn Db) -> Self {
-        Self(self.0.iter().map(|ty| ty.normalized(db)).collect())
+        Self::from_elements(self.0.iter().map(|ty| ty.normalized(db)))
     }
 
     fn materialize(&self, db: &'db dyn Db, variance: TypeVarVariance) -> Self {
-        Self(
+        Self::from_elements(self.0.iter().map(|ty| ty.materialize(db, variance)))
-            self.0
-                .iter()
-                .map(|ty| ty.materialize(db, variance))
-                .collect(),
-        )
     }
 
     fn apply_type_mapping<'a>(&self, db: &'db dyn Db, type_mapping: &TypeMapping<'a, 'db>) -> Self {
-        Self(
+        Self::from_elements(
             self.0
                 .iter()
-                .map(|ty| ty.apply_type_mapping(db, type_mapping))
+                .map(|ty| ty.apply_type_mapping(db, type_mapping)),
-                .collect(),
         )
     }
 
@@ -315,13 +299,6 @@ impl<'db> FixedLengthTupleSpec<'db> {
                 .all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
     }
 
-    fn is_disjoint_from(&self, db: &'db dyn Db, other: &Self) -> bool {
-        self.0.len() != other.0.len()
-            || (self.0.iter())
-                .zip(&other.0)
-                .any(|(self_ty, other_ty)| self_ty.is_disjoint_from(db, *other_ty))
-    }
-
     fn is_fully_static(&self, db: &'db dyn Db) -> bool {
         self.0.iter().all(|ty| ty.is_fully_static(db))
     }
@@ -371,35 +348,110 @@ pub struct VariableLengthTupleSpec<'db> {
 impl<'db> VariableLengthTupleSpec<'db> {
     /// Creates a new tuple spec containing zero or more elements of a given type, with no prefix
     /// or suffix.
-    fn homogeneous(ty: Type<'db>) -> Self {
+    fn homogeneous(ty: Type<'db>) -> TupleSpec<'db> {
-        Self {
+        Self::mixed([], ty, [])
-            prefix: vec![],
-            variable: ty,
-            suffix: vec![],
-        }
     }
 
-    #[cfg(test)]
     fn mixed(
-        prefix: impl IntoIterator<Item = impl Into<Type<'db>>>,
+        prefix: impl IntoIterator<Item = Type<'db>>,
         variable: Type<'db>,
-        suffix: impl IntoIterator<Item = impl Into<Type<'db>>>,
+        suffix: impl IntoIterator<Item = Type<'db>>,
-    ) -> Self {
+    ) -> TupleSpec<'db> {
-        Self {
+        // If the variable-length portion is Never, it can only be instantiated with zero elements.
-            prefix: prefix.into_iter().map(Into::into).collect(),
+        // That means this isn't a variable-length tuple after all!
-            variable,
+        if variable.is_never() {
-            suffix: suffix.into_iter().map(Into::into).collect(),
+            return TupleSpec::Fixed(FixedLengthTupleSpec::from_elements(
+                prefix.into_iter().chain(suffix),
+            ));
         }
+
+        TupleSpec::Variable(Self {
+            prefix: prefix.into_iter().collect(),
+            variable,
+            suffix: suffix.into_iter().collect(),
+        })
+    }
+
+    fn prefix_elements(
+        &self,
+    ) -> impl DoubleEndedIterator<Item = Type<'db>> + ExactSizeIterator + '_ {
+        self.prefix.iter().copied()
+    }
+
+    /// Returns the prefix of the prenormalization of this tuple.
+    ///
+    /// This is used in our subtyping and equivalence checks below to handle different tuple types
+    /// that represent the same set of runtime tuple values. For instance, the following two tuple
+    /// types both represent "a tuple of one or more `int`s":
+    ///
+    /// ```py
+    /// tuple[int, *tuple[int, ...]]
+    /// tuple[*tuple[int, ...], int]
+    /// ```
+    ///
+    /// Prenormalization rewrites both types into the former form. We arbitrarily prefer the
+    /// elements to appear in the prefix if they can, so we move elements from the beginning of the
+    /// suffix, which are equivalent to the variable-length portion, to the end of the prefix.
+    ///
+    /// Complicating matters is that we don't always want to compare with _this_ tuple's
+    /// variable-length portion. (When this tuple's variable-length portion is gradual —
+    /// `tuple[Any, ...]` — we compare with the assumption that the `Any` materializes to the other
+    /// tuple's variable-length portion.)
+    fn prenormalized_prefix_elements<'a>(
+        &'a self,
+        db: &'db dyn Db,
+        variable: Option<Type<'db>>,
+    ) -> impl Iterator<Item = Type<'db>> + 'a {
+        let variable = variable.unwrap_or(self.variable);
+        self.prefix_elements().chain(
+            self.suffix_elements()
+                .take_while(move |element| element.is_equivalent_to(db, variable)),
+        )
+    }
+
+    fn suffix_elements(
+        &self,
+    ) -> impl DoubleEndedIterator<Item = Type<'db>> + ExactSizeIterator + '_ {
+        self.suffix.iter().copied()
+    }
+
+    /// Returns the suffix of the prenormalization of this tuple.
+    ///
+    /// This is used in our subtyping and equivalence checks below to handle different tuple types
+    /// that represent the same set of runtime tuple values. For instance, the following two tuple
+    /// types both represent "a tuple of one or more `int`s":
+    ///
+    /// ```py
+    /// tuple[int, *tuple[int, ...]]
+    /// tuple[*tuple[int, ...], int]
+    /// ```
+    ///
+    /// Prenormalization rewrites both types into the former form. We arbitrarily prefer the
+    /// elements to appear in the prefix if they can, so we move elements from the beginning of the
+    /// suffix, which are equivalent to the variable-length portion, to the end of the prefix.
+    ///
+    /// Complicating matters is that we don't always want to compare with _this_ tuple's
+    /// variable-length portion. (When this tuple's variable-length portion is gradual —
+    /// `tuple[Any, ...]` — we compare with the assumption that the `Any` materializes to the other
+    /// tuple's variable-length portion.)
+    fn prenormalized_suffix_elements<'a>(
+        &'a self,
+        db: &'db dyn Db,
+        variable: Option<Type<'db>>,
+    ) -> impl Iterator<Item = Type<'db>> + 'a {
+        let variable = variable.unwrap_or(self.variable);
+        self.suffix_elements()
+            .skip_while(move |element| element.is_equivalent_to(db, variable))
     }
 
     fn fixed_elements(&self) -> impl Iterator<Item = Type<'db>> + '_ {
-        (self.prefix.iter().copied()).chain(self.suffix.iter().copied())
+        self.prefix_elements().chain(self.suffix_elements())
     }
 
     fn all_elements(&self) -> impl Iterator<Item = Type<'db>> + '_ {
-        (self.prefix.iter().copied())
+        self.prefix_elements()
             .chain(std::iter::once(self.variable))
-            .chain(self.suffix.iter().copied())
+            .chain(self.suffix_elements())
     }
 
     /// Returns the minimum length of this tuple.
@@ -409,29 +461,24 @@ impl<'db> VariableLengthTupleSpec<'db> {
 
     fn concat(&self, db: &'db dyn Db, other: &TupleSpec<'db>) -> TupleSpec<'db> {
         match other {
-            TupleSpec::Fixed(other) => {
+            TupleSpec::Fixed(other) => VariableLengthTupleSpec::mixed(
-                let mut suffix = Vec::with_capacity(self.suffix.len() + other.0.len());
+                self.prefix_elements(),
-                suffix.extend_from_slice(&self.suffix);
+                self.variable,
-                suffix.extend_from_slice(&other.0);
+                self.suffix_elements().chain(other.elements()),
-                TupleSpec::Variable(VariableLengthTupleSpec {
+            ),
-                    prefix: self.prefix.clone(),
-                    variable: self.variable,
-                    suffix,
-                })
-            }
 
             TupleSpec::Variable(other) => {
                 let variable = UnionType::from_elements(
                     db,
-                    (self.suffix.iter().copied())
+                    self.suffix_elements()
                         .chain([self.variable, other.variable])
-                        .chain(other.prefix.iter().copied()),
+                        .chain(other.prefix_elements()),
                 );
-                TupleSpec::Variable(VariableLengthTupleSpec {
+                VariableLengthTupleSpec::mixed(
-                    prefix: self.prefix.clone(),
+                    self.prefix_elements(),
                     variable,
-                    suffix: other.suffix.clone(),
+                    other.suffix_elements(),
-                })
+                )
             }
         }
     }
@@ -441,44 +488,38 @@ impl<'db> VariableLengthTupleSpec<'db> {
     }
 
     #[must_use]
-    fn normalized(&self, db: &'db dyn Db) -> Self {
+    fn normalized(&self, db: &'db dyn Db) -> TupleSpec<'db> {
-        Self {
+        Self::mixed(
-            prefix: self.prefix.iter().map(|ty| ty.normalized(db)).collect(),
+            self.prenormalized_prefix_elements(db, None)
-            variable: self.variable.normalized(db),
+                .map(|ty| ty.normalized(db)),
-            suffix: self.suffix.iter().map(|ty| ty.normalized(db)).collect(),
+            self.variable.normalized(db),
-        }
+            self.prenormalized_suffix_elements(db, None)
+                .map(|ty| ty.normalized(db)),
+        )
     }
 
-    fn materialize(&self, db: &'db dyn Db, variance: TypeVarVariance) -> Self {
+    fn materialize(&self, db: &'db dyn Db, variance: TypeVarVariance) -> TupleSpec<'db> {
-        Self {
+        Self::mixed(
-            prefix: self
+            self.prefix.iter().map(|ty| ty.materialize(db, variance)),
-                .prefix
+            self.variable.materialize(db, variance),
-                .iter()
+            self.suffix.iter().map(|ty| ty.materialize(db, variance)),
-                .map(|ty| ty.materialize(db, variance))
+        )
-                .collect(),
-            variable: self.variable.materialize(db, variance),
-            suffix: self
-                .suffix
-                .iter()
-                .map(|ty| ty.materialize(db, variance))
-                .collect(),
-        }
     }
 
-    fn apply_type_mapping<'a>(&self, db: &'db dyn Db, type_mapping: &TypeMapping<'a, 'db>) -> Self {
+    fn apply_type_mapping<'a>(
-        Self {
+        &self,
-            prefix: self
+        db: &'db dyn Db,
-                .prefix
+        type_mapping: &TypeMapping<'a, 'db>,
+    ) -> TupleSpec<'db> {
+        Self::mixed(
+            self.prefix
                 .iter()
-                .map(|ty| ty.apply_type_mapping(db, type_mapping))
+                .map(|ty| ty.apply_type_mapping(db, type_mapping)),
-                .collect(),
+            self.variable.apply_type_mapping(db, type_mapping),
-            variable: self.variable.apply_type_mapping(db, type_mapping),
+            self.suffix
-            suffix: self
-                .suffix
                 .iter()
-                .map(|ty| ty.apply_type_mapping(db, type_mapping))
+                .map(|ty| ty.apply_type_mapping(db, type_mapping)),
-                .collect(),
+        )
-        }
     }
 
     fn find_legacy_typevars(
@@ -521,20 +562,21 @@ impl<'db> VariableLengthTupleSpec<'db> {
                 // In addition, the other tuple must have enough elements to match up with this
                 // tuple's prefix and suffix, and each of those elements must pairwise satisfy the
                 // relation.
-                let mut other_iter = other.0.iter();
+                let mut other_iter = other.elements();
-                for self_ty in &self.prefix {
+                for self_ty in self.prenormalized_prefix_elements(db, None) {
                     let Some(other_ty) = other_iter.next() else {
                         return false;
                     };
-                    if !self_ty.has_relation_to(db, *other_ty, relation) {
+                    if !self_ty.has_relation_to(db, other_ty, relation) {
                         return false;
                     }
                 }
-                for self_ty in self.suffix.iter().rev() {
+                let suffix: Vec<_> = self.prenormalized_suffix_elements(db, None).collect();
+                for self_ty in suffix.iter().rev() {
                     let Some(other_ty) = other_iter.next_back() else {
                         return false;
                     };
-                    if !self_ty.has_relation_to(db, *other_ty, relation) {
+                    if !self_ty.has_relation_to(db, other_ty, relation) {
                         return false;
                     }
                 }
@@ -543,33 +585,50 @@ impl<'db> VariableLengthTupleSpec<'db> {
             }
 
             TupleSpec::Variable(other) => {
+                // When prenormalizing below, we assume that a dynamic variable-length portion of
+                // one tuple materializes to the variable-length portion of the other tuple.
+                let self_prenormalize_variable = match self.variable {
+                    Type::Dynamic(_) => Some(other.variable),
+                    _ => None,
+                };
+                let other_prenormalize_variable = match other.variable {
+                    Type::Dynamic(_) => Some(self.variable),
+                    _ => None,
+                };
+
                 // The overlapping parts of the prefixes and suffixes must satisfy the relation.
                 // Any remaining parts must satisfy the relation with the other tuple's
                 // variable-length part.
                 if !self
-                    .prefix
+                    .prenormalized_prefix_elements(db, self_prenormalize_variable)
-                    .iter()
+                    .zip_longest(
-                    .zip_longest(&other.prefix)
+                        other.prenormalized_prefix_elements(db, other_prenormalize_variable),
+                    )
                     .all(|pair| match pair {
                         EitherOrBoth::Both(self_ty, other_ty) => {
-                            self_ty.has_relation_to(db, *other_ty, relation)
+                            self_ty.has_relation_to(db, other_ty, relation)
                         }
                         EitherOrBoth::Left(self_ty) => {
                             self_ty.has_relation_to(db, other.variable, relation)
                         }
-                        EitherOrBoth::Right(other_ty) => {
+                        EitherOrBoth::Right(_) => {
-                            self.variable.has_relation_to(db, *other_ty, relation)
+                            // The rhs has a required element that the lhs is not guaranteed to
+                            // provide.
+                            false
                         }
                     })
                 {
                     return false;
                 }
 
-                if !self
+                let self_suffix: Vec<_> = self
-                    .suffix
+                    .prenormalized_suffix_elements(db, self_prenormalize_variable)
-                    .iter()
+                    .collect();
-                    .rev()
+                let other_suffix: Vec<_> = other
-                    .zip_longest(other.suffix.iter().rev())
+                    .prenormalized_suffix_elements(db, other_prenormalize_variable)
+                    .collect();
+                if !(self_suffix.iter().rev())
+                    .zip_longest(other_suffix.iter().rev())
                     .all(|pair| match pair {
                         EitherOrBoth::Both(self_ty, other_ty) => {
                             self_ty.has_relation_to(db, *other_ty, relation)
@@ -577,8 +636,10 @@ impl<'db> VariableLengthTupleSpec<'db> {
                         EitherOrBoth::Left(self_ty) => {
                             self_ty.has_relation_to(db, other.variable, relation)
                         }
-                        EitherOrBoth::Right(other_ty) => {
+                        EitherOrBoth::Right(_) => {
-                            self.variable.has_relation_to(db, *other_ty, relation)
+                            // The rhs has a required element that the lhs is not guaranteed to
+                            // provide.
+                            false
                         }
                     })
                 {
@@ -592,33 +653,45 @@ impl<'db> VariableLengthTupleSpec<'db> {
     }
 
     fn is_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        self.prefix.len() == other.prefix.len()
+        self.variable.is_equivalent_to(db, other.variable)
-            && self.suffix.len() == other.suffix.len()
+            && (self.prenormalized_prefix_elements(db, None))
-            && self.variable.is_equivalent_to(db, other.variable)
+                .zip_longest(other.prenormalized_prefix_elements(db, None))
-            && (self.prefix.iter())
+                .all(|pair| match pair {
-                .zip(&other.prefix)
+                    EitherOrBoth::Both(self_ty, other_ty) => self_ty.is_equivalent_to(db, other_ty),
-                .all(|(self_ty, other_ty)| self_ty.is_equivalent_to(db, *other_ty))
+                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
-            && (self.suffix.iter())
+                })
-                .zip(&other.suffix)
+            && (self.prenormalized_suffix_elements(db, None))
-                .all(|(self_ty, other_ty)| self_ty.is_equivalent_to(db, *other_ty))
+                .zip_longest(other.prenormalized_suffix_elements(db, None))
+                .all(|pair| match pair {
+                    EitherOrBoth::Both(self_ty, other_ty) => self_ty.is_equivalent_to(db, other_ty),
+                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
+                })
     }
 
     fn is_gradual_equivalent_to(&self, db: &'db dyn Db, other: &Self) -> bool {
-        self.prefix.len() == other.prefix.len()
+        self.variable.is_gradual_equivalent_to(db, other.variable)
-            && self.suffix.len() == other.suffix.len()
+            && (self.prenormalized_prefix_elements(db, None))
-            && self.variable.is_gradual_equivalent_to(db, other.variable)
+                .zip_longest(other.prenormalized_prefix_elements(db, None))
-            && (self.prefix.iter())
+                .all(|pair| match pair {
-                .zip(&other.prefix)
+                    EitherOrBoth::Both(self_ty, other_ty) => {
-                .all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
+                        self_ty.is_gradual_equivalent_to(db, other_ty)
-            && (self.suffix.iter())
+                    }
-                .zip(&other.suffix)
+                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
-                .all(|(self_ty, other_ty)| self_ty.is_gradual_equivalent_to(db, *other_ty))
+                })
+            && (self.prenormalized_suffix_elements(db, None))
+                .zip_longest(other.prenormalized_suffix_elements(db, None))
+                .all(|pair| match pair {
+                    EitherOrBoth::Both(self_ty, other_ty) => {
+                        self_ty.is_gradual_equivalent_to(db, other_ty)
+                    }
+                    EitherOrBoth::Left(_) | EitherOrBoth::Right(_) => false,
+                })
     }
 
     fn is_fully_static(&self, db: &'db dyn Db) -> bool {
         self.variable.is_fully_static(db)
-            && self.prefix.iter().all(|ty| ty.is_fully_static(db))
+            && self.prefix_elements().all(|ty| ty.is_fully_static(db))
-            && self.suffix.iter().all(|ty| ty.is_fully_static(db))
+            && self.suffix_elements().all(|ty| ty.is_fully_static(db))
     }
 }
 
@@ -640,7 +713,7 @@ impl<'db> PyIndex<'db> for &VariableLengthTupleSpec<'db> {
                 Ok(UnionType::from_elements(
                     db,
                     std::iter::once(self.variable)
-                        .chain(self.suffix.iter().copied().take(index_past_prefix)),
+                        .chain(self.suffix_elements().take(index_past_prefix)),
                 ))
             }
 
@@ -656,7 +729,7 @@ impl<'db> PyIndex<'db> for &VariableLengthTupleSpec<'db> {
                 let index_past_suffix = index_from_end - self.suffix.len() + 1;
                 Ok(UnionType::from_elements(
                     db,
-                    (self.prefix.iter().rev().copied())
+                    (self.prefix_elements().rev())
                         .take(index_past_suffix)
                         .rev()
                         .chain(std::iter::once(self.variable)),
@@ -683,7 +756,7 @@ impl<'db> TupleSpec<'db> {
     }
 
     pub(crate) fn homogeneous(element: Type<'db>) -> Self {
-        TupleSpec::from(VariableLengthTupleSpec::homogeneous(element))
+        VariableLengthTupleSpec::homogeneous(element)
     }
 
     /// Returns an iterator of all of the fixed-length element types of this tuple.
@@ -751,23 +824,21 @@ impl<'db> TupleSpec<'db> {
     fn normalized(&self, db: &'db dyn Db) -> Self {
         match self {
             TupleSpec::Fixed(tuple) => TupleSpec::Fixed(tuple.normalized(db)),
-            TupleSpec::Variable(tuple) => TupleSpec::Variable(tuple.normalized(db)),
+            TupleSpec::Variable(tuple) => tuple.normalized(db),
         }
     }
 
     fn materialize(&self, db: &'db dyn Db, variance: TypeVarVariance) -> Self {
         match self {
             TupleSpec::Fixed(tuple) => TupleSpec::Fixed(tuple.materialize(db, variance)),
-            TupleSpec::Variable(tuple) => TupleSpec::Variable(tuple.materialize(db, variance)),
+            TupleSpec::Variable(tuple) => tuple.materialize(db, variance),
         }
     }
 
     fn apply_type_mapping<'a>(&self, db: &'db dyn Db, type_mapping: &TypeMapping<'a, 'db>) -> Self {
         match self {
             TupleSpec::Fixed(tuple) => TupleSpec::Fixed(tuple.apply_type_mapping(db, type_mapping)),
-            TupleSpec::Variable(tuple) => {
+            TupleSpec::Variable(tuple) => tuple.apply_type_mapping(db, type_mapping),
-                TupleSpec::Variable(tuple.apply_type_mapping(db, type_mapping))
-            }
         }
     }
 
@@ -816,20 +887,67 @@ impl<'db> TupleSpec<'db> {
     }
 
     fn is_disjoint_from(&self, db: &'db dyn Db, other: &Self) -> bool {
+        // Two tuples with an incompatible number of required elements must always be disjoint.
+        let (self_min, self_max) = self.size_hint();
+        let (other_min, other_max) = other.size_hint();
+        if self_max.is_some_and(|max| max < other_min) {
+            return true;
+        }
+        if other_max.is_some_and(|max| max < self_min) {
+            return true;
+        }
+
+        // If any of the required elements are pairwise disjoint, the tuples are disjoint as well.
+        #[allow(clippy::items_after_statements)]
+        fn any_disjoint<'db>(
+            db: &'db dyn Db,
+            a: impl IntoIterator<Item = Type<'db>>,
+            b: impl IntoIterator<Item = Type<'db>>,
+        ) -> bool {
+            a.into_iter().zip(b).any(|(self_element, other_element)| {
+                self_element.is_disjoint_from(db, other_element)
+            })
+        }
+
         match (self, other) {
             (TupleSpec::Fixed(self_tuple), TupleSpec::Fixed(other_tuple)) => {
-                self_tuple.is_disjoint_from(db, other_tuple)
+                if any_disjoint(db, self_tuple.elements(), other_tuple.elements()) {
+                    return true;
+                }
+            }
+
+            (TupleSpec::Variable(self_tuple), TupleSpec::Variable(other_tuple)) => {
+                if any_disjoint(
+                    db,
+                    self_tuple.prefix_elements(),
+                    other_tuple.prefix_elements(),
+                ) {
+                    return true;
+                }
+                if any_disjoint(
+                    db,
+                    self_tuple.suffix_elements().rev(),
+                    other_tuple.suffix_elements().rev(),
+                ) {
+                    return true;
+                }
+            }
+
+            (TupleSpec::Fixed(fixed), TupleSpec::Variable(variable))
+            | (TupleSpec::Variable(variable), TupleSpec::Fixed(fixed)) => {
+                if any_disjoint(db, fixed.elements(), variable.prefix_elements()) {
+                    return true;
+                }
+                if any_disjoint(db, fixed.elements().rev(), variable.suffix_elements().rev()) {
+                    return true;
+                }
             }
-            // Two pure homogeneous tuples `tuple[A, ...]` and `tuple[B, ...]` can never be
-            // disjoint even if A and B are disjoint, because `tuple[()]` would be assignable to
-            // both.
-            // TODO: Consider checking for disjointness between the tuples' prefixes and suffixes.
-            (TupleSpec::Variable(_), TupleSpec::Variable(_)) => false,
-            // TODO: Consider checking for disjointness between the fixed-length tuple and the
-            // variable-length tuple's prefix/suffix.
-            (TupleSpec::Fixed(_), TupleSpec::Variable(_))
-            | (TupleSpec::Variable(_), TupleSpec::Fixed(_)) => false,
         }
+
+        // Two pure homogeneous tuples `tuple[A, ...]` and `tuple[B, ...]` can never be
+        // disjoint even if A and B are disjoint, because `tuple[()]` would be assignable to
+        // both.
+        false
     }
 
     fn is_fully_static(&self, db: &'db dyn Db) -> bool {