[ty] Only consider fully static pivots when deriving transitive constraints (#22444)

When working with constraint sets, we track transitive relationships
between the constraints in the set. For instance, in `S ≤ int ∧ int ≤
T`, we can infer that `S ≤ T`. However, we should only consider fully
static types when looking for a "pivot" for this kind of transitive
relationship. The same pattern does not hold for `S ≤ Any ∧ Any ≤ T`;
because the two `Any`s can materialize to different types, we cannot
infer that `S ≤ T`.

Fixes https://github.com/astral-sh/ty/issues/2371

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

@@ -949,3 +949,29 @@ class Builder(Generic[TMsg]):
     def _handler(self, stream: Stream[Msg]) -> Stream[Msg]:
         return stream
 ```
+
+## Regressions
+
+### Only consider fully static types as pivots for transitivity
+
+This is a regression test for [ty#2371]. When working with constraint sets, we track transitive
+relationships between the constraints in the set. For instance, in `S ≤ int ∧ int ≤ T`, we can infer
+that `S ≤ T`. However, we should only consider fully static types when looking for a "pivot" for
+this kind of transitive relationship. The same pattern does not hold for `S ≤ Any ∧ Any ≤ T`;
+because the two `Any`s can materialize to different types, we cannot infer that `S ≤ T`.
+
+We have lower level tests of this in [`type_properties/implies_subtype_of.md`][implies_subtype_of].
+`functools.reduce` has a signature that exercises this behavior, as well, so we also include this
+regression test.
+
+```py
+from functools import reduce
+
+def _(keys: list[str]):
+    # TODO: revealed: int
+    # revealed: Unknown | Literal[0]
+    reveal_type(reduce(lambda total, k: total + len(k), keys, 0))
+```
+
+[implies_subtype_of]: ../../type_properties/implies_subtype_of.md
+[ty#2371]: https://github.com/astral-sh/ty/issues/2371

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

@@ -537,4 +537,43 @@ def identity2[T](t: T) -> T:
     return t
 ```
 
+## Transitivity
+
+### Transitivity can propagate across typevars
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+def concrete_pivot[T, U]():
+    # If [int ≤ T ∧ T ≤ U], then [int ≤ U] must be true as well.
+    constraints = ConstraintSet.range(int, T, object) & ConstraintSet.range(T, U, object)
+    static_assert(constraints.implies_subtype_of(int, U))
+```
+
+### Transitivity can propagate across fully static concrete types
+
+```py
+from typing import Never
+from ty_extensions import ConstraintSet, static_assert
+
+def concrete_pivot[T, U]():
+    # If [T ≤ int ∧ int ≤ U], then [T ≤ U] must be true as well.
+    constraints = ConstraintSet.range(Never, T, int) & ConstraintSet.range(int, U, object)
+    static_assert(constraints.implies_subtype_of(T, U))
+```
+
+### Transitivity cannot propagate across non-fully-static concrete types
+
+```py
+from typing import Any, Never
+from ty_extensions import ConstraintSet, static_assert
+
+def concrete_pivot[T, U]():
+    # If [T ≤ Any ∧ Any ≤ U], then the two `Any`s might materialize to different types. That means
+    # [T ≤ U] is NOT necessarily true.
+    constraints = ConstraintSet.range(Never, T, Any) & ConstraintSet.range(Any, U, object)
+    static_assert(not constraints.implies_subtype_of(T, U))
+```
+
 [subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence

crates/ty_python_semantic/src/types/constraints.rs

@@ -3094,18 +3094,29 @@ impl<'db> SequentMap<'db> {
 
             // (CL ≤ C ≤ pivot) ∧ (pivot ≤ B ≤ BU) → (CL ≤ C ≤ B)
             (constrained_lower, constrained_upper)
-                if constrained_upper == bound_constraint.lower(db)
-                    && !constrained_upper.is_never()
-                    && !constrained_upper.is_object() =>
+                if !constrained_upper.is_never()
+                    && !constrained_upper.is_object()
+                    && constrained_upper
+                        .top_materialization(db)
+                        .is_constraint_set_assignable_to(
+                            db,
+                            bound_constraint.lower(db).bottom_materialization(db),
+                        ) =>
             {
                 (constrained_lower, Type::TypeVar(bound_typevar))
             }
 
             // (pivot ≤ C ≤ CU) ∧ (BL ≤ B ≤ pivot) → (B ≤ C ≤ CU)
             (constrained_lower, constrained_upper)
-                if constrained_lower == bound_constraint.upper(db)
-                    && !constrained_lower.is_never()
-                    && !constrained_lower.is_object() =>
+                if !constrained_lower.is_never()
+                    && !constrained_lower.is_object()
+                    && bound_constraint
+                        .upper(db)
+                        .top_materialization(db)
+                        .is_constraint_set_assignable_to(
+                            db,
+                            constrained_lower.bottom_materialization(db),
+                        ) =>
             {
                 (Type::TypeVar(bound_typevar), constrained_upper)
             }