diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md index e4f8d2267c..bb24e8c90d 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/implies_subtype_of.md +++ b/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])) diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index cc8df42add..9b5dd95238 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/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 - /// type is any fully static type that does not contain a typevar.) 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. + /// For concrete types (types that do not contain typevars), this relationship is the same as + /// [subtyping][Self::Subtyping]. (Constraint sets place restrictions on typevars, so if you + /// are not comparing typevars, the constraint set can have no effect on whether subtyping + /// holds.) /// - /// 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. For instance, a constraint set that requires - /// `T ≤ bool` implies that `T` is a subtype of `int`, since every valid specialization - /// satisfies `T ≤ int`. But the reverse is not true: the constraint set `T ≤ int` does _not_ - /// imply that `T` is a subtype of `bool`, since `T = int` is a valid specialization, and `int` - /// is not a subtype of `bool`. + /// 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!) ConstraintImplication(ConstraintSet<'db>), } diff --git a/crates/ty_python_semantic/src/types/call/bind.rs b/crates/ty_python_semantic/src/types/call/bind.rs index 423783b420..c017ee68d4 100644 --- a/crates/ty_python_semantic/src/types/call/bind.rs +++ b/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); diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index f3230214a7..1595e609c6 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/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. - /// - /// 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!) + /// 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`.) 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( - self, - db: &'db dyn Db, - lhs: Type<'db>, - rhs: Type<'db>, - inferable: InferableTypeVars<'_, 'db>, - ) -> Self { + fn when_subtype_of_given(self, db: &'db dyn Db, lhs: Type<'db>, rhs: Type<'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. - _ => return lhs.when_subtype_of(db, rhs, inferable).node, + _ => panic!("at least one type should be a typevar"), }; self.satisfies(db, constraint)