[ty] Clarify behavior of constraint sets for gradual upper bounds and constraints

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

@@ -141,6 +141,116 @@ def bounded[T: Base]():
     static_assert(not constraints.satisfied_by_all_typevars())
 ```
 
+If the upper bound is a gradual type, we are free to choose any materialization of the upper bound
+that makes the test succeed. In non-inferable positions, it is most helpful to choose an upper bound
+that is as restrictive as possible, since that minimizes the number of valid specializations that
+must satisfy the constraint set. (That means we will almost always choose `Never` — or more
+precisely, the bottom specialization — as the upper bound.) In inferable positions, the opposite is
+true: it is most helpful to choose an upper bound that is as permissive as possible, since that
+maximizes the number of valid specializations that might satisfy the constraint set.
+
+```py
+from typing import Any
+
+def bounded_by_gradual[T: Any]():
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars())
+
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
+
+    # If we choose Super as the materialization, then (T = Super) is a valid specialization, which
+    # satisfies (T ≤ Super).
+    static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Never) is the only valid specialization,
+    # which satisfies (T ≤ Super).
+    static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars())
+
+    # If we choose Base as the materialization, then (T = Base) is a valid specialization, which
+    # satisfies (T ≤ Base).
+    static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Never) is the only valid specialization,
+    # which satisfies (T ≤ Base).
+    static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars())
+
+    # If we choose Sub as the materialization, then (T = Sub) is a valid specialization, which
+    # satisfies (T ≤ Sub).
+    static_assert(ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Never) is the only valid specialization,
+    # which satisfies (T ≤ Sub).
+    static_assert(ConstraintSet.range(Never, T, Sub).satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = Unrelated) is a valid specialization,
+    # which satisfies (T ≤ Unrelated).
+    constraints = ConstraintSet.range(Never, T, Unrelated)
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Never) is the only valid specialization,
+    # which satisfies (T ≤ Unrelated).
+    static_assert(constraints.satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = Unrelated) is a valid specialization,
+    # which satisfies (T ≤ Unrelated ∧ T ≠ Never).
+    constraints = constraints & ~ConstraintSet.range(Never, T, Never)
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # There is no upper bound that we can choose to satisfy this constraint set in non-inferable
+    # position. (T = Never) will be a valid assignment no matter what, and that does not satisfy
+    # (T ≤ Unrelated ∧ T ≠ Never).
+    static_assert(not constraints.satisfied_by_all_typevars())
+```
+
+When the upper bound is a more complex gradual type, we are still free to choose any materialization
+that causes the check to succeed, and we will still choose a restrictive materialization in
+non-inferable position, and a permissive materialization in inferable position. The variance of the
+typevar does not affect whether there is a materialization we can choose. Below, we test the most
+restrictive variance (i.e., invariance), but we get the same results for other variances as well.
+
+```py
+def bounded_by_gradual[T: list[Any]]():
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars())
+
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
+
+    # If we choose Super as the materialization, then (T = list[Super]) is a valid specialization,
+    # which satisfies (T ≤ list[Super]).
+    static_assert(ConstraintSet.range(Never, T, list[Super]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Super as the materialization, then all valid specializations must satisfy
+    # (T ≤ list[Super]).
+    static_assert(ConstraintSet.range(Never, T, list[Super]).satisfied_by_all_typevars())
+
+    # If we choose Base as the materialization, then (T = list[Base]) is a valid specialization,
+    # which satisfies (T ≤ list[Base]).
+    static_assert(ConstraintSet.range(Never, T, list[Base]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Base as the materialization, then all valid specializations must satisfy
+    # (T ≤ list[Base]).
+    static_assert(ConstraintSet.range(Never, T, list[Base]).satisfied_by_all_typevars())
+
+    # If we choose Sub as the materialization, then (T = list[Sub]) is a valid specialization, which
+    # satisfies (T ≤ list[Sub]).
+    static_assert(ConstraintSet.range(Never, T, list[Sub]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Sub as the materialization, then all valid specializations must satisfy
+    # (T ≤ list[Sub]).
+    static_assert(ConstraintSet.range(Never, T, list[Sub]).satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = list[Unrelated]) is a valid
+    # specialization, which satisfies (T ≤ list[Unrelated]).
+    constraints = ConstraintSet.range(Never, T, list[Unrelated])
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Unrelated as the materialization, then all valid specializations must satisfy
+    # (T ≤ list[Unrelated]).
+    static_assert(constraints.satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = list[Unrelated]) is a valid
+    # specialization, which satisfies (T ≤ list[Unrelated] ∧ T ≠ Never).
+    constraints = constraints & ~ConstraintSet.range(Never, T, Never)
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # There is no upper bound that we can choose to satisfy this constraint set in non-inferable
+    # position. (T = Never) will be a valid assignment no matter what, and that does not satisfy
+    # (T ≤ list[Unrelated] ∧ T ≠ Never).
+    static_assert(not constraints.satisfied_by_all_typevars())
+```
+
 ## Constrained typevar
 
 If a typevar has constraints, then it must specialize to one of those specific types. (Not to a
@@ -218,3 +328,96 @@ def constrained[T: (Base, Unrelated)]():
     # (T = Base) is a valid specialization, which does not satisfy (T = Sub ∨ T = Unrelated).
     static_assert(not constraints.satisfied_by_all_typevars())
 ```
+
+If one of the constraints is a gradual type, we are free to choose any materialization of the
+constraint that makes the test succeed. In non-inferable positions, it is most helpful to choose a
+constraint that is as restrictive as possible, since that minimizes the number of valid
+specializations that must satisfy the constraint set. (That means we will almost always choose
+`Never` — or more precisely, the bottom specialization — as the constraint.) In inferable positions,
+the opposite is true: it is most helpful to choose a constraint that is as permissive as possible,
+since that maximizes the number of valid specializations that might satisfy the constraint set.
+
+```py
+from typing import Any
+
+def constrained_by_gradual[T: (Base, Any)]():
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars())
+
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = Unrelated) is a valid specialization,
+    # which satisfies (T ≤ Unrelated).
+    static_assert(ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars(inferable=tuple[T]))
+    # No matter which materialization we choose, (T = Base) is a valid specialization, which does
+    # not satisfy (T ≤ Unrelated).
+    static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars())
+
+    # If we choose Super as the materialization, then (T = Super) is a valid specialization, which
+    # satisfies (T ≤ Super).
+    static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Base) and (T = Never) are the only valid
+    # specializations, both of which satisfy (T ≤ Super).
+    static_assert(ConstraintSet.range(Never, T, Super).satisfied_by_all_typevars())
+
+    # If we choose Base as the materialization, then (T = Base) is a valid specialization, which
+    # satisfies (T ≤ Base).
+    static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Never as the materialization, then (T = Base) and (T = Never) are the only valid
+    # specializations, both of which satisfy (T ≤ Base).
+    static_assert(ConstraintSet.range(Never, T, Base).satisfied_by_all_typevars())
+```
+
+When the constraint is a more complex gradual type, we are still free to choose any materialization
+that causes the check to succeed, and we will still choose a restrictive materialization in
+non-inferable position, and a permissive materialization in inferable position. The variance of the
+typevar does not affect whether there is a materialization we can choose. Below, we test the most
+restrictive variance (i.e., invariance), but we get the same results for other variances as well.
+
+```py
+def constrained_by_gradual[T: (list[Base], list[Any])]():
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(ConstraintSet.always().satisfied_by_all_typevars())
+
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.never().satisfied_by_all_typevars())
+
+    # If we choose Super as the materialization, then (T = list[Super]) is a valid specialization,
+    # which satisfies (T ≤ list[Super]).
+    static_assert(ConstraintSet.range(Never, T, list[Super]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # No matter which materialization we choose, (T = list[Base]) is a valid specialization, which
+    # does not satisfy (T ≤ list[Super]).
+    static_assert(not ConstraintSet.range(Never, T, list[Super]).satisfied_by_all_typevars())
+
+    # If we choose Base as the materialization, then (T = list[Base]) is a valid specialization,
+    # which satisfies (T ≤ list[Base]).
+    static_assert(ConstraintSet.range(Never, T, list[Base]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Base as the materialization, then all valid specializations must satisfy
+    # (T ≤ list[Base]).
+    static_assert(ConstraintSet.range(Never, T, list[Base]).satisfied_by_all_typevars())
+
+    # If we choose Sub as the materialization, then (T = list[Sub]) is a valid specialization, which
+    # satisfies (T ≤ list[Sub]).
+    static_assert(ConstraintSet.range(Never, T, list[Sub]).satisfied_by_all_typevars(inferable=tuple[T]))
+    # No matter which materialization we choose, (T = list[Base]) is a valid specialization, which
+    # does not satisfy (T ≤ list[Sub]).
+    static_assert(not ConstraintSet.range(Never, T, list[Sub]).satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = list[Unrelated]) is a valid
+    # specialization, which satisfies (T ≤ list[Unrelated]).
+    constraints = ConstraintSet.range(Never, T, list[Unrelated])
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # No matter which materialization we choose, (T = list[Base]) is a valid specialization, which
+    # does not satisfy (T ≤ list[Unrelated]).
+    static_assert(not constraints.satisfied_by_all_typevars())
+
+    # If we choose Unrelated as the materialization, then (T = list[Unrelated]) is a valid
+    # specialization, which satisfies (T ≤ list[Unrelated] ∧ T ≠ Never).
+    constraints = constraints & ~ConstraintSet.range(Never, T, Never)
+    static_assert(constraints.satisfied_by_all_typevars(inferable=tuple[T]))
+    # There is no constraint that we can choose to satisfy this constraint set in non-inferable
+    # position. (T = Never) will be a valid assignment no matter what, and that does not satisfy
+    # (T ≤ list[Unrelated] ∧ T ≠ Never).
+    static_assert(not constraints.satisfied_by_all_typevars())
+```

crates/ty_python_semantic/src/types/constraints.rs

@@ -871,7 +871,7 @@ impl<'db> Node<'db> {
 
         for typevar in typevars {
             // Determine which valid specializations of this typevar satisfy the constraint set.
-            let valid_specializations = typevar.valid_specializations(db).node;
+            let valid_specializations = typevar.valid_specializations(db, inferable).node;
             let when_satisfied = valid_specializations
                 .satisfies(db, self)
                 .and(db, valid_specializations);
@@ -1984,25 +1984,32 @@ impl<'db> SatisfiedClauses<'db> {
 
 /// Returns a constraint set describing the valid specializations of a typevar.
 impl<'db> BoundTypeVarInstance<'db> {
-    pub(crate) fn valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> {
+    pub(crate) fn valid_specializations(
+        self,
+        db: &'db dyn Db,
+        inferable: InferableTypeVars<'_, 'db>,
+    ) -> ConstraintSet<'db> {
+        // For upper bounds and constraints, we are free to choose any materialization that makes
+        // the check succeed. In non-inferable positions, it is most helpful to choose a
+        // materialization that is as restrictive as possible, since that minimizes the number of
+        // valid specializations that must satisfy the check. In inferable positions, the opposite
+        // is true: it is most helpful to choose a materialization that is as permissive as
+        // possible, since that maximizes the number of valid specializations that might satisfy
+        // the check.
+        let relation = if self.is_inferable(db, inferable) {
+            TypeRelation::Assignability
+        } else {
+            TypeRelation::Subtyping
+        };
+
         match self.typevar(db).bound_or_constraints(db) {
             None => ConstraintSet::from(true),
-            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => ConstraintSet::constrain_typevar(
-                db,
-                self,
-                Type::Never,
-                bound,
-                TypeRelation::Assignability,
-            ),
+            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                ConstraintSet::constrain_typevar(db, self, Type::Never, bound, relation)
+            }
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
                 constraints.elements(db).iter().when_any(db, |constraint| {
-                    ConstraintSet::constrain_typevar(
-                        db,
-                        self,
-                        *constraint,
-                        *constraint,
-                        TypeRelation::Assignability,
-                    )
+                    ConstraintSet::constrain_typevar(db, self, *constraint, *constraint, relation)
                 })
             }
         }