From 3ee3f71686506277ebfab6d50871ecb41e02a1d2 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 09:45:53 -0500 Subject: [PATCH 1/7] bounded by gradual --- .../satisfied_by_all_typevars.md | 57 +++++++++++++++++++ .../src/types/constraints.rs | 39 +++++++------ 2 files changed, 80 insertions(+), 16 deletions(-) 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..48ddcc774150b 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,63 @@ 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()) +``` + ## Constrained typevar If a typevar has constraints, then it must specialize to one of those specific types. (Not to a diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index c1e5ac269779c..3ea0f4a3a5866 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/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) }) } } From 337fe875c89b7061169439ee5a17b1a3aaceb0ce Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 12:11:44 -0500 Subject: [PATCH 2/7] bounded by invariant --- .../satisfied_by_all_typevars.md | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) 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 48ddcc774150b..346753cd2e774 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 @@ -198,6 +198,59 @@ def bounded_by_gradual[T: Any](): 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 From 7af42b8a5ecac7109e43526acaac3c2c055fe24e Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 12:39:28 -0500 Subject: [PATCH 3/7] constrained by gradual --- .../satisfied_by_all_typevars.md | 40 +++++++++++++++++++ 1 file changed, 40 insertions(+) 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 346753cd2e774..8a499028f260f 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 @@ -328,3 +328,43 @@ 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()) +``` From 45279de823248156f441323d1b44032dc0a12705 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 12:43:45 -0500 Subject: [PATCH 4/7] constrained by invariant --- .../satisfied_by_all_typevars.md | 53 +++++++++++++++++++ 1 file changed, 53 insertions(+) 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 8a499028f260f..e90339657c37a 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 @@ -368,3 +368,56 @@ def constrained_by_gradual[T: (Base, Any)](): # 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()) +``` From 1295459fcccfd63bbba9523ffd447280124ee8de Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 15:55:20 -0500 Subject: [PATCH 5/7] clarify docs --- .../satisfied_by_all_typevars.md | 32 +++++++++---------- 1 file changed, 16 insertions(+), 16 deletions(-) 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 e90339657c37a..23457cb74298a 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 @@ -142,12 +142,12 @@ def bounded[T: Base](): ``` 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. +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 @@ -199,8 +199,8 @@ def bounded_by_gradual[T: Any](): ``` 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 +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. @@ -330,12 +330,12 @@ def constrained[T: (Base, Unrelated)](): ``` 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. +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 @@ -370,8 +370,8 @@ def constrained_by_gradual[T: (Base, Any)](): ``` 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 +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. From d49fe8964b9906d3227bf5922b5b55c50ab4cf57 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 17:43:41 -0500 Subject: [PATCH 6/7] contraints are more complex :-( --- .../satisfied_by_all_typevars.md | 96 ++++++++++- .../src/types/constraints.rs | 150 +++++++++++++----- 2 files changed, 208 insertions(+), 38 deletions(-) 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 23457cb74298a..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 @@ -329,7 +329,7 @@ def constrained[T: (Base, 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 +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 @@ -361,6 +361,41 @@ def constrained_by_gradual[T: (Base, Any)](): # 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])) @@ -369,7 +404,7 @@ def constrained_by_gradual[T: (Base, Any)](): 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 +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 @@ -383,6 +418,12 @@ def constrained_by_gradual[T: (list[Base], list[Any])](): 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])) @@ -420,4 +461,55 @@ def constrained_by_gradual[T: (list[Base], list[Any])](): # 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 3ea0f4a3a5866..509a1df31aadd 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -869,25 +869,50 @@ impl<'db> Node<'db> { typevars.insert(constraint.typevar(db)); }); + // 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, specializations); + !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); + when_satisfied + .iff(db, specializations) + .is_always_satisfied(db) + }; + for typevar in typevars { - // Determine which valid specializations of this typevar satisfy the constraint set. - let valid_specializations = typevar.valid_specializations(db, inferable).node; - let when_satisfied = valid_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() + 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,35 +2007,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( + /// 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 => Node::AlwaysTrue, + Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { + let bound = bound.top_materialization(db); + ConstrainedTypeVar::new_node(db, self, Type::Never, bound) + } + Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { + 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, + 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, - inferable: InferableTypeVars<'_, 'db>, - ) -> ConstraintSet<'db> { + ) -> (Node<'db>, impl IntoIterator>) { // 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 - }; - + // 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 => ConstraintSet::from(true), + None => (Node::AlwaysTrue, Vec::new()), Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { - ConstraintSet::constrain_typevar(db, self, Type::Never, bound, relation) + let bound = bound.bottom_materialization(db); + ( + ConstrainedTypeVar::new_node(db, self, Type::Never, bound), + Vec::new(), + ) } Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { - constraints.elements(db).iter().when_any(db, |constraint| { - ConstraintSet::constrain_typevar(db, self, *constraint, *constraint, relation) - }) + 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) } } } From fc22207f2a9b147f3a66608a4a112b0ee469c0e5 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 22:19:14 -0500 Subject: [PATCH 7/7] fix those tests --- crates/ty_python_semantic/src/types/constraints.rs | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 509a1df31aadd..d2520deb083ba 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -871,13 +871,19 @@ impl<'db> Node<'db> { // 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, specializations); + let when_satisfied = specializations + .satisfies(db, self) + .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); + let when_satisfied = specializations + .satisfies(db, self) + .and(db, specializations) + .simplify(db); when_satisfied .iff(db, specializations) .is_always_satisfied(db)