[ty] Constraining a typevar with itself (possibly via union or intersection) (#21273)

This PR carries over some of the `has_relation_to` logic for comparing a
typevar with itself. A typevar will specialize to the same type if it's
mentioned multiple times, so it is always assignable to and a subtype of
itself. (Note that typevars can only specialize to fully static types.)
This is also true when the typevar appears in a union on the right-hand
side, or in an intersection on the left-hand side. Similarly, a typevar
is always disjoint from its negation, so when a negated typevar appears
on the left-hand side, the constraint set is never satisfiable.

(Eventually this will allow us to remove the corresponding clauses from
`has_relation_to`, but that can't happen until more of #20093 lands.)
This commit is contained in:
Douglas Creager 2025-11-05 12:31:53 -05:00 committed by GitHub
parent cef6600cf3
commit eda85f3c64
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
6 changed files with 278 additions and 10 deletions

View file

@ -258,6 +258,50 @@ def _[T]() -> None:
reveal_type(ConstraintSet.range(SubSub, T, Sub) & ConstraintSet.range(Unrelated, T, object))
```
Expanding on this, when intersecting two upper bounds constraints (`(T ≤ Base) ∧ (T ≤ Other)`), we
intersect the upper bounds. Any type that satisfies both `T ≤ Base` and `T ≤ Other` must necessarily
satisfy their intersection `T ≤ Base & Other`, and vice versa.
```py
from typing import Never
from ty_extensions import Intersection, static_assert
# This is not final, so it's possible for a subclass to inherit from both Base and Other.
class Other: ...
def upper_bounds[T]():
intersection_type = ConstraintSet.range(Never, T, Intersection[Base, Other])
# revealed: ty_extensions.ConstraintSet[(T@upper_bounds ≤ Base & Other)]
reveal_type(intersection_type)
intersection_constraint = ConstraintSet.range(Never, T, Base) & ConstraintSet.range(Never, T, Other)
# revealed: ty_extensions.ConstraintSet[(T@upper_bounds ≤ Base & Other)]
reveal_type(intersection_constraint)
# The two constraint sets are equivalent; each satisfies the other.
static_assert(intersection_type.satisfies(intersection_constraint))
static_assert(intersection_constraint.satisfies(intersection_type))
```
For an intersection of two lower bounds constraints (`(Base ≤ T) ∧ (Other ≤ T)`), we union the lower
bounds. Any type that satisfies both `Base ≤ T` and `Other ≤ T` must necessarily satisfy their union
`Base | Other ≤ T`, and vice versa.
```py
def lower_bounds[T]():
union_type = ConstraintSet.range(Base | Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@lower_bounds)]
reveal_type(union_type)
intersection_constraint = ConstraintSet.range(Base, T, object) & ConstraintSet.range(Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@lower_bounds)]
reveal_type(intersection_constraint)
# The two constraint sets are equivalent; each satisfies the other.
static_assert(union_type.satisfies(intersection_constraint))
static_assert(intersection_constraint.satisfies(union_type))
```
### Intersection of a range and a negated range
The bounds of the range constraint provide a range of types that should be included; the bounds of
@ -335,7 +379,7 @@ def _[T]() -> None:
reveal_type(~ConstraintSet.range(Sub, T, Super) & ~ConstraintSet.range(Sub, T, Super))
```
Otherwise, the union cannot be simplified.
Otherwise, the intersection cannot be simplified.
```py
def _[T]() -> None:
@ -350,13 +394,14 @@ def _[T]() -> None:
In particular, the following does not simplify, even though it seems like it could simplify to
`¬(SubSub ≤ T@_ ≤ Super)`. The issue is that there are types that are within the bounds of
`SubSub ≤ T@_ ≤ Super`, but which are not comparable to `Base` or `Sub`, and which therefore should
be included in the union. An example would be the type that contains all instances of `Super`,
`Base`, and `SubSub` (but _not_ including instances of `Sub`). (We don't have a way to spell that
type at the moment, but it is a valid type.) That type is not in `SubSub ≤ T ≤ Base`, since it
includes `Super`, which is outside the range. It's also not in `Sub ≤ T ≤ Super`, because it does
not include `Sub`. That means it should be in the union. (Remember that for negated range
constraints, the lower and upper bounds define the "hole" of types that are _not_ allowed.) Since
that type _is_ in `SubSub ≤ T ≤ Super`, it is not correct to simplify the union in this way.
be included in the intersection. An example would be the type that contains all instances of
`Super`, `Base`, and `SubSub` (but _not_ including instances of `Sub`). (We don't have a way to
spell that type at the moment, but it is a valid type.) That type is not in `SubSub ≤ T ≤ Base`,
since it includes `Super`, which is outside the range. It's also not in `Sub ≤ T ≤ Super`, because
it does not include `Sub`. That means it should be in the intersection. (Remember that for negated
range constraints, the lower and upper bounds define the "hole" of types that are _not_ allowed.)
Since that type _is_ in `SubSub ≤ T ≤ Super`, it is not correct to simplify the intersection in this
way.
```py
def _[T]() -> None:
@ -441,6 +486,65 @@ def _[T]() -> None:
reveal_type(ConstraintSet.range(SubSub, T, Base) | ConstraintSet.range(Sub, T, Super))
```
The union of two upper bound constraints (`(T ≤ Base) (T ≤ Other)`) is different than the single
range constraint involving the corresponding union type (`T ≤ Base | Other`). There are types (such
as `T = Base | Other`) that satisfy the union type, but not the union constraint. But every type
that satisfies the union constraint satisfies the union type.
```py
from typing import Never
from ty_extensions import static_assert
# This is not final, so it's possible for a subclass to inherit from both Base and Other.
class Other: ...
def union[T]():
union_type = ConstraintSet.range(Never, T, Base | Other)
# revealed: ty_extensions.ConstraintSet[(T@union ≤ Base | Other)]
reveal_type(union_type)
union_constraint = ConstraintSet.range(Never, T, Base) | ConstraintSet.range(Never, T, Other)
# revealed: ty_extensions.ConstraintSet[(T@union ≤ Base) (T@union ≤ Other)]
reveal_type(union_constraint)
# (T = Base | Other) satisfies (T ≤ Base | Other) but not (T ≤ Base T ≤ Other)
specialization = ConstraintSet.range(Base | Other, T, Base | Other)
# revealed: ty_extensions.ConstraintSet[(T@union = Base | Other)]
reveal_type(specialization)
static_assert(specialization.satisfies(union_type))
static_assert(not specialization.satisfies(union_constraint))
# Every specialization that satisfies (T ≤ Base T ≤ Other) also satisfies
# (T ≤ Base | Other)
static_assert(union_constraint.satisfies(union_type))
```
These relationships are reversed for unions involving lower bounds. `T = Base` is an example that
satisfies the union constraint (`(Base ≤ T) (Other ≤ T)`) but not the union type
(`Base | Other ≤ T`). And every type that satisfies the union type satisfies the union constraint.
```py
def union[T]():
union_type = ConstraintSet.range(Base | Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base | Other ≤ T@union)]
reveal_type(union_type)
union_constraint = ConstraintSet.range(Base, T, object) | ConstraintSet.range(Other, T, object)
# revealed: ty_extensions.ConstraintSet[(Base ≤ T@union) (Other ≤ T@union)]
reveal_type(union_constraint)
# (T = Base) satisfies (Base ≤ T Other ≤ T) but not (Base | Other ≤ T)
specialization = ConstraintSet.range(Base, T, Base)
# revealed: ty_extensions.ConstraintSet[(T@union = Base)]
reveal_type(specialization)
static_assert(not specialization.satisfies(union_type))
static_assert(specialization.satisfies(union_constraint))
# Every specialization that satisfies (Base | Other ≤ T) also satisfies
# (Base ≤ T Other ≤ T)
static_assert(union_type.satisfies(union_constraint))
```
### Union of a range and a negated range
The bounds of the range constraint provide a range of types that should be included; the bounds of
@ -729,3 +833,52 @@ def f[T]():
# revealed: ty_extensions.ConstraintSet[(T@f ≤ int | str)]
reveal_type(ConstraintSet.range(Never, T, int | str))
```
### Constraints on the same typevar
Any particular specialization maps each typevar to one type. That means it's not useful to constrain
a typevar with itself as an upper or lower bound. No matter what type the typevar is specialized to,
that type is always a subtype of itself. (Remember that typevars are only specialized to fully
static types.)
```py
from typing import Never
from ty_extensions import ConstraintSet
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(Never, T, T))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(T, T, object))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(T, T, T))
```
This is also true when the typevar appears in a union in the upper bound, or in an intersection in
the lower bound. (Note that this lines up with how we simplify the intersection of two constraints,
as shown above.)
```py
from ty_extensions import Intersection
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(Never, T, T | None))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(Intersection[T, None], T, object))
# revealed: ty_extensions.ConstraintSet[always]
reveal_type(ConstraintSet.range(Intersection[T, None], T, T | None))
```
Similarly, if the lower bound is an intersection containing the _negation_ of the typevar, then the
constraint set can never be satisfied, since every type is disjoint with its negation.
```py
from ty_extensions import Not
def same_typevar[T]():
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(ConstraintSet.range(Intersection[Not[T], None], T, object))
# revealed: ty_extensions.ConstraintSet[never]
reveal_type(ConstraintSet.range(Not[T], T, object))
```

View file

@ -4197,6 +4197,14 @@ impl<'db> Type<'db> {
))
.into()
}
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
if name == "satisfies" =>
{
Place::bound(Type::KnownBoundMethod(
KnownBoundMethodType::ConstraintSetSatisfies(tracked),
))
.into()
}
Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked))
if name == "satisfied_by_all_typevars" =>
{
@ -6973,6 +6981,7 @@ impl<'db> Type<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_)
)
| Type::DataclassDecorator(_)
@ -7126,6 +7135,7 @@ impl<'db> Type<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
)
| Type::DataclassDecorator(_)
@ -10470,6 +10480,7 @@ pub enum KnownBoundMethodType<'db> {
ConstraintSetAlways,
ConstraintSetNever,
ConstraintSetImpliesSubtypeOf(TrackedConstraintSet<'db>),
ConstraintSetSatisfies(TrackedConstraintSet<'db>),
ConstraintSetSatisfiedByAllTypeVars(TrackedConstraintSet<'db>),
}
@ -10499,6 +10510,7 @@ pub(super) fn walk_method_wrapper_type<'db, V: visitor::TypeVisitor<'db> + ?Size
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {}
}
}
@ -10568,6 +10580,10 @@ impl<'db> KnownBoundMethodType<'db> {
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_),
)
| (
KnownBoundMethodType::ConstraintSetSatisfies(_),
KnownBoundMethodType::ConstraintSetSatisfies(_),
)
| (
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
@ -10584,6 +10600,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::FunctionTypeDunderGet(_)
| KnownBoundMethodType::FunctionTypeDunderCall(_)
@ -10595,6 +10612,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
) => ConstraintSet::from(false),
}
@ -10649,6 +10667,10 @@ impl<'db> KnownBoundMethodType<'db> {
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(left_constraints),
KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(right_constraints),
)
| (
KnownBoundMethodType::ConstraintSetSatisfies(left_constraints),
KnownBoundMethodType::ConstraintSetSatisfies(right_constraints),
)
| (
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(left_constraints),
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(right_constraints),
@ -10667,6 +10689,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
KnownBoundMethodType::FunctionTypeDunderGet(_)
| KnownBoundMethodType::FunctionTypeDunderCall(_)
@ -10678,6 +10701,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_),
) => ConstraintSet::from(false),
}
@ -10703,6 +10727,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => self,
}
}
@ -10720,6 +10745,7 @@ impl<'db> KnownBoundMethodType<'db> {
| KnownBoundMethodType::ConstraintSetAlways
| KnownBoundMethodType::ConstraintSetNever
| KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)
| KnownBoundMethodType::ConstraintSetSatisfies(_)
| KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {
KnownClass::ConstraintSet
}
@ -10862,6 +10888,14 @@ impl<'db> KnownBoundMethodType<'db> {
)))
}
KnownBoundMethodType::ConstraintSetSatisfies(_) => {
Either::Right(std::iter::once(Signature::new(
Parameters::new([Parameter::positional_only(Some(Name::new_static("other")))
.with_annotated_type(KnownClass::ConstraintSet.to_instance(db))]),
Some(KnownClass::ConstraintSet.to_instance(db)),
)))
}
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(_) => {
Either::Right(std::iter::once(Signature::new(
Parameters::new([Parameter::keyword_only(Name::new_static("inferable"))

View file

@ -1176,6 +1176,26 @@ impl<'db> Bindings<'db> {
));
}
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSatisfies(
tracked,
)) => {
let [Some(other)] = overload.parameter_types() else {
continue;
};
let Type::KnownInstance(KnownInstanceType::ConstraintSet(other)) = other
else {
continue;
};
let result = tracked
.constraints(db)
.implies(db, || other.constraints(db));
let tracked = TrackedConstraintSet::new(db, result);
overload.set_return_type(Type::KnownInstance(
KnownInstanceType::ConstraintSet(tracked),
));
}
Type::KnownBoundMethod(
KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(tracked),
) => {

View file

@ -320,6 +320,11 @@ impl<'db> ConstraintSet<'db> {
self
}
/// Returns a constraint set encoding that this constraint set implies another.
pub(crate) fn implies(self, db: &'db dyn Db, other: impl FnOnce() -> Self) -> Self {
self.negate(db).or(db, other)
}
pub(crate) fn iff(self, db: &'db dyn Db, other: Self) -> Self {
ConstraintSet {
node: self.node.iff(db, other.node),
@ -381,12 +386,58 @@ impl<'db> ConstrainedTypeVar<'db> {
fn new_node(
db: &'db dyn Db,
typevar: BoundTypeVarInstance<'db>,
lower: Type<'db>,
upper: Type<'db>,
mut lower: Type<'db>,
mut upper: Type<'db>,
) -> Node<'db> {
debug_assert_eq!(lower, lower.bottom_materialization(db));
debug_assert_eq!(upper, upper.top_materialization(db));
// Two identical typevars must always solve to the same type, so it is not useful to have
// an upper or lower bound that is the typevar being constrained.
match lower {
Type::TypeVar(lower_bound_typevar)
if typevar.is_same_typevar_as(db, lower_bound_typevar) =>
{
lower = Type::Never;
}
Type::Intersection(intersection)
if intersection.positive(db).iter().any(|element| {
element.as_typevar().is_some_and(|element_bound_typevar| {
typevar.is_same_typevar_as(db, element_bound_typevar)
})
}) =>
{
lower = Type::Never;
}
Type::Intersection(intersection)
if intersection.negative(db).iter().any(|element| {
element.as_typevar().is_some_and(|element_bound_typevar| {
typevar.is_same_typevar_as(db, element_bound_typevar)
})
}) =>
{
return Node::AlwaysFalse;
}
_ => {}
}
match upper {
Type::TypeVar(upper_bound_typevar)
if typevar.is_same_typevar_as(db, upper_bound_typevar) =>
{
upper = Type::object();
}
Type::Union(union)
if union.elements(db).iter().any(|element| {
element.as_typevar().is_some_and(|element_bound_typevar| {
typevar.is_same_typevar_as(db, element_bound_typevar)
})
}) =>
{
upper = Type::object();
}
_ => {}
}
// If `lower ≰ upper`, then the constraint cannot be satisfied, since there is no type that
// is both greater than `lower`, and less than `upper`.
if !lower.is_subtype_of(db, upper) {

View file

@ -535,6 +535,9 @@ impl Display for DisplayRepresentation<'_> {
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetImpliesSubtypeOf(_)) => {
f.write_str("bound method `ConstraintSet.implies_subtype_of`")
}
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSatisfies(_)) => {
f.write_str("bound method `ConstraintSet.satisfies`")
}
Type::KnownBoundMethod(KnownBoundMethodType::ConstraintSetSatisfiedByAllTypeVars(
_,
)) => f.write_str("bound method `ConstraintSet.satisfied_by_all_typevars`"),

View file

@ -67,6 +67,13 @@ class ConstraintSet:
.. _subtype: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence
"""
def satisfies(self, other: Self) -> Self:
"""
Returns whether this constraint set satisfies another that is, whether
every specialization that satisfies this constraint set also satisfies
`other`.
"""
def satisfied_by_all_typevars(
self, *, inferable: tuple[Any, ...] | None = None
) -> bool: