diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/satisfied_by_all_typevars.md b/crates/ty_python_semantic/resources/mdtest/type_properties/satisfied_by_all_typevars.md
index 8d9f56325093b..678ca9e45f3ce 100644
--- a/crates/ty_python_semantic/resources/mdtest/type_properties/satisfied_by_all_typevars.md
+++ b/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 the bottom
+materialization as the upper bound. That is the most restrictive possible choice, which minimizes
+the number of valid specializations that must satisfy the constraint set. In inferable positions,
+the opposite is true: it is most helpful to choose the top materialization. That is the most
+permissive possible choice, which 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 the bottom materialization in
+non-inferable position, and the top 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,188 @@ 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 any of the constraints is a gradual type, we are free to choose any materialization of that
+constraint that makes the test succeed. In non-inferable positions, it is most helpful to choose the
+bottom materialization as the constraint. That is the most restrictive possible choice, which
+minimizes the number of valid specializations that must satisfy the constraint set. In inferable
+positions, the opposite is true: it is most helpful to choose the top materialization. That is the
+most permissive possible choice, which 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())
+
+def constrained_by_two_gradual[T: (Any, 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]))
+    # If we choose Unrelated as the materialization, then (T = Unrelated) is the only valid
+    # specialization, which satisfies (T ≤ Unrelated).
+    static_assert(ConstraintSet.range(Never, T, Unrelated).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, Any).satisfied_by_all_typevars(inferable=tuple[T]))
+    # If we choose Unrelated as the materialization, then (T = Unrelated) is the only valid
+    # specialization, which satisfies (T ≤ Unrelated).
+    static_assert(ConstraintSet.range(Never, T, Any).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 a 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 the bottom materialization in
+non-inferable position, and the top 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())
+
+    # No matter which materialization we choose, every valid specialization will be of the form
+    # (T = list[X]). Because Unrelated is final, it is disjoint from all lists. There is therefore
+    # no materialization or specialization that satisfies (T ≤ Unrelated).
+    static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.range(Never, T, Unrelated).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())
+
+def constrained_by_two_gradual[T: (list[Any], 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())
+
+    # No matter which materialization we choose, every valid specialization will be of the form
+    # (T = list[X]). Because Unrelated is final, it is disjoint from all lists. There is therefore
+    # no materialization or specialization that satisfies (T ≤ Unrelated).
+    static_assert(not ConstraintSet.range(Never, T, Unrelated).satisfied_by_all_typevars(inferable=tuple[T]))
+    static_assert(not ConstraintSet.range(Never, T, Unrelated).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(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(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(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(constraints.satisfied_by_all_typevars())
+```
diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs
index c1e5ac269779c..d2520deb083ba 100644
--- a/crates/ty_python_semantic/src/types/constraints.rs
+++ b/crates/ty_python_semantic/src/types/constraints.rs
@@ -869,25 +869,56 @@ impl<'db> Node<'db> {
             typevars.insert(constraint.typevar(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 when_satisfied = valid_specializations
+        // Returns if some specialization satisfies this constraint set.
+        let some_specialization_satisfies = move |specializations: Node<'db>| {
+            let when_satisfied = specializations
                 .satisfies(db, self)
-                .and(db, valid_specializations);
-            let satisfied = if typevar.is_inferable(db, inferable) {
-                // If the typevar is inferable, then we only need one valid specialization to
-                // satisfy the constraint set.
-                !when_satisfied.is_never_satisfied()
+                .and(db, specializations)
+                .simplify(db);
+            !when_satisfied.is_never_satisfied()
+        };
+
+        // Returns if all specializations satisfy this constraint set.
+        let all_specializations_satisfy = move |specializations: Node<'db>| {
+            let when_satisfied = specializations
+                .satisfies(db, self)
+                .and(db, specializations)
+                .simplify(db);
+            when_satisfied
+                .iff(db, specializations)
+                .is_always_satisfied(db)
+        };
+
+        for typevar in typevars {
+            if typevar.is_inferable(db, inferable) {
+                // If the typevar is in inferable position, we need to verify that some valid
+                // specialization satisfies the constraint set.
+                let valid_specializations = typevar.valid_specializations(db);
+                if !some_specialization_satisfies(valid_specializations) {
+                    return false;
+                }
             } else {
-                // If the typevar is non-inferable, then we need _all_ valid specializations to
-                // satisfy the constraint set.
-                when_satisfied
-                    .iff(db, valid_specializations)
-                    .is_always_satisfied(db)
-            };
-            if !satisfied {
-                return false;
+                // If the typevar is in non-inferable position, we need to verify that all required
+                // specializations satisfy the constraint set. Complicating things, the typevar
+                // might have gradual constraints. For those, we need to know the range of valid
+                // materializations, but we only need some materialization to satisfy the
+                // constraint set.
+                //
+                // NB: We could also model this by introducing a synthetic typevar for the gradual
+                // constraint, treating that synthetic typevar as always inferable (so that we only
+                // need to verify for some materialization), and then update this typevar's
+                // constraint to refer to the synthetic typevar instead of the original gradual
+                // constraint.
+                let (static_specializations, gradual_constraints) =
+                    typevar.required_specializations(db);
+                if !all_specializations_satisfy(static_specializations) {
+                    return false;
+                }
+                for gradual_constraint in gradual_constraints {
+                    if !some_specialization_satisfies(gradual_constraint) {
+                        return false;
+                    }
+                }
             }
         }
 
@@ -1982,28 +2013,88 @@ 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> {
+    /// Returns the valid specializations of a typevar. This is used when checking a constraint set
+    /// when this typevar is in inferable position, where we only need _some_ specialization to
+    /// satisfy the constraint set.
+    fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> {
+        // For gradual upper bounds and constraints, we are free to choose any materialization that
+        // makes the check succeed. In inferable positions, 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. We therefore take the top
+        // materialization of the bound or constraints.
+        //
+        // Moreover, for a gradual constraint, we don't need to worry that typevar constraints are
+        // _equality_ comparisons, not _subtyping_ comparisons — since we are only going to check
+        // that _some_ valid specialization satisfies the constraint set, it's correct for us to
+        // return the range of valid materializations that we can choose from.
         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,
-            ),
+            None => Node::AlwaysTrue,
+            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                let bound = bound.top_materialization(db);
+                ConstrainedTypeVar::new_node(db, self, Type::Never, bound)
+            }
             Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
-                constraints.elements(db).iter().when_any(db, |constraint| {
-                    ConstraintSet::constrain_typevar(
+                let mut specializations = Node::AlwaysFalse;
+                for constraint in constraints.elements(db) {
+                    let constraint_lower = constraint.bottom_materialization(db);
+                    let constraint_upper = constraint.top_materialization(db);
+                    specializations = specializations.or(
                         db,
-                        self,
-                        *constraint,
-                        *constraint,
-                        TypeRelation::Assignability,
-                    )
-                })
+                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper),
+                    );
+                }
+                specializations
+            }
+        }
+    }
+
+    /// Returns the required specializations of a typevar. This is used when checking a constraint
+    /// set when this typevar is in non-inferable position, where we need _all_ specializations to
+    /// satisfy the constraint set.
+    ///
+    /// That causes complications if this is a constrained typevar, where one of the constraints is
+    /// gradual. In that case, we need to return the range of valid materializations, but we don't
+    /// want to require that all of those materializations satisfy the constraint set.
+    ///
+    /// To handle this, we return a "primary" result, and an iterator of any gradual constraints.
+    /// For an unbounded/unconstrained typevar or a bounded typevar, the primary result fully
+    /// specifies the required specializations, and the iterator will be empty. For a constrained
+    /// typevar, the primary result will include the fully static constraints, and the iterator
+    /// will include an entry for each non-fully-static constraint.
+    fn required_specializations(
+        self,
+        db: &'db dyn Db,
+    ) -> (Node<'db>, impl IntoIterator<Item = Node<'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. We therefore take the bottom
+        // materialization of the bound or constraints.
+        match self.typevar(db).bound_or_constraints(db) {
+            None => (Node::AlwaysTrue, Vec::new()),
+            Some(TypeVarBoundOrConstraints::UpperBound(bound)) => {
+                let bound = bound.bottom_materialization(db);
+                (
+                    ConstrainedTypeVar::new_node(db, self, Type::Never, bound),
+                    Vec::new(),
+                )
+            }
+            Some(TypeVarBoundOrConstraints::Constraints(constraints)) => {
+                let mut non_gradual_constraints = Node::AlwaysFalse;
+                let mut gradual_constraints = Vec::new();
+                for constraint in constraints.elements(db) {
+                    let constraint_lower = constraint.bottom_materialization(db);
+                    let constraint_upper = constraint.top_materialization(db);
+                    let constraint =
+                        ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper);
+                    if constraint_lower == constraint_upper {
+                        non_gradual_constraints = non_gradual_constraints.or(db, constraint);
+                    } else {
+                        gradual_constraints.push(constraint);
+                    }
+                }
+                (non_gradual_constraints, gradual_constraints)
             }
         }
     }