move implementation

crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md

@@ -208,30 +208,18 @@ def given_constraints[T]():
     static_assert(not ConstraintSet.always().implies_subtype_of(Covariant[T], Covariant[str]))
 
     # These are vacuously true; false implies anything
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[int]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[bool]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Covariant[T], Covariant[str]))
 
     # For a covariant typevar, (T ≤ int) implies that (Covariant[T] ≤ Covariant[int]).
     given_int = ConstraintSet.range(Never, T, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
 
     given_bool = ConstraintSet.range(Never, T, bool)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_bool.implies_subtype_of(Covariant[T], Covariant[int]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_bool.implies_subtype_of(Covariant[T], Covariant[bool]))
     static_assert(not given_bool.implies_subtype_of(Covariant[T], Covariant[str]))
 
@@ -239,8 +227,6 @@ def mutually_constrained[T, U]():
     # If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Covariant[T] ≤ Covariant[int]).
     given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
@@ -248,8 +234,6 @@ def mutually_constrained[T, U]():
     # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Covariant[T] ≤ Covariant[int]).
     given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Covariant[T], Covariant[int]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[bool]))
     static_assert(not given_int.implies_subtype_of(Covariant[T], Covariant[str]))
@@ -268,28 +252,18 @@ def given_constraints[T]():
     static_assert(not ConstraintSet.always().implies_subtype_of(Contravariant[str], Contravariant[T]))
 
     # These are vacuously true; false implies anything
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[int], Contravariant[T]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[bool], Contravariant[T]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Contravariant[str], Contravariant[T]))
 
     # For a contravariant typevar, (T ≤ int) implies that (Contravariant[int] ≤ Contravariant[T]).
     # (The order of the comparison is reversed because of contravariance.)
     given_int = ConstraintSet.range(Never, T, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
 
     given_bool = ConstraintSet.range(Never, T, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_bool.implies_subtype_of(Contravariant[int], Contravariant[T]))
     # TODO: no error
     # error: [static-assert-error]
@@ -300,8 +274,6 @@ def mutually_constrained[T, U]():
     # If (T = U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Contravariant[int] ≤ Contravariant[T]).
     given_int = ConstraintSet.range(U, T, U) & ConstraintSet.range(Never, U, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
@@ -309,8 +281,6 @@ def mutually_constrained[T, U]():
     # If (T ≤ U ∧ U ≤ int), then (T ≤ int) must be true as well, and therefore
     # (Contravariant[int] ≤ Contravariant[T]).
     given_int = ConstraintSet.range(Never, T, U) & ConstraintSet.range(Never, U, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Contravariant[int], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[bool], Contravariant[T]))
     static_assert(not given_int.implies_subtype_of(Contravariant[str], Contravariant[T]))
@@ -333,14 +303,8 @@ def given_constraints[T]():
     static_assert(not ConstraintSet.always().implies_subtype_of(Invariant[T], Invariant[str]))
 
     # These are vacuously true; false implies anything
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[int]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[bool]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(ConstraintSet.never().implies_subtype_of(Invariant[T], Invariant[str]))
 
     # For an invariant typevar, (T ≤ int) does not imply that (Invariant[T] ≤ Invariant[int]).
@@ -356,11 +320,7 @@ def given_constraints[T]():
 
     # But (T = int) does imply both.
     given_int = ConstraintSet.range(int, T, int)
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Invariant[T], Invariant[int]))
-    # TODO: no error
-    # error: [static-assert-error]
     static_assert(given_int.implies_subtype_of(Invariant[int], Invariant[T]))
     static_assert(not given_int.implies_subtype_of(Invariant[bool], Invariant[T]))
     static_assert(not given_int.implies_subtype_of(Invariant[T], Invariant[bool]))

crates/ty_python_semantic/src/types.rs

@@ -1618,6 +1618,25 @@ impl<'db> Type<'db> {
         self.has_relation_to(db, target, inferable, TypeRelation::Subtyping)
     }
 
+    /// Return the constraints under which this type is a subtype of type `target`, assuming that
+    /// all of the restrictions in `constraints` hold.
+    ///
+    /// See [`TypeRelation::ConstraintImplication`] for more details.
+    fn when_subtype_of_given(
+        self,
+        db: &'db dyn Db,
+        target: Type<'db>,
+        constraints: ConstraintSet<'db>,
+        inferable: InferableTypeVars<'_, 'db>,
+    ) -> ConstraintSet<'db> {
+        self.has_relation_to(
+            db,
+            target,
+            inferable,
+            TypeRelation::ConstraintImplication(constraints),
+        )
+    }
+
     /// Return true if this type is assignable to type `target`.
     ///
     /// See [`TypeRelation::Assignability`] for more details.
@@ -1679,6 +1698,14 @@ impl<'db> Type<'db> {
             return ConstraintSet::from(true);
         }
 
+        // Handle constraint implication first. If either `self` or `target` is a typevar, check
+        // the constraint set to see if the corresponding constraint is satisfied.
+        if let TypeRelation::ConstraintImplication(constraints) = relation
+            && (self.is_type_var() || target.is_type_var())
+        {
+            return constraints.when_subtype_of_given(db, self, target);
+        }
+
         match (self, target) {
             // Everything is a subtype of `object`.
             (_, Type::NominalInstance(instance)) if instance.is_object() => {
@@ -10319,21 +10346,36 @@ pub(crate) enum TypeRelation<'db> {
     /// This relationship tests whether one type is a [subtype][Self::Subtyping] 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
+    /// For concrete types (types that do not contain typevars), this relationship is the same as
-    /// type is any fully static type that does not contain a typevar.) Moreover, for concrete
+    /// [subtyping][Self::Subtyping]. (Constraint sets place restrictions on typevars, so if you
-    /// types, the answer does not depend on which constraint set we are considering. `bool` is a
+    /// are not comparing typevars, the constraint set can have no effect on whether subtyping
-    /// subtype of `int` no matter what types any typevars are specialized to — and even if
+    /// holds.)
-    /// there isn't a valid specialization for the typevars we are considering.
     ///
-    /// The interesting case is typevars. The other typing relationships (TODO: will) all "punt" on
+    /// If you're comparing a typevar, we have to consider what restrictions the constraint set
-    /// the question when considering a typevar, by translating the desired relationship into a
+    /// places on that typevar to determine if subtyping holds. For instance, if you want to check
-    /// constraint set. At some point, though, we need to resolve a constraint set; at that point,
+    /// whether `T ≤ int`, then answer will depend on what constraint set you are considering:
-    /// we can no longer punt on the question. Unlike with concrete types, the answer will depend
+    ///
-    /// on the constraint set that we are considering. For instance, a constraint set that requires
+    /// ```text
-    /// `T ≤ bool` implies that `T` is a subtype of `int`, since every valid specialization
+    /// when_subtype_of_given(T ≤ bool, T, int) ⇒ true
-    /// satisfies `T ≤ int`. But the reverse is not true: the constraint set `T ≤ int` does _not_
+    /// when_subtype_of_given(T ≤ int, T, int)  ⇒ true
-    /// imply that `T` is a subtype of `bool`, since `T = int` is a valid specialization, and `int`
+    /// when_subtype_of_given(T ≤ str, T, int)  ⇒ false
-    /// is not a subtype of `bool`.
+    /// ```
+    ///
+    /// 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!)
     ConstraintImplication(ConstraintSet<'db>),
 }
 

crates/ty_python_semantic/src/types/call/bind.rs

@@ -1179,10 +1179,10 @@ impl<'db> Bindings<'db> {
                             continue;
                         };
 
-                        let result = tracked.constraints(db).when_subtype_of_given(
+                        let result = ty_a.when_subtype_of_given(
                             db,
-                            *ty_a,
                             *ty_b,
+                            tracked.constraints(db),
                             InferableTypeVars::None,
                         );
                         let tracked = TrackedConstraintSet::new(db, result);

crates/ty_python_semantic/src/types/constraints.rs

@@ -216,47 +216,16 @@ impl<'db> ConstraintSet<'db> {
     }
 
     /// Returns the constraints under which `lhs` is a subtype of `rhs`, assuming that the
-    /// constraints in this constraint set hold.
+    /// constraints in this constraint set hold. Panics if neither of the types being compared are
-    ///
+    /// a typevar. (That case is handled by `Type::has_relation_to`.)
-    /// 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),
+            node: self.node.when_subtype_of_given(db, lhs, rhs),
         }
     }
 
@@ -830,13 +799,7 @@ impl<'db> Node<'db> {
         simplified.and(db, domain)
     }
 
-    fn when_subtype_of_given(
+    fn when_subtype_of_given(self, db: &'db dyn Db, lhs: Type<'db>, rhs: Type<'db>) -> Self {
-        self,
-        db: &'db dyn Db,
-        lhs: Type<'db>,
-        rhs: Type<'db>,
-        inferable: InferableTypeVars<'_, 'db>,
-    ) -> Self {
         // When checking subtyping involving a typevar, 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.
@@ -847,8 +810,7 @@ impl<'db> Node<'db> {
             (_, Type::TypeVar(bound_typevar)) => {
                 ConstrainedTypeVar::new_node(db, bound_typevar, lhs, Type::object())
             }
-            // If neither type is a typevar, then we fall back on a normal subtyping check.
+            _ => panic!("at least one type should be a typevar"),
-            _ => return lhs.when_subtype_of(db, rhs, inferable).node,
         };
 
         self.satisfies(db, constraint)