[ty] Add new "constraint implication" typing relation

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 =