[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 #18600 (comment)

---------

Co-authored-by: Alex Waygood <[email protected]>

Author: dcreager

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
-`Q1` or if `P2` is disjoint from `Q2`:
+```toml
+[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]))
+```
+
+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
+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]
+python-version = "3.11"
+```
+
+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`, even if all elements are falsy:
+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, Literal
+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,27 +275,36 @@ 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::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(),
             ),
-            3 => Ty::Intersection {
+            4 => Ty::Intersection {
                 pos: (0..*g.choose(&[0, 1, 2]).unwrap())
                     .map(|_| arbitrary_type(g, size - 1))
                     .collect(),
                 neg: (0..*g.choose(&[0, 1, 2]).unwrap())
                     .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() {
-                0 => None,
-                1 => Some(elts.into_iter().next().unwrap()),
-                _ => Some(Ty::Tuple(elts)),
-            })),
+            Ty::FixedLengthTuple(types) => {
+                Box::new(types.shrink().filter_map(|elts| match elts.len() {
+                    0 => None,
+                    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!
                 //