From eda85f3c646ddb9f3dddf13315d653f51d187f64 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Wed, 5 Nov 2025 12:31:53 -0500 Subject: [PATCH] [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.) --- .../mdtest/type_properties/constraints.md | 169 +++++++++++++++++- crates/ty_python_semantic/src/types.rs | 34 ++++ .../ty_python_semantic/src/types/call/bind.rs | 20 +++ .../src/types/constraints.rs | 55 +++++- .../ty_python_semantic/src/types/display.rs | 3 + .../ty_extensions/ty_extensions.pyi | 7 + 6 files changed, 278 insertions(+), 10 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md index 00a3e2837f..f677298c51 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md @@ -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)) +``` diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index 131d9e7630..59e1ef4030 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -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")) diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs index d2739fa696..60868cfc3f 100644 --- a/crates/ty_python_semantic/src/types/call/bind.rs +++ b/crates/ty_python_semantic/src/types/call/bind.rs @@ -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), ) => { diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index ee66cd85f3..c1e5ac2697 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -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) { diff --git a/crates/ty_python_semantic/src/types/display.rs b/crates/ty_python_semantic/src/types/display.rs index 8500c142e8..42e2373134 100644 --- a/crates/ty_python_semantic/src/types/display.rs +++ b/crates/ty_python_semantic/src/types/display.rs @@ -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`"), diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi index d23554f0ae..744bd5af37 100644 --- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi +++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi @@ -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: