From c6f4929cdc596d0b0e0018216fc29b23a8621a92 Mon Sep 17 00:00:00 2001 From: Alex Waygood Date: Wed, 7 May 2025 16:50:22 +0100 Subject: [PATCH] [ty] fix assigning a typevar to a union with itself (#17910) Co-authored-by: Carl Meyer --- .../mdtest/generics/pep695/variables.md | 101 ++++++++++++++++++ crates/ty_python_semantic/src/types.rs | 94 +++++++++------- 2 files changed, 159 insertions(+), 36 deletions(-) diff --git a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md index 2b921a3c3b..17d5c706f0 100644 --- a/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md +++ b/crates/ty_python_semantic/resources/mdtest/generics/pep695/variables.md @@ -320,6 +320,107 @@ def two_final_constrained[T: (FinalClass, AnotherFinalClass), U: (FinalClass, An static_assert(not is_subtype_of(U, T)) ``` +A bound or constrained typevar is a subtype of itself in a union: + +```py +def union[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None: + static_assert(is_assignable_to(T, T | None)) + static_assert(is_assignable_to(U, U | None)) + + static_assert(is_subtype_of(T, T | None)) + static_assert(is_subtype_of(U, U | None)) +``` + +And an intersection of a typevar with another type is always a subtype of the TypeVar: + +```py +from ty_extensions import Intersection, Not, is_disjoint_from + +class A: ... + +def inter[T: Base, U: (Base, Unrelated)](t: T, u: U) -> None: + static_assert(is_assignable_to(Intersection[T, Unrelated], T)) + static_assert(is_subtype_of(Intersection[T, Unrelated], T)) + + static_assert(is_assignable_to(Intersection[U, A], U)) + static_assert(is_subtype_of(Intersection[U, A], U)) + + # TODO: these should pass + static_assert(is_disjoint_from(Not[T], T)) # error: [static-assert-error] + static_assert(is_disjoint_from(T, Not[T])) # error: [static-assert-error] + static_assert(is_disjoint_from(Not[U], U)) # error: [static-assert-error] + static_assert(is_disjoint_from(U, Not[U])) # error: [static-assert-error] +``` + +## Equivalence + +A fully static `TypeVar` is always equivalent to itself, but never to another `TypeVar`, since there +is no guarantee that they will be specialized to the same type. (This is true even if both typevars +are bounded by the same final class, since you can specialize the typevars to `Never` in addition to +that final class.) + +```py +from typing import final +from ty_extensions import is_equivalent_to, static_assert, is_gradual_equivalent_to + +@final +class FinalClass: ... + +@final +class SecondFinalClass: ... + +def f[A, B, C: FinalClass, D: FinalClass, E: (FinalClass, SecondFinalClass), F: (FinalClass, SecondFinalClass)](): + static_assert(is_equivalent_to(A, A)) + static_assert(is_equivalent_to(B, B)) + static_assert(is_equivalent_to(C, C)) + static_assert(is_equivalent_to(D, D)) + static_assert(is_equivalent_to(E, E)) + static_assert(is_equivalent_to(F, F)) + + static_assert(is_gradual_equivalent_to(A, A)) + static_assert(is_gradual_equivalent_to(B, B)) + static_assert(is_gradual_equivalent_to(C, C)) + static_assert(is_gradual_equivalent_to(D, D)) + static_assert(is_gradual_equivalent_to(E, E)) + static_assert(is_gradual_equivalent_to(F, F)) + + static_assert(not is_equivalent_to(A, B)) + static_assert(not is_equivalent_to(C, D)) + static_assert(not is_equivalent_to(E, F)) + + static_assert(not is_gradual_equivalent_to(A, B)) + static_assert(not is_gradual_equivalent_to(C, D)) + static_assert(not is_gradual_equivalent_to(E, F)) +``` + +TypeVars which have non-fully-static bounds or constraints do not participate in equivalence +relations, but do participate in gradual equivalence relations. + +```py +from typing import final, Any +from ty_extensions import is_equivalent_to, static_assert, is_gradual_equivalent_to + +# fmt: off + +def f[ + A: tuple[Any], + B: tuple[Any], + C: (tuple[Any], tuple[Any, Any]), + D: (tuple[Any], tuple[Any, Any]) +](): + static_assert(not is_equivalent_to(A, A)) + static_assert(not is_equivalent_to(B, B)) + static_assert(not is_equivalent_to(C, C)) + static_assert(not is_equivalent_to(D, D)) + + static_assert(is_gradual_equivalent_to(A, A)) + static_assert(is_gradual_equivalent_to(B, B)) + static_assert(is_gradual_equivalent_to(C, C)) + static_assert(is_gradual_equivalent_to(D, D)) + +# fmt: on +``` + ## Singletons and single-valued types (Note: for simplicity, all of the prose in this section refers to _singleton_ types, but all of the diff --git a/crates/ty_python_semantic/src/types.rs b/crates/ty_python_semantic/src/types.rs index 658aface9a..7b26a77dc6 100644 --- a/crates/ty_python_semantic/src/types.rs +++ b/crates/ty_python_semantic/src/types.rs @@ -997,12 +997,24 @@ impl<'db> Type<'db> { // Everything is a subtype of `object`. (_, Type::NominalInstance(instance)) if instance.class().is_object(db) => true, - // A fully static typevar is always a subtype of itself, and is never a subtype of any - // other typevar, since there is no guarantee that they will be specialized to the same - // type. (This is true even if both typevars are bounded by the same final class, since - // you can specialize the typevars to `Never` in addition to that final class.) - (Type::TypeVar(self_typevar), Type::TypeVar(other_typevar)) => { - self_typevar == other_typevar + // 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(_), Type::Union(union)) if union.elements(db).contains(&self) => true, + (Type::Intersection(intersection), Type::TypeVar(_)) + if intersection.positive(db).contains(&target) => + { + true + } + (Type::Intersection(intersection), Type::TypeVar(_)) + if intersection.negative(db).contains(&target) => + { + false } // A fully static typevar is a subtype of its upper bound, and to something similar to @@ -1021,16 +1033,6 @@ impl<'db> Type<'db> { } } - (Type::Union(union), _) => union - .elements(db) - .iter() - .all(|&elem_ty| elem_ty.is_subtype_of(db, target)), - - (_, Type::Union(union)) => union - .elements(db) - .iter() - .any(|&elem_ty| self.is_subtype_of(db, elem_ty)), - // 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. @@ -1044,6 +1046,16 @@ impl<'db> Type<'db> { true } + (Type::Union(union), _) => union + .elements(db) + .iter() + .all(|&elem_ty| elem_ty.is_subtype_of(db, target)), + + (_, Type::Union(union)) => union + .elements(db) + .iter() + .any(|&elem_ty| self.is_subtype_of(db, elem_ty)), + // If both sides are intersections we need to handle the right side first // (A & B & C) is a subtype of (A & B) because the left is a subtype of both A and B, // but none of A, B, or C is a subtype of (A & B). @@ -1309,12 +1321,24 @@ impl<'db> Type<'db> { // TODO this special case might be removable once the below cases are comprehensive (_, Type::NominalInstance(instance)) if instance.class().is_object(db) => true, - // A typevar is always assignable to itself, and is never assignable to any other - // typevar, since there is no guarantee that they will be specialized to the same - // type. (This is true even if both typevars are bounded by the same final class, since - // you can specialize the typevars to `Never` in addition to that final class.) - (Type::TypeVar(self_typevar), Type::TypeVar(other_typevar)) => { - self_typevar == other_typevar + // In general, a TypeVar `T` is not assignable to a type `S` unless one of the two conditions is satisfied: + // 1. `T` is a bound TypeVar and `T`'s upper bound is assignable to `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 assignable to `S`. + // + // However, there is one exception to this general rule: for any given typevar `T`, + // `T` will always be assignable to any union containing `T`. + // A similar rule applies in reverse to intersection types. + (Type::TypeVar(_), Type::Union(union)) if union.elements(db).contains(&self) => true, + (Type::Intersection(intersection), Type::TypeVar(_)) + if intersection.positive(db).contains(&target) => + { + true + } + (Type::Intersection(intersection), Type::TypeVar(_)) + if intersection.negative(db).contains(&target) => + { + false } // A typevar is assignable to its upper bound, and to something similar to the union of @@ -1333,18 +1357,6 @@ impl<'db> Type<'db> { } } - // A union is assignable to a type T iff every element of the union is assignable to T. - (Type::Union(union), ty) => union - .elements(db) - .iter() - .all(|&elem_ty| elem_ty.is_assignable_to(db, ty)), - - // A type T is assignable to a union iff T is assignable to any element of the union. - (ty, Type::Union(union)) => union - .elements(db) - .iter() - .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)), - // 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 assignable to all of the constraints. @@ -1358,6 +1370,18 @@ impl<'db> Type<'db> { true } + // A union is assignable to a type T iff every element of the union is assignable to T. + (Type::Union(union), ty) => union + .elements(db) + .iter() + .all(|&elem_ty| elem_ty.is_assignable_to(db, ty)), + + // A type T is assignable to a union iff T is assignable to any element of the union. + (ty, Type::Union(union)) => union + .elements(db) + .iter() + .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)), + // If both sides are intersections we need to handle the right side first // (A & B & C) is assignable to (A & B) because the left is assignable to both A and B, // but none of A, B, or C is assignable to (A & B). @@ -1572,8 +1596,6 @@ impl<'db> Type<'db> { } } - (Type::TypeVar(first), Type::TypeVar(second)) => first == second, - (Type::NominalInstance(first), Type::NominalInstance(second)) => { first.is_gradual_equivalent_to(db, second) }