mirrors/ruff
1
0
Fork 0
mirror of https://github.com/astral-sh/ruff.git synced 2025-11-18 19:41:34 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions 3

[ty] Clarify behavior of constraint sets for gradual upper bounds and constraints (#21287)

Browse source 
When checking whether a constraint set is satisfied, if a typevar has a
non-fully-static upper bound or constraint, we are free to choose any
materialization that makes the check succeed.

In non-inferable positions, we have to show that the constraint set is
satisfied for all valid specializations, so it's best to choose the most
restrictive materialization, since that minimizes the set of valid
specializations that have to pass.

In inferable positions, we only have to show that the constraint set is
satisfied for _some_ valid specializations, so it's best to choose the
most permissive materialization, since that maximizes our chances of
finding a specialization that passes.
This commit is contained in:
Douglas Creager 2025-11-07 14:01:39 -05:00 • committed by GitHub
parent 276f1d0d88
commit faae72b836
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 388 additions and 35 deletions
Download patch file Download diff file Expand all files Collapse all files

262
crates/ty_python_semantic/resources/mdtest/type_properties/satisfied_by_all_typevars.md
View file

@ -141,6 +141,97 @@ 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 Base as the materialization for the upper bound, 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]))
# We are free to choose any materialization of the upper bound, and only have to show that the
# constraint set holds for that one materialization. Having chosen one materialization, we then
# have to show that the constraint set holds for all valid specializations of that
# materialization. If we choose Never as the materialization, then all valid specializations
# must satisfy (T ≤ Never). That means there is only one valid specialization, (T = Never),
# which satisfies (T ≤ Base).
static_assert(ConstraintSet.range(Never, T, Base).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 list[Base] as the materialization of the upper bound, 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]).
# We are free to choose any materialization of the upper bound, and only have to show that the
# constraint set holds for that one materialization. Having chosen one materialization, we then
# have to show that the constraint set holds for all valid specializations of that
# materialization. If we choose list[Base] as the materialization, then all valid specializations
# must satisfy (T ≤ list[Base]), which is exactly the constraint set that we need to satisfy.
static_assert(ConstraintSet.range(Never, T, list[Base]).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 +309,174 @@ 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 of the gradual constraint, 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 of either constraint, 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 of both constraints, 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 Base as the materialization of either constraint, 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 of both constraints, then (T = Never) is the only
# valid specialization, which satisfies (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 list[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 list[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 list[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 list[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 list[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 list[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 materialization 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 list[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 list[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 list[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 list[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 list[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())
```

161
crates/ty_python_semantic/src/types/constraints.rs
View file

@ -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)
}
}
}