[ty] Restrict range implications from gradual equivalence (astral-sh#29577)

Fix false `invalid-argument-type` errors when inferring constrained type
variables from callbacks that return an invariant generic with a gradual
type argument. A callback returning `Box[Any]` can satisfy `Callable[[],
T | Box[T]]` when `T` is constrained to `str` or `bytes`.

The solver treated equivalence to a gradual type as exact substitution,
allowing a valid union alternative to imply an incompatible bound.
Require a static equivalence bound before deriving either lower- or
upper-bound implications, including when gradual types are nested inside
a bound.

Prerequisite to avoid regressions in astral-sh#29236.

Author: carljm

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

@@ -2102,6 +2102,44 @@ reveal_type(infer_any_bound(list[str]()))  # revealed: str
 reveal_type(infer_list_bound(list[list[str]]()))  # revealed: list[str]
 ```
 
+## Gradual specializations in callable union returns
+
+A callable's return type only needs to match one member of an expected union, even when the match
+relies on a gradual type argument. If several declared constraints remain possible, inference
+preserves the gradual type argument.
+
+```py
+from typing import Any, Callable, Generic, TypeVar
+
+T = TypeVar("T", str, bytes)
+
+class Box(Generic[T]):
+    value: T
+
+def infer(callback: Callable[[], T | Box[T]]) -> T:
+    raise NotImplementedError
+
+unknown = Box()
+any_ = Box[Any]()
+
+unknown_result = infer(lambda: unknown)  # no diagnostic
+reveal_type(unknown_result)  # revealed: Unknown
+any_result = infer(lambda: any_)  # no diagnostic
+reveal_type(any_result)  # revealed: Any
+```
+
+Other arguments must still satisfy the type variable's declared constraints. Gradual evidence from a
+callback does not make an incompatible argument valid:
+
+```py
+def consume(callback: Callable[[], Box[T]], other: T) -> None: ...
+
+# The callback returns a box, as required by `Box[T]`. The second argument must instead
+# be `str` or `bytes`, but is also a box: only its type argument is gradual.
+consume(lambda: unknown, unknown)  # error: [invalid-argument-type] "does not satisfy constraints"
+consume(lambda: any_, any_)  # error: [invalid-argument-type] "does not satisfy constraints"
+```
+
 ## Invalid bounds in generic union members
 
 An argument that violates a type variable's bound is rejected even when another union member is not

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

@@ -3764,6 +3764,42 @@ reveal_type(infer_any_bound(list[str]()))  # revealed: str
 reveal_type(infer_list_bound(list[list[str]]()))  # revealed: list[str]
 ```
 
+## Gradual specializations in callable union returns
+
+A callable's return type only needs to match one member of an expected union, even when the match
+relies on a gradual type argument. If several declared constraints remain possible, inference
+preserves the gradual type argument.
+
+```py
+from typing import Any, Callable
+
+class Box[T: (str, bytes)]:
+    value: T
+
+def infer[T: (str, bytes)](callback: Callable[[], T | Box[T]]) -> T:
+    raise NotImplementedError
+
+unknown = Box()
+any_ = Box[Any]()
+
+unknown_result = infer(lambda: unknown)  # no diagnostic
+reveal_type(unknown_result)  # revealed: Unknown
+any_result = infer(lambda: any_)  # no diagnostic
+reveal_type(any_result)  # revealed: Any
+```
+
+Other arguments must still satisfy the type variable's declared constraints. Gradual evidence from a
+callback does not make an incompatible argument valid:
+
+```py
+def consume[T: (str, bytes)](callback: Callable[[], Box[T]], other: T) -> None: ...
+
+# The callback returns a box, as required by `Box[T]`. The second argument must instead
+# be `str` or `bytes`, but is also a box: only its type argument is gradual.
+consume(lambda: unknown, unknown)  # error: [invalid-argument-type] "does not satisfy constraints"
+consume(lambda: any_, any_)  # error: [invalid-argument-type] "does not satisfy constraints"
+```
+
 ## Invalid bounds in generic union members
 
 An argument that violates a type variable's bound is rejected even when another union member is not

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

@@ -747,7 +747,8 @@ def lower_bound[T, U]():
 ### Substituting gradual equivalences into nested bounds
 
 Substituting a gradual equivalence into a lower bound preserves assignability, but does not
-establish subtyping.
+establish subtyping. This also holds for equivalence bounds: separate occurrences of `Any` in a
+subtype comparison can materialize to different types.
 
 ```py
 from typing import Any
@@ -765,8 +766,9 @@ def equivalence_into_lower[T, U]():
 
 def equivalence_into_equality[T, U]():
     constraints = ConstraintSet.equality(T, Any) & ConstraintSet.equality(U, Covariant[T])
-    static_assert(constraints.implies_subtype_of(Covariant[Any], U))
-    static_assert(constraints.implies_subtype_of(U, Covariant[Any]))
+    static_assert(constraints.satisfies(ConstraintSet.equality(U, Covariant[Any])))
+    static_assert(not constraints.implies_subtype_of(Covariant[Any], U))
+    static_assert(not constraints.implies_subtype_of(U, Covariant[Any]))
 ```
 
 ### Gradual range substitutions do not preserve correlation

crates/ty_python_semantic/src/types/constraints.rs

@@ -5703,6 +5703,60 @@ class E: ...
         Ok(())
     }
 
+    #[test]
+    fn gradual_equivalence_preserves_alternative_bounds() {
+        let db = setup_db();
+        let db = &db;
+        let env = db.program_environment();
+        let t = create_typevar(db, "T");
+        let int = known_instance(db, KnownClass::Int);
+        let str = known_instance(db, KnownClass::Str);
+        let list = |ty| KnownClass::List.to_specialized_instance(db, &env, &[ty]);
+
+        for dynamic in [Type::any(), Type::unknown()] {
+            for (gradual, bound, witness) in
+                [(dynamic, int, str), (list(dynamic), list(int), list(str))]
+            {
+                for (lower, upper) in [(Some(bound), None), (None, Some(bound))] {
+                    let builder = ConstraintSetBuilder::new();
+                    let equivalent = ConstraintSet::constrain_typevar_equivalence_bound(
+                        db,
+                        &env,
+                        &builder,
+                        ConstraintProvenance::Evidence,
+                        t,
+                        gradual,
+                    );
+                    let range =
+                        create_constraint_set_with_bounds(db, &env, &builder, t, lower, upper);
+                    let witness = ConstraintSet::constrain_typevar_equivalence_bound(
+                        db,
+                        &env,
+                        &builder,
+                        ConstraintProvenance::Evidence,
+                        t,
+                        witness,
+                    );
+
+                    // `T = Any` permits `T = str`, even though `int ≤ T` (or `T ≤ int`)
+                    // does not. The same holds inside an invariant container.
+                    let alternatives =
+                        equivalent
+                            .or(db, &builder, || range)
+                            .and(db, &builder, || witness);
+                    assert!(!alternatives.is_never_satisfied(db, &env, TypeVarSet::None));
+
+                    // Requiring both bounds still rules out that specialization.
+                    let conjunction =
+                        equivalent
+                            .and(db, &builder, || range)
+                            .and(db, &builder, || witness);
+                    assert!(conjunction.is_never_satisfied(db, &env, TypeVarSet::None));
+                }
+            }
+        }
+    }
+
     #[test]
     fn trivial_satisfaction_only_recognizes_terminals() {
         let db = setup_db();

crates/ty_python_semantic/src/types/constraints/sequents.rs

@@ -1547,9 +1547,12 @@ impl<'db> ConcreteLowerBound<'db> {
         }
 
         // (α ≤ β) ⇒ ((T = β) ⇒ (α ≤ T))
-        if self
-            .bound
-            .is_constraint_set_assignable_to(db, env, other.bound)
+        // This requires a static equivalence bound: `T = Any` permits `T = str`, so
+        // assignability of `int` to `Any` does not imply `int ≤ T`.
+        if other.bound.is_static_sequent_eligible(db, env)
+            && self
+                .bound
+                .is_constraint_set_assignable_to(db, env, other.bound)
         {
             map.add_single_implication(other.into(), self.into());
         }
@@ -1728,14 +1731,17 @@ impl<'db> ConcreteUpperBound<'db> {
         }
 
         // (β ≤ α) ⇒ ((T = β) ⇒ (T ≤ α))
-        if other
-            .bound
-            .is_constraint_set_assignable_to(db, env, self.bound)
+        // This requires a static equivalence bound: `T = Any` permits `T = str`, so
+        // assignability of `Any` to `int` does not imply `T ≤ int`.
+        if other.bound.is_static_sequent_eligible(db, env)
+            && other
+                .bound
+                .is_constraint_set_assignable_to(db, env, self.bound)
         {
             map.add_single_implication(other.into(), self.into());
         }
 
-        // Given constraints `T ≤ α` and `T = β`, `α ≤ β` must also hold. If those bounds contain
+        // Given constraints `T ≤ α` and `T = β`, `β ≤ α` must also hold. If those bounds contain
         // other typevars, we can infer additional constraints.
         AtomicConstraint::add_sequents_for_range(db, env, map, other, self);
     }