[ty] Add new "constraint implication" typing relation (#21010)

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.

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

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

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(

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 =

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<T> {
@@ -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<bool> 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);

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

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,
 

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.
     """