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 1a72da9464..1da443c12f 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 @@ -45,31 +45,27 @@ def even_given_unsatisfiable_constraints(): ## 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. +The interesting case is typevars. The other typing relationships 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] + # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ bool)] reveal_type(is_assignable_to(T, bool)) - # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ int] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ int)] reveal_type(is_assignable_to(T, int)) - # revealed: ty_extensions.ConstraintSet[always] + # revealed: ty_extensions.ConstraintSet[(T@assignability = *)] reveal_type(is_assignable_to(T, object)) def subtyping[T](): - # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ bool] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ bool)] reveal_type(is_subtype_of(T, bool)) - # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ int] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ int)] reveal_type(is_subtype_of(T, int)) - # revealed: ty_extensions.ConstraintSet[always] + # revealed: ty_extensions.ConstraintSet[(T@subtyping = *)] reveal_type(is_subtype_of(T, object)) ``` @@ -88,49 +84,37 @@ class Contravariant[T]: pass def assignability[T](): - # aka [T@assignability ≤ object], which is always satisfiable - # revealed: ty_extensions.ConstraintSet[always] + # revealed: ty_extensions.ConstraintSet[(T@assignability = *)] reveal_type(is_assignable_to(T, Any)) - # aka [Never ≤ T@assignability], which is always satisfiable - # revealed: ty_extensions.ConstraintSet[always] + # revealed: ty_extensions.ConstraintSet[(T@assignability = *)] reveal_type(is_assignable_to(Any, T)) - # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Covariant[object]] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ Covariant[object])] reveal_type(is_assignable_to(T, Covariant[Any])) - # TODO: revealed: ty_extensions.ConstraintSet[Covariant[Never] ≤ T@assignability] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(Covariant[Never] ≤ T@assignability)] reveal_type(is_assignable_to(Covariant[Any], T)) - # TODO: revealed: ty_extensions.ConstraintSet[T@assignability ≤ Contravariant[Never]] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@assignability ≤ Contravariant[Never])] reveal_type(is_assignable_to(T, Contravariant[Any])) - # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[object] ≤ T@assignability] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(Contravariant[object] ≤ T@assignability)] reveal_type(is_assignable_to(Contravariant[Any], T)) def subtyping[T](): - # aka [T@assignability ≤ object], which is always satisfiable - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping = Never)] reveal_type(is_subtype_of(T, Any)) - # aka [Never ≤ T@assignability], which is always satisfiable - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping = object)] reveal_type(is_subtype_of(Any, T)) - # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Covariant[Never]] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ Covariant[Never])] reveal_type(is_subtype_of(T, Covariant[Any])) - # TODO: revealed: ty_extensions.ConstraintSet[Covariant[object] ≤ T@subtyping] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(Covariant[object] ≤ T@subtyping)] reveal_type(is_subtype_of(Covariant[Any], T)) - # TODO: revealed: ty_extensions.ConstraintSet[T@subtyping ≤ Contravariant[object]] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(T@subtyping ≤ Contravariant[object])] reveal_type(is_subtype_of(T, Contravariant[Any])) - # TODO: revealed: ty_extensions.ConstraintSet[Contravariant[Never] ≤ T@subtyping] - # revealed: ty_extensions.ConstraintSet[never] + # revealed: ty_extensions.ConstraintSet[(Contravariant[Never] ≤ T@subtyping)] reveal_type(is_subtype_of(Contravariant[Any], T)) ``` diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md index 3ac4f9b652..79716ad19a 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_assignable_to.md @@ -1248,14 +1248,10 @@ def identity[T](t: T) -> T: static_assert(is_assignable_to(TypeOf[identity], Callable[[int], int])) static_assert(is_assignable_to(TypeOf[identity], Callable[[str], str])) -# TODO: no error -# error: [static-assert-error] static_assert(not is_assignable_to(TypeOf[identity], Callable[[str], int])) static_assert(is_assignable_to(CallableTypeOf[identity], Callable[[int], int])) static_assert(is_assignable_to(CallableTypeOf[identity], Callable[[str], str])) -# TODO: no error -# error: [static-assert-error] static_assert(not is_assignable_to(CallableTypeOf[identity], Callable[[str], int])) ``` diff --git a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md index a2b9ca89d0..c756ecf5f7 100644 --- a/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md +++ b/crates/ty_python_semantic/resources/mdtest/type_properties/is_subtype_of.md @@ -2221,23 +2221,11 @@ from ty_extensions import CallableTypeOf, TypeOf, is_subtype_of, static_assert def identity[T](t: T) -> T: return t -# TODO: Confusingly, these are not the same results as the corresponding checks in -# is_assignable_to.md, even though all of these types are fully static. We have some heuristics that -# currently conflict with each other, that we are in the process of removing with the constraint set -# work. -# TODO: no error -# error: [static-assert-error] static_assert(is_subtype_of(TypeOf[identity], Callable[[int], int])) -# TODO: no error -# error: [static-assert-error] static_assert(is_subtype_of(TypeOf[identity], Callable[[str], str])) static_assert(not is_subtype_of(TypeOf[identity], Callable[[str], int])) -# TODO: no error -# error: [static-assert-error] static_assert(is_subtype_of(CallableTypeOf[identity], Callable[[int], int])) -# TODO: no error -# error: [static-assert-error] static_assert(is_subtype_of(CallableTypeOf[identity], Callable[[str], str])) static_assert(not is_subtype_of(CallableTypeOf[identity], Callable[[str], int])) ``` diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index cd483f2220..9424fbb72b 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -1756,6 +1756,29 @@ impl<'db> Type<'db> { } match (self, target) { + // Two identical typevars must always solve to the same type, so they are always + // subtypes of each other and assignable to each other. + // + // Note that this is not handled by the early return at the beginning of this method, + // 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_same_typevar_as(db, rhs_bound_typevar) => + { + ConstraintSet::from(true) + } + + // A typevar satisfies a relation when...it satisfies the relation. Yes that's a + // tautology! We're moving the caller's subtyping/assignability requirement into a + // constraint set. If the typevar has an upper bound or constraints, then the relation + // only has to hold when the typevar has a valid specialization (i.e., one that + // satisfies the upper bound/constraints). + (Type::TypeVar(bound_typevar), _) => { + ConstraintSet::constrain_typevar(db, bound_typevar, Type::Never, target, relation) + } + (_, Type::TypeVar(bound_typevar)) => { + ConstraintSet::constrain_typevar(db, bound_typevar, self, Type::object(), relation) + } + // Everything is a subtype of `object`. (_, Type::NominalInstance(instance)) if instance.is_object() => { ConstraintSet::from(true) @@ -1859,130 +1882,6 @@ impl<'db> Type<'db> { }, }), - // In general, a TypeVar `T` is not a subtype of a type `S` unless one of the two conditions is satisfied: - // 1. `T` is a bound TypeVar and `T`'s upper bound is a subtype of `S`. - // TypeVars without an explicit upper bound are treated as having an implicit upper bound of `object`. - // 2. `T` is a constrained TypeVar and all of `T`'s constraints are subtypes of `S`. - // - // However, there is one exception to this general rule: for any given typevar `T`, - // `T` will always be a subtype of any union containing `T`. - // A similar rule applies in reverse to intersection types. - (Type::TypeVar(bound_typevar), Type::Union(union)) - if !bound_typevar.is_inferable(db, inferable) - && union.elements(db).contains(&self) => - { - ConstraintSet::from(true) - } - (Type::Intersection(intersection), Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && intersection.positive(db).contains(&target) => - { - ConstraintSet::from(true) - } - (Type::Intersection(intersection), Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && intersection.negative(db).contains(&target) => - { - ConstraintSet::from(false) - } - - // Two identical typevars must always solve to the same type, so they are always - // subtypes of each other and assignable to each other. - // - // Note that this is not handled by the early return at the beginning of this method, - // 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.is_same_typevar_as(db, rhs_bound_typevar) => - { - ConstraintSet::from(true) - } - - // A fully static typevar is a subtype of its upper bound, and to something similar to - // the union of its constraints. An unbound, unconstrained, fully static typevar has an - // implicit upper bound of `object` (which is handled above). - (Type::TypeVar(bound_typevar), _) - if !bound_typevar.is_inferable(db, inferable) - && bound_typevar.typevar(db).bound_or_constraints(db).is_some() => - { - match bound_typevar.typevar(db).bound_or_constraints(db) { - None => unreachable!(), - Some(TypeVarBoundOrConstraints::UpperBound(bound)) => bound - .has_relation_to_impl( - db, - target, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ), - Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { - constraints.elements(db).iter().when_all(db, |constraint| { - constraint.has_relation_to_impl( - db, - target, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - } - } - } - - // If the typevar is constrained, there must be multiple constraints, and the typevar - // might be specialized to any one of them. However, the constraints do not have to be - // disjoint, which means an lhs type might be a subtype of all of the constraints. - (_, Type::TypeVar(bound_typevar)) - if !bound_typevar.is_inferable(db, inferable) - && !bound_typevar - .typevar(db) - .constraints(db) - .when_some_and(|constraints| { - constraints.iter().when_all(db, |constraint| { - self.has_relation_to_impl( - db, - *constraint, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - }) - .is_never_satisfied(db) => - { - // TODO: The repetition here isn't great, but we really need the fallthrough logic, - // where this arm only engages if it returns true (or in the world of constraints, - // not false). Once we're using real constraint sets instead of bool, we should be - // able to simplify the typevar logic. - bound_typevar - .typevar(db) - .constraints(db) - .when_some_and(|constraints| { - constraints.iter().when_all(db, |constraint| { - self.has_relation_to_impl( - db, - *constraint, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - }) - } - - (Type::TypeVar(bound_typevar), _) if bound_typevar.is_inferable(db, inferable) => { - // The implicit lower bound of a typevar is `Never`, which means - // that it is always assignable to any other type. - - // TODO: record the unification constraints - - ConstraintSet::from(true) - } - // `Never` is the bottom type, the empty set. (_, Type::Never) => ConstraintSet::from(false), @@ -2074,55 +1973,6 @@ impl<'db> Type<'db> { }) } - // Other than the special cases checked above, no other types are a subtype of a - // typevar, since there's no guarantee what type the typevar will be specialized to. - // (If the typevar is bounded, it might be specialized to a smaller type than the - // bound. This is true even if the bound is a final class, since the typevar can still - // be specialized to `Never`.) - (_, Type::TypeVar(bound_typevar)) if !bound_typevar.is_inferable(db, inferable) => { - ConstraintSet::from(false) - } - - (_, Type::TypeVar(typevar)) - if typevar.is_inferable(db, inferable) - && relation.is_assignability() - && typevar.typevar(db).upper_bound(db).is_none_or(|bound| { - !self - .has_relation_to_impl( - db, - bound, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - .is_never_satisfied(db) - }) => - { - // TODO: record the unification constraints - - typevar.typevar(db).upper_bound(db).when_none_or(|bound| { - self.has_relation_to_impl( - db, - bound, - inferable, - relation, - relation_visitor, - disjointness_visitor, - ) - }) - } - - // TODO: Infer specializations here - (_, Type::TypeVar(bound_typevar)) if bound_typevar.is_inferable(db, inferable) => { - ConstraintSet::from(false) - } - (Type::TypeVar(bound_typevar), _) => { - // All inferable cases should have been handled above - assert!(!bound_typevar.is_inferable(db, inferable)); - ConstraintSet::from(false) - } - // Note that the definition of `Type::AlwaysFalsy` depends on the return value of `__bool__`. // If `__bool__` always returns True or False, it can be treated as a subtype of `AlwaysTruthy` or `AlwaysFalsy`, respectively. (left, Type::AlwaysFalsy) => ConstraintSet::from(left.bool(db).is_always_false()), diff --git a/crates/ty_python_semantic/src/types/constraints.rs b/crates/ty_python_semantic/src/types/constraints.rs index 744910f7d1..c409cd8c6e 100644 --- a/crates/ty_python_semantic/src/types/constraints.rs +++ b/crates/ty_python_semantic/src/types/constraints.rs @@ -349,11 +349,11 @@ impl<'db> ConstraintSet<'db> { /// constraint set have valid specializations, according to any upper bound or constraints they /// might have. pub(crate) fn limit_to_valid_specializations(self, db: &'db dyn Db) -> Self { - let mut result = self.node; + let mut result = self; self.node.for_each_constraint(db, &mut |constraint| { - result = result.and(db, constraint.typevar(db).valid_specializations(db)); + result.intersect(db, constraint.typevar(db).valid_specializations(db)); }); - Self { node: result } + result } /// Updates this constraint set to hold the union of itself and another constraint set. @@ -1072,7 +1072,7 @@ impl<'db> Node<'db> { // If the typevar is in inferable position, we need to verify that some valid // specialization satisfies the constraint set. let valid_specializations = typevar.valid_specializations(db); - if !some_specialization_satisfies(valid_specializations) { + if !some_specialization_satisfies(valid_specializations.node) { return false; } } else { @@ -3041,7 +3041,7 @@ impl<'db> BoundTypeVarInstance<'db> { /// Returns the valid specializations of a typevar. This is used when checking a constraint set /// when this typevar is in inferable position, where we only need _some_ specialization to /// satisfy the constraint set. - fn valid_specializations(self, db: &'db dyn Db) -> Node<'db> { + pub(crate) fn valid_specializations(self, db: &'db dyn Db) -> ConstraintSet<'db> { // For gradual upper bounds and constraints, we are free to choose any materialization that // makes the check succeed. In inferable positions, it is most helpful to choose a // materialization that is as permissive as possible, since that maximizes the number of @@ -3053,10 +3053,11 @@ impl<'db> BoundTypeVarInstance<'db> { // that _some_ valid specialization satisfies the constraint set, it's correct for us to // return the range of valid materializations that we can choose from. match self.typevar(db).bound_or_constraints(db) { - None => Node::AlwaysTrue, + None => ConstraintSet::from(true), Some(TypeVarBoundOrConstraints::UpperBound(bound)) => { let bound = bound.top_materialization(db); - ConstrainedTypeVar::new_node(db, self, Type::Never, bound) + let node = ConstrainedTypeVar::new_node(db, self, Type::Never, bound); + ConstraintSet { node } } Some(TypeVarBoundOrConstraints::Constraints(constraints)) => { let mut specializations = Node::AlwaysFalse; @@ -3068,7 +3069,9 @@ impl<'db> BoundTypeVarInstance<'db> { ConstrainedTypeVar::new_node(db, self, constraint_lower, constraint_upper), ); } - specializations + ConstraintSet { + node: specializations, + } } } } @@ -3142,7 +3145,7 @@ impl<'db> GenericContext<'db> { let abstracted = self .variables(db) .fold(constraints.node, |constraints, bound_typevar| { - constraints.and(db, bound_typevar.valid_specializations(db)) + constraints.and(db, bound_typevar.valid_specializations(db).node) }); // Then we find all of the "representative types" for each typevar in the constraint set.