From 29462ea1d486dd8976251a2d3b6ebb3890c55ad3 Mon Sep 17 00:00:00 2001 From: Douglas Creager Date: Mon, 27 Oct 2025 22:01:08 -0400 Subject: [PATCH] [ty] Add new "constraint implication" typing relation (#21010) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit This PR adds the new **_constraint implication_** relationship between types, aka `is_subtype_of_given`, which tests whether one type is a subtype of another _assuming that the constraints in a particular constraint set hold_. For concrete types, constraint implication is exactly the same as subtyping. (A concrete type is any fully static type that is not a typevar. It can _contain_ a typevar, though — `list[T]` is considered concrete.) The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the question when considering a typevar, by translating the desired relationship into a constraint set. At some point, though, we need to resolve a constraint set; at that point, we can no longer punt on the question. Unlike with concrete types, the answer will depend on the constraint set that we are considering. --- .../mdtest/type_properties/constraints.md | 56 ++++ .../type_properties/is_subtype_of_given.md | 198 ++++++++++++ crates/ty_python_semantic/src/types.rs | 35 ++- .../ty_python_semantic/src/types/call/bind.rs | 28 ++ .../src/types/constraints.rs | 288 +++++++++++++++--- .../ty_python_semantic/src/types/function.rs | 9 +- .../src/types/type_ordering.rs | 6 +- .../ty_extensions/ty_extensions.pyi | 17 +- 8 files changed, 578 insertions(+), 59 deletions(-) create mode 100644 crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of_given.md 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 65b59a55b4..5d1f4e7142 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/constraints.md @@ -602,6 +602,62 @@ def _[T, U]() -> None: reveal_type(~union | union) ``` +## Typevar ordering + +Constraints can relate two typevars — i.e., `S ≤ T`. We could encode that in one of two ways: +`Never ≤ S ≤ T` or `S ≤ T ≤ object`. In other words, we can decide whether `S` or `T` is the typevar +being constrained. The other is then the lower or upper bound of the constraint. + +To handle this, we enforce an arbitrary ordering on typevars, and always place the constraint on the +"earlier" typevar. For the example above, that does not change how the constraint is displayed, +since we always hide `Never` lower bounds and `object` upper bounds. + +```py +from typing import Never +from ty_extensions import range_constraint + +def f[S, T](): + # revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] + reveal_type(range_constraint(Never, S, T)) + # revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] + reveal_type(range_constraint(S, T, object)) + +def f[T, S](): + # revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] + reveal_type(range_constraint(Never, S, T)) + # revealed: ty_extensions.ConstraintSet[(S@f ≤ T@f)] + reveal_type(range_constraint(S, T, object)) +``` + +Equivalence constraints are similar; internally we arbitrarily choose the "earlier" typevar to be +the constraint, and the other the bound. But we display the result the same way no matter what. + +```py +def f[S, T](): + # revealed: ty_extensions.ConstraintSet[(S@f = T@f)] + reveal_type(range_constraint(T, S, T)) + # revealed: ty_extensions.ConstraintSet[(S@f = T@f)] + reveal_type(range_constraint(S, T, S)) + +def f[T, S](): + # revealed: ty_extensions.ConstraintSet[(S@f = T@f)] + reveal_type(range_constraint(T, S, T)) + # revealed: ty_extensions.ConstraintSet[(S@f = T@f)] + reveal_type(range_constraint(S, T, S)) +``` + +But in the case of `S ≤ T ≤ U`, we end up with an ambiguity. Depending on the typevar ordering, that +might display as `S ≤ T ≤ U`, or as `(S ≤ T) ∧ (T ≤ U)`. + +```py +def f[S, T, U](): + # Could be either of: + # ty_extensions.ConstraintSet[(S@f ≤ T@f ≤ U@f)] + # ty_extensions.ConstraintSet[(S@f ≤ T@f) ∧ (T@f ≤ U@f)] + # reveal_type(range_constraint(S, T, U)) + ... +``` + ## Other simplifications ### Displaying constraint sets diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of_given.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of_given.md new file mode 100644 index 0000000000..c1a0577fa3 --- /dev/null +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of_given.md @@ -0,0 +1,198 @@ +# Constraint implication + +```toml +[environment] +python-version = "3.12" +``` + +This file tests the _constraint implication_ relationship between types, aka `is_subtype_of_given`, +which tests whether one type is a [subtype][subtyping] of another _assuming that the constraints in +a particular constraint set hold_. + +## Concrete types + +For concrete types, constraint implication is exactly the same as subtyping. (A concrete type is any +fully static type that is not a typevar. It can _contain_ a typevar, though — `list[T]` is +considered concrete.) + +```py +from ty_extensions import is_subtype_of, is_subtype_of_given, static_assert + +def equivalent_to_other_relationships[T](): + static_assert(is_subtype_of(bool, int)) + static_assert(is_subtype_of_given(True, bool, int)) + + static_assert(not is_subtype_of(bool, str)) + static_assert(not is_subtype_of_given(True, bool, str)) +``` + +Moreover, for concrete types, the answer does not depend on which constraint set we are considering. +`bool` is a subtype of `int` no matter what types any typevars are specialized to — and even if +there isn't a valid specialization for the typevars we are considering. + +```py +from typing import Never +from ty_extensions import range_constraint + +def even_given_constraints[T](): + constraints = range_constraint(Never, T, int) + static_assert(is_subtype_of_given(constraints, bool, int)) + static_assert(not is_subtype_of_given(constraints, bool, str)) + +def even_given_unsatisfiable_constraints(): + static_assert(is_subtype_of_given(False, bool, int)) + static_assert(not is_subtype_of_given(False, bool, str)) +``` + +## Type variables + +The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on the +question when considering a typevar, by translating the desired relationship into a constraint set. + +```py +from typing import Any +from ty_extensions import is_assignable_to, is_subtype_of + +def assignability[T](): + # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ bool] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(T, bool)) + # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ int] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(T, int)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(is_assignable_to(T, object)) + +def subtyping[T](): + # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ bool] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(T, bool)) + # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ int] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(T, int)) + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(is_subtype_of(T, object)) +``` + +When checking assignability with a dynamic type, we use the bottom and top materializations of the +lower and upper bounds, respectively. For subtyping, we use the top and bottom materializations. +(That is, assignability turns into a "permissive" constraint, and subtyping turns into a +"conservative" constraint.) + +```py +class Covariant[T]: + def get(self) -> T: + raise ValueError + +class Contravariant[T]: + def set(self, value: T): + pass + +def assignability[T](): + # aka [T@assignability ≤ object], which is always satisfiable + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(is_assignable_to(T, Any)) + + # aka [Never ≤ T@assignability], which is always satisfiable + # revealed: ty_extensions.ConstraintSet[always] + reveal_type(is_assignable_to(Any, T)) + + # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Covariant[object]] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(T, Covariant[Any])) + # TODO: revealed: ty_extensions.ConstraintSet[Covariant[Never] ≤ T@assignability] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(Covariant[Any], T)) + + # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Contravariant[Never]] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(T, Contravariant[Any])) + # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[object] ≤ T@assignability] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_assignable_to(Contravariant[Any], T)) + +def subtyping[T](): + # aka [T@assignability ≤ object], which is always satisfiable + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(T, Any)) + + # aka [Never ≤ T@assignability], which is always satisfiable + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(Any, T)) + + # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Covariant[Never]] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(T, Covariant[Any])) + # TODO: revealed: ty_extensions.ConstraintSet[Covariant[object] ≤ T@subtyping] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(Covariant[Any], T)) + + # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Contravariant[object]] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(T, Contravariant[Any])) + # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[Never] ≤ T@subtyping] + # revealed: ty_extensions.ConstraintSet[never] + reveal_type(is_subtype_of(Contravariant[Any], T)) +``` + +At some point, though, we need to resolve a constraint set; at that point, we can no longer punt on +the question. Unlike with concrete types, the answer will depend on the constraint set that we are +considering. + +```py +from typing import Never +from ty_extensions import is_subtype_of_given, range_constraint, static_assert + +def given_constraints[T](): + static_assert(not is_subtype_of_given(True, T, int)) + static_assert(not is_subtype_of_given(True, T, bool)) + static_assert(not is_subtype_of_given(True, T, str)) + + # These are vacuously true; false implies anything + static_assert(is_subtype_of_given(False, T, int)) + static_assert(is_subtype_of_given(False, T, bool)) + static_assert(is_subtype_of_given(False, T, str)) + + given_int = range_constraint(Never, T, int) + static_assert(is_subtype_of_given(given_int, T, int)) + static_assert(not is_subtype_of_given(given_int, T, bool)) + static_assert(not is_subtype_of_given(given_int, T, str)) + + given_bool = range_constraint(Never, T, bool) + static_assert(is_subtype_of_given(given_bool, T, int)) + static_assert(is_subtype_of_given(given_bool, T, bool)) + static_assert(not is_subtype_of_given(given_bool, T, str)) + + given_both = given_bool & given_int + static_assert(is_subtype_of_given(given_both, T, int)) + static_assert(is_subtype_of_given(given_both, T, bool)) + static_assert(not is_subtype_of_given(given_both, T, str)) + + given_str = range_constraint(Never, T, str) + static_assert(not is_subtype_of_given(given_str, T, int)) + static_assert(not is_subtype_of_given(given_str, T, bool)) + static_assert(is_subtype_of_given(given_str, T, str)) +``` + +This might require propagating constraints from other typevars. + +```py +def mutually_constrained[T, U](): + # If [T = U ∧ U ≤ int], then [T ≤ int] must be true as well. + given_int = range_constraint(U, T, U) & range_constraint(Never, U, int) + # TODO: no static-assert-error + # error: [static-assert-error] + static_assert(is_subtype_of_given(given_int, T, int)) + static_assert(not is_subtype_of_given(given_int, T, bool)) + static_assert(not is_subtype_of_given(given_int, T, str)) + + # If [T ≤ U ∧ U ≤ int], then [T ≤ int] must be true as well. + given_int = range_constraint(Never, T, U) & range_constraint(Never, U, int) + # TODO: no static-assert-error + # error: [static-assert-error] + static_assert(is_subtype_of_given(given_int, T, int)) + static_assert(not is_subtype_of_given(given_int, T, bool)) + static_assert(not is_subtype_of_given(given_int, T, str)) +``` + +[subtyping]: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index f2330fabc3..8f87593986 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1724,7 +1724,7 @@ impl<'db> Type<'db> { // since subtyping between a TypeVar and an arbitrary other type cannot be guaranteed to be reflexive. (Type::TypeVar(lhs_bound_typevar), Type::TypeVar(rhs_bound_typevar)) if !lhs_bound_typevar.is_inferable(db, inferable) - && lhs_bound_typevar.identity(db) == rhs_bound_typevar.identity(db) => + && lhs_bound_typevar.is_same_typevar_as(db, rhs_bound_typevar) => { ConstraintSet::from(true) } @@ -2621,7 +2621,7 @@ impl<'db> Type<'db> { // constraints, which are handled below. (Type::TypeVar(self_bound_typevar), Type::TypeVar(other_bound_typevar)) if !self_bound_typevar.is_inferable(db, inferable) - && self_bound_typevar.identity(db) == other_bound_typevar.identity(db) => + && self_bound_typevar.is_same_typevar_as(db, other_bound_typevar) => { ConstraintSet::from(false) } @@ -4833,6 +4833,30 @@ impl<'db> Type<'db> { ) .into(), + Some(KnownFunction::IsSubtypeOfGiven) => Binding::single( + self, + Signature::new( + Parameters::new([ + Parameter::positional_only(Some(Name::new_static("constraints"))) + .with_annotated_type(UnionType::from_elements( + db, + [ + KnownClass::Bool.to_instance(db), + KnownClass::ConstraintSet.to_instance(db), + ], + )), + Parameter::positional_only(Some(Name::new_static("ty"))) + .type_form() + .with_annotated_type(Type::any()), + Parameter::positional_only(Some(Name::new_static("of"))) + .type_form() + .with_annotated_type(Type::any()), + ]), + Some(KnownClass::ConstraintSet.to_instance(db)), + ), + ) + .into(), + Some(KnownFunction::RangeConstraint | KnownFunction::NegatedRangeConstraint) => { Binding::single( self, @@ -8534,7 +8558,6 @@ pub struct BoundTypeVarIdentity<'db> { /// A type variable that has been bound to a generic context, and which can be specialized to a /// concrete type. #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)] -#[derive(PartialOrd, Ord)] pub struct BoundTypeVarInstance<'db> { pub typevar: TypeVarInstance<'db>, binding_context: BindingContext<'db>, @@ -8555,6 +8578,12 @@ impl<'db> BoundTypeVarInstance<'db> { } } + /// Returns whether two bound typevars represent the same logical typevar, regardless of e.g. + /// differences in their bounds or constraints due to materialization. + pub(crate) fn is_same_typevar_as(self, db: &'db dyn Db, other: Self) -> bool { + self.identity(db) == other.identity(db) + } + /// Create a new PEP 695 type variable that can be used in signatures /// of synthetic generic functions. pub(crate) fn synthetic( diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs index e72d798dd6..d1aa621b82 100644 --- a/crates/ty_python_semantic/src/types/call/bind.rs +++ b/crates/ty_python_semantic/src/types/call/bind.rs @@ -17,6 +17,7 @@ use crate::db::Db; use crate::dunder_all::dunder_all_names; use crate::place::{Definedness, Place}; use crate::types::call::arguments::{Expansion, is_expandable_type}; +use crate::types::constraints::ConstraintSet; use crate::types::diagnostic::{ CALL_NON_CALLABLE, CONFLICTING_ARGUMENT_FORMS, INVALID_ARGUMENT_TYPE, MISSING_ARGUMENT, NO_MATCHING_OVERLOAD, PARAMETER_ALREADY_ASSIGNED, POSITIONAL_ONLY_PARAMETER_AS_KWARG, @@ -704,6 +705,33 @@ impl<'db> Bindings<'db> { } } + Some(KnownFunction::IsSubtypeOfGiven) => { + let [Some(constraints), Some(ty_a), Some(ty_b)] = + overload.parameter_types() + else { + continue; + }; + + let constraints = match constraints { + Type::KnownInstance(KnownInstanceType::ConstraintSet(tracked)) => { + tracked.constraints(db) + } + Type::BooleanLiteral(b) => ConstraintSet::from(*b), + _ => continue, + }; + + let result = constraints.when_subtype_of_given( + db, + *ty_a, + *ty_b, + InferableTypeVars::None, + ); + let tracked = TrackedConstraintSet::new(db, result); + overload.set_return_type(Type::KnownInstance( + KnownInstanceType::ConstraintSet(tracked), + )); + } + Some(KnownFunction::IsAssignableTo) => { if let [Some(ty_a), Some(ty_b)] = overload.parameter_types() { let constraints = diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 417399203c..b5e3cc3e7d 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -64,7 +64,8 @@ use rustc_hash::FxHashSet; use salsa::plumbing::AsId; use crate::Db; -use crate::types::{BoundTypeVarIdentity, IntersectionType, Type, UnionType}; +use crate::types::generics::InferableTypeVars; +use crate::types::{BoundTypeVarInstance, IntersectionType, Type, TypeRelation, UnionType}; /// An extension trait for building constraint sets from [`Option`] values. pub(crate) trait OptionConstraintsExtension { @@ -175,6 +176,31 @@ impl<'db> ConstraintSet<'db> { } } + /// Returns a constraint set that constraints a typevar to a particular range of types. + pub(crate) fn constrain_typevar( + db: &'db dyn Db, + typevar: BoundTypeVarInstance<'db>, + lower: Type<'db>, + upper: Type<'db>, + relation: TypeRelation, + ) -> Self { + let (lower, upper) = match relation { + // TODO: Is this the correct constraint for redundancy? + TypeRelation::Subtyping | TypeRelation::Redundancy => ( + lower.top_materialization(db), + upper.bottom_materialization(db), + ), + TypeRelation::Assignability => ( + lower.bottom_materialization(db), + upper.top_materialization(db), + ), + }; + + Self { + node: ConstrainedTypeVar::new_node(db, typevar, lower, upper), + } + } + /// Returns whether this constraint set never holds pub(crate) fn is_never_satisfied(self, _db: &'db dyn Db) -> bool { self.node.is_never_satisfied() @@ -185,6 +211,51 @@ impl<'db> ConstraintSet<'db> { self.node.is_always_satisfied(db) } + /// Returns the constraints under which `lhs` is a subtype of `rhs`, assuming that the + /// constraints in this constraint set hold. + /// + /// For concrete types (types that are not typevars), this returns the same result as + /// [`when_subtype_of`][Type::when_subtype_of]. (Constraint sets place restrictions on + /// typevars, so if you are not comparing typevars, the constraint set can have no effect on + /// whether subtyping holds.) + /// + /// If you're comparing a typevar, we have to consider what restrictions the constraint set + /// places on that typevar to determine if subtyping holds. For instance, if you want to check + /// whether `T ≤ int`, then answer will depend on what constraint set you are considering: + /// + /// ```text + /// when_subtype_of_given(T ≤ bool, T, int) ⇒ true + /// when_subtype_of_given(T ≤ int, T, int) ⇒ true + /// when_subtype_of_given(T ≤ str, T, int) ⇒ false + /// ``` + /// + /// In the first two cases, the constraint set ensures that `T` will always specialize to a + /// type that is a subtype of `int`. In the final case, the constraint set requires `T` to + /// specialize to a subtype of `str`, and there is no such type that is also a subtype of + /// `int`. + /// + /// There are two constraint sets that deserve special consideration. + /// + /// - The "always true" constraint set does not place any restrictions on any typevar. In this + /// case, `when_subtype_of_given` will return the same result as `when_subtype_of`, even if + /// you're comparing against a typevar. + /// + /// - The "always false" constraint set represents an impossible situation. In this case, every + /// subtype check will be vacuously true, even if you're comparing two concrete types that + /// are not actually subtypes of each other. (That is, + /// `when_subtype_of_given(false, int, str)` will return true!) + pub(crate) fn when_subtype_of_given( + self, + db: &'db dyn Db, + lhs: Type<'db>, + rhs: Type<'db>, + inferable: InferableTypeVars<'_, 'db>, + ) -> Self { + Self { + node: self.node.when_subtype_of_given(db, lhs, rhs, inferable), + } + } + /// Updates this constraint set to hold the union of itself and another constraint set. pub(crate) fn union(&mut self, db: &'db dyn Db, other: Self) -> Self { self.node = self.node.or(db, other.node); @@ -227,20 +298,16 @@ impl<'db> ConstraintSet<'db> { pub(crate) fn range( db: &'db dyn Db, lower: Type<'db>, - typevar: BoundTypeVarIdentity<'db>, + typevar: BoundTypeVarInstance<'db>, upper: Type<'db>, ) -> Self { - let lower = lower.bottom_materialization(db); - let upper = upper.top_materialization(db); - Self { - node: ConstrainedTypeVar::new_node(db, lower, typevar, upper), - } + Self::constrain_typevar(db, typevar, lower, upper, TypeRelation::Assignability) } pub(crate) fn negated_range( db: &'db dyn Db, lower: Type<'db>, - typevar: BoundTypeVarIdentity<'db>, + typevar: BoundTypeVarInstance<'db>, upper: Type<'db>, ) -> Self { Self::range(db, lower, typevar, upper).negate(db) @@ -257,11 +324,26 @@ impl From for ConstraintSet<'_> { } } +impl<'db> BoundTypeVarInstance<'db> { + /// Returns whether this typevar can be the lower or upper bound of another typevar in a + /// constraint set. + /// + /// We enforce an (arbitrary) ordering on typevars, and ensure that the bounds of a constraint + /// are "later" according to that order than the typevar being constrained. Having an order + /// ensures that we can build up transitive relationships between constraints without incurring + /// any cycles. This particular ordering plays nicely with how we are ordering constraints + /// within a BDD — it means that if a typevar has another typevar as a bound, all of the + /// constraints that apply to the bound will appear lower in the BDD. + fn can_be_bound_for(self, db: &'db dyn Db, typevar: Self) -> bool { + self.identity(db) > typevar.identity(db) + } +} + /// An individual constraint in a constraint set. This restricts a single typevar to be within a /// lower and upper bound. #[salsa::interned(debug, heap_size=ruff_memory_usage::heap_size)] pub(crate) struct ConstrainedTypeVar<'db> { - typevar: BoundTypeVarIdentity<'db>, + typevar: BoundTypeVarInstance<'db>, lower: Type<'db>, upper: Type<'db>, } @@ -276,8 +358,8 @@ impl<'db> ConstrainedTypeVar<'db> { /// Panics if `lower` and `upper` are not both fully static. fn new_node( db: &'db dyn Db, + typevar: BoundTypeVarInstance<'db>, lower: Type<'db>, - typevar: BoundTypeVarIdentity<'db>, upper: Type<'db>, ) -> Node<'db> { debug_assert_eq!(lower, lower.bottom_materialization(db)); @@ -297,7 +379,69 @@ impl<'db> ConstrainedTypeVar<'db> { let lower = lower.normalized(db); let upper = upper.normalized(db); - Node::new_constraint(db, ConstrainedTypeVar::new(db, typevar, lower, upper)) + + // We have an (arbitrary) ordering for typevars. If the upper and/or lower bounds are + // typevars, we have to ensure that the bounds are "later" according to that order than the + // typevar being constrained. + // + // In the comments below, we use brackets to indicate which typevar is "earlier", and + // therefore the typevar that the constraint applies to. + match (lower, upper) { + // L ≤ T ≤ L == (T ≤ [L] ≤ T) + (Type::TypeVar(lower), Type::TypeVar(upper)) if lower.is_same_typevar_as(db, upper) => { + let (bound, typevar) = if lower.can_be_bound_for(db, typevar) { + (lower, typevar) + } else { + (typevar, lower) + }; + Node::new_constraint( + db, + ConstrainedTypeVar::new( + db, + typevar, + Type::TypeVar(bound), + Type::TypeVar(bound), + ), + ) + } + + // L ≤ T ≤ U == ([L] ≤ T) && (T ≤ [U]) + (Type::TypeVar(lower), Type::TypeVar(upper)) + if typevar.can_be_bound_for(db, lower) && typevar.can_be_bound_for(db, upper) => + { + let lower = Node::new_constraint( + db, + ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), + ); + let upper = Node::new_constraint( + db, + ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), + ); + lower.and(db, upper) + } + + // L ≤ T ≤ U == ([L] ≤ T) && ([T] ≤ U) + (Type::TypeVar(lower), _) if typevar.can_be_bound_for(db, lower) => { + let lower = Node::new_constraint( + db, + ConstrainedTypeVar::new(db, lower, Type::Never, Type::TypeVar(typevar)), + ); + let upper = Self::new_node(db, typevar, Type::Never, upper); + lower.and(db, upper) + } + + // L ≤ T ≤ U == (L ≤ [T]) && (T ≤ [U]) + (_, Type::TypeVar(upper)) if typevar.can_be_bound_for(db, upper) => { + let lower = Self::new_node(db, typevar, lower, Type::object()); + let upper = Node::new_constraint( + db, + ConstrainedTypeVar::new(db, upper, Type::TypeVar(typevar), Type::object()), + ); + lower.and(db, upper) + } + + _ => Node::new_constraint(db, ConstrainedTypeVar::new(db, typevar, lower, upper)), + } } fn when_true(self) -> ConstraintAssignment<'db> { @@ -308,14 +452,6 @@ impl<'db> ConstrainedTypeVar<'db> { ConstraintAssignment::Negative(self) } - fn contains(self, db: &'db dyn Db, other: Self) -> bool { - if self.typevar(db) != other.typevar(db) { - return false; - } - self.lower(db).is_subtype_of(db, other.lower(db)) - && other.upper(db).is_subtype_of(db, self.upper(db)) - } - /// Defines the ordering of the variables in a constraint set BDD. /// /// If we only care about _correctness_, we can choose any ordering that we want, as long as @@ -329,16 +465,20 @@ impl<'db> ConstrainedTypeVar<'db> { /// simplifications that we perform that operate on constraints with the same typevar, and this /// ensures that we can find all candidate simplifications more easily. fn ordering(self, db: &'db dyn Db) -> impl Ord { - (self.typevar(db), self.as_id()) + (self.typevar(db).identity(db), self.as_id()) } /// Returns whether this constraint implies another — i.e., whether every type that /// satisfies this constraint also satisfies `other`. /// - /// This is used (among other places) to simplify how we display constraint sets, by removing - /// redundant constraints from a clause. + /// This is used to simplify how we display constraint sets, by removing redundant constraints + /// from a clause. fn implies(self, db: &'db dyn Db, other: Self) -> bool { - other.contains(db, self) + if !self.typevar(db).is_same_typevar_as(db, other.typevar(db)) { + return false; + } + other.lower(db).is_subtype_of(db, self.lower(db)) + && self.upper(db).is_subtype_of(db, other.upper(db)) } /// Returns the intersection of two range constraints, or `None` if the intersection is empty. @@ -376,11 +516,32 @@ impl<'db> ConstrainedTypeVar<'db> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let lower = self.constraint.lower(self.db); let upper = self.constraint.upper(self.db); + let typevar = self.constraint.typevar(self.db); if lower.is_equivalent_to(self.db, upper) { + // If this typevar is equivalent to another, output the constraint in a + // consistent alphabetical order, regardless of the salsa ordering that we are + // using the in BDD. + if let Type::TypeVar(bound) = lower { + let bound = bound.identity(self.db).display(self.db).to_string(); + let typevar = typevar.identity(self.db).display(self.db).to_string(); + let (smaller, larger) = if bound < typevar { + (bound, typevar) + } else { + (typevar, bound) + }; + return write!( + f, + "({} {} {})", + smaller, + if self.negated { "≠" } else { "=" }, + larger, + ); + } + return write!( f, "({} {} {})", - self.constraint.typevar(self.db).display(self.db), + typevar.identity(self.db).display(self.db), if self.negated { "≠" } else { "=" }, lower.display(self.db) ); @@ -393,7 +554,7 @@ impl<'db> ConstrainedTypeVar<'db> { if !lower.is_never() { write!(f, "{} ≤ ", lower.display(self.db))?; } - self.constraint.typevar(self.db).display(self.db).fmt(f)?; + typevar.identity(self.db).display(self.db).fmt(f)?; if !upper.is_object() { write!(f, " ≤ {}", upper.display(self.db))?; } @@ -588,6 +749,39 @@ impl<'db> Node<'db> { .or(db, self.negate(db).and(db, else_node)) } + fn when_subtype_of_given( + self, + db: &'db dyn Db, + lhs: Type<'db>, + rhs: Type<'db>, + inferable: InferableTypeVars<'_, 'db>, + ) -> Self { + match (lhs, rhs) { + // When checking subtyping involving a typevar, we project the BDD so that it only + // contains that typevar, and any other typevars that could be its upper/lower bound. + // (That is, other typevars that are "later" in our arbitrary ordering of typevars.) + // + // Having done that, we can turn the subtyping check into a constraint (i.e, "is `T` a + // subtype of `int` becomes the constraint `T ≤ int`), and then check when the BDD + // implies that constraint. + (Type::TypeVar(bound_typevar), _) => { + let constraint = ConstrainedTypeVar::new_node(db, bound_typevar, Type::Never, rhs); + let (simplified, domain) = self.implies(db, constraint).simplify_and_domain(db); + simplified.and(db, domain) + } + + (_, Type::TypeVar(bound_typevar)) => { + let constraint = + ConstrainedTypeVar::new_node(db, bound_typevar, lhs, Type::object()); + let (simplified, domain) = self.implies(db, constraint).simplify_and_domain(db); + simplified.and(db, domain) + } + + // If neither type is a typevar, then we fall back on a normal subtyping check. + _ => lhs.when_subtype_of(db, rhs, inferable).node, + } + } + /// Returns a new BDD that returns the same results as `self`, but with some inputs fixed to /// particular values. (Those variables will not be checked when evaluating the result, and /// will not be present in the result.) @@ -747,26 +941,24 @@ impl<'db> Node<'db> { interior.if_false(db).for_each_constraint(db, f); } + /// Returns a simplified version of a BDD, along with the BDD's domain. + fn simplify_and_domain(self, db: &'db dyn Db) -> (Self, Self) { + match self { + Node::AlwaysTrue | Node::AlwaysFalse => (self, Node::AlwaysTrue), + Node::Interior(interior) => interior.simplify(db), + } + } + /// Simplifies a BDD, replacing constraints with simpler or smaller constraints where possible. fn simplify(self, db: &'db dyn Db) -> Self { - match self { - Node::AlwaysTrue | Node::AlwaysFalse => self, - Node::Interior(interior) => { - let (simplified, _) = interior.simplify(db); - simplified - } - } + let (simplified, _) = self.simplify_and_domain(db); + simplified } /// Returns the domain (the set of allowed inputs) for a BDD. fn domain(self, db: &'db dyn Db) -> Self { - match self { - Node::AlwaysTrue | Node::AlwaysFalse => Node::AlwaysTrue, - Node::Interior(interior) => { - let (_, domain) = interior.simplify(db); - domain - } - } + let (_, domain) = self.simplify_and_domain(db); + domain } /// Returns clauses describing all of the variable assignments that cause this BDD to evaluate @@ -1079,10 +1271,10 @@ impl<'db> InteriorNode<'db> { // Containment: The range of one constraint might completely contain the range of the // other. If so, there are several potential simplifications. - let larger_smaller = if left_constraint.contains(db, right_constraint) { - Some((left_constraint, right_constraint)) - } else if right_constraint.contains(db, left_constraint) { + let larger_smaller = if left_constraint.implies(db, right_constraint) { Some((right_constraint, left_constraint)) + } else if right_constraint.implies(db, left_constraint) { + Some((left_constraint, right_constraint)) } else { None }; @@ -1313,8 +1505,8 @@ impl<'db> ConstraintAssignment<'db> { /// Returns whether this constraint implies another — i.e., whether every type that /// satisfies this constraint also satisfies `other`. /// - /// This is used (among other places) to simplify how we display constraint sets, by removing - /// redundant constraints from a clause. + /// This is used to simplify how we display constraint sets, by removing redundant constraints + /// from a clause. fn implies(self, db: &'db dyn Db, other: Self) -> bool { match (self, other) { // For two positive constraints, one range has to fully contain the other; the smaller @@ -1641,10 +1833,10 @@ mod tests { let u = BoundTypeVarInstance::synthetic(&db, "U", TypeVarVariance::Invariant); let bool_type = KnownClass::Bool.to_instance(&db); let str_type = KnownClass::Str.to_instance(&db); - let t_str = ConstraintSet::range(&db, str_type, t.identity(&db), str_type); - let t_bool = ConstraintSet::range(&db, bool_type, t.identity(&db), bool_type); - let u_str = ConstraintSet::range(&db, str_type, u.identity(&db), str_type); - let u_bool = ConstraintSet::range(&db, bool_type, u.identity(&db), bool_type); + let t_str = ConstraintSet::range(&db, str_type, t, str_type); + let t_bool = ConstraintSet::range(&db, bool_type, t, bool_type); + let u_str = ConstraintSet::range(&db, str_type, u, str_type); + let u_bool = ConstraintSet::range(&db, bool_type, u, bool_type); let constraints = (t_str.or(&db, || t_bool)).and(&db, || u_str.or(&db, || u_bool)); let actual = constraints.node.display_graph(&db, &"").to_string(); assert_eq!(actual, expected); diff --git a/crates/ty_python_semantic/src/types/function.rs b/crates/ty_python_semantic/src/types/function.rs index 87870e61b8..9aae4aef02 100644 --- a/crates/ty_python_semantic/src/types/function.rs +++ b/crates/ty_python_semantic/src/types/function.rs @@ -1299,6 +1299,8 @@ pub enum KnownFunction { IsEquivalentTo, /// `ty_extensions.is_subtype_of` IsSubtypeOf, + /// `ty_extensions.is_subtype_of_given` + IsSubtypeOfGiven, /// `ty_extensions.is_assignable_to` IsAssignableTo, /// `ty_extensions.is_disjoint_from` @@ -1391,6 +1393,7 @@ impl KnownFunction { | Self::IsSingleValued | Self::IsSingleton | Self::IsSubtypeOf + | Self::IsSubtypeOfGiven | Self::GenericContext | Self::DunderAllNames | Self::EnumMembers @@ -1783,7 +1786,7 @@ impl KnownFunction { return; }; - let constraints = ConstraintSet::range(db, *lower, typevar.identity(db), *upper); + let constraints = ConstraintSet::range(db, *lower, *typevar, *upper); let tracked = TrackedConstraintSet::new(db, constraints); overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet( tracked, @@ -1796,8 +1799,7 @@ impl KnownFunction { return; }; - let constraints = - ConstraintSet::negated_range(db, *lower, typevar.identity(db), *upper); + let constraints = ConstraintSet::negated_range(db, *lower, *typevar, *upper); let tracked = TrackedConstraintSet::new(db, constraints); overload.set_return_type(Type::KnownInstance(KnownInstanceType::ConstraintSet( tracked, @@ -1892,6 +1894,7 @@ pub(crate) mod tests { KnownFunction::IsSingleton | KnownFunction::IsSubtypeOf + | KnownFunction::IsSubtypeOfGiven | KnownFunction::GenericContext | KnownFunction::DunderAllNames | KnownFunction::EnumMembers diff --git a/crates/ty_python_semantic/src/types/type_ordering.rs b/crates/ty_python_semantic/src/types/type_ordering.rs index 7b52a45e8d..e45e0c9ba5 100644 --- a/crates/ty_python_semantic/src/types/type_ordering.rs +++ b/crates/ty_python_semantic/src/types/type_ordering.rs @@ -1,5 +1,7 @@ use std::cmp::Ordering; +use salsa::plumbing::AsId; + use crate::{db::Db, types::bound_super::SuperOwnerKind}; use super::{ @@ -137,7 +139,9 @@ pub(super) fn union_or_intersection_elements_ordering<'db>( (Type::ProtocolInstance(_), _) => Ordering::Less, (_, Type::ProtocolInstance(_)) => Ordering::Greater, - (Type::TypeVar(left), Type::TypeVar(right)) => left.cmp(right), + // This is one place where we want to compare the typevar identities directly, instead of + // falling back on `is_same_typevar_as` or `can_be_bound_for`. + (Type::TypeVar(left), Type::TypeVar(right)) => left.as_id().cmp(&right.as_id()), (Type::TypeVar(_), _) => Ordering::Less, (_, Type::TypeVar(_)) => Ordering::Greater, diff --git a/crates/ty_vendored/ty_extensions/ty_extensions.pyi b/crates/ty_vendored/ty_extensions/ty_extensions.pyi index 0fe23b3535..be9b4ebff4 100644 --- a/crates/ty_vendored/ty_extensions/ty_extensions.pyi +++ b/crates/ty_vendored/ty_extensions/ty_extensions.pyi @@ -63,26 +63,35 @@ def negated_range_constraint( # Ideally, these would be annotated using `TypeForm`, but that has not been # standardized yet (https://peps.python.org/pep-0747). def is_equivalent_to(type_a: Any, type_b: Any) -> ConstraintSet: - """Returns a constraint that is satisfied when `type_a` and `type_b` are + """Returns a constraint set that is satisfied when `type_a` and `type_b` are `equivalent`_ types. .. _equivalent: https://typing.python.org/en/latest/spec/glossary.html#term-equivalent """ def is_subtype_of(ty: Any, of: Any) -> ConstraintSet: - """Returns a constraint that is satisfied when `ty` is a `subtype`_ of `of`. + """Returns a constraint set that is satisfied when `ty` is a `subtype`_ of `of`. + + .. _subtype: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence + """ + +def is_subtype_of_given( + constraints: bool | ConstraintSet, ty: Any, of: Any +) -> ConstraintSet: + """Returns a constraint set that is satisfied when `ty` is a `subtype`_ of `of`, + assuming that all of the constraints in `constraints` hold. .. _subtype: https://typing.python.org/en/latest/spec/concepts.html#subtype-supertype-and-type-equivalence """ def is_assignable_to(ty: Any, to: Any) -> ConstraintSet: - """Returns a constraint that is satisfied when `ty` is `assignable`_ to `to`. + """Returns a constraint set that is satisfied when `ty` is `assignable`_ to `to`. .. _assignable: https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation """ def is_disjoint_from(type_a: Any, type_b: Any) -> ConstraintSet: - """Returns a constraint that is satisfied when `type_a` and `type_b` are disjoint types. + """Returns a constraint set that is satisfied when `type_a` and `type_b` are disjoint types. Two types are disjoint if they have no inhabitants in common. """