[red-knot] Handle gradual intersection types in assignability (#16611)

## Summary This mostly fixes #14899 My motivation was similar to the last comment by @sharkdp there. I ran red_knot on a codebase and the most common error was patterns like this failing: ``` def foo(x: str): ... x: Any = ... if isinstance(x, str): foo(x) # Object of type `Any & str` cannot be assigned to parameter 1 (`x`) of function `foo`; expected type `str` ``` The desired behavior is pretty much to ignore Any/Unknown when resolving intersection assignability - `Any & str` should be assignable to `str`, and `str` should be assignable to `str & Any` The fix is actually very similar to the existing code in `is_subtype_of`, we need to correctly handle intersections on either side, while being careful to handle dynamic types as desired. This does not fix the second test case from that issue: ``` static_assert(is_assignable_to(Intersection[Unrelated, Any], Not[tuple[Unrelated, Any]])) ``` but that's misleading because the root cause there has nothing to do with gradual types. I added a simpler test case that also fails: ``` static_assert(is_assignable_to(Unrelated, Not[tuple[Unrelated]])) ``` This is because we don't determine that Unrelated does not subclass from tuple so we can't rule out this relation. If that logic is improved then this fix should also handle the case of the intersection ## Test Plan Added a bunch of is_assignable_to tests, most of which failed before this fix.
2025-03-11 16:58:56 +02:00
parent 3b497716f1
commit e8e24310fb
3 changed files with 50 additions and 30 deletions
--- a/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
+++ b/crates/red_knot_python_semantic/resources/mdtest/type_properties/is_assignable_to.md
@@ -248,6 +248,7 @@ static_assert(is_assignable_to(Intersection[Child1, Parent], Parent))

 static_assert(is_assignable_to(Intersection[Parent, Unrelated], Parent))
 static_assert(is_assignable_to(Intersection[Child1, Unrelated], Child1))
+static_assert(is_assignable_to(Intersection[Child1, Unrelated, Child2], Intersection[Child1, Unrelated]))

 static_assert(is_assignable_to(Intersection[Child1, Not[Child2]], Child1))
 static_assert(is_assignable_to(Intersection[Child1, Not[Child2]], Parent))
@@ -256,21 +257,40 @@ static_assert(is_assignable_to(Intersection[Child1, Not[Grandchild]], Parent))
 static_assert(is_assignable_to(Intersection[Child1, Child2], Intersection[Child1, Child2]))
 static_assert(is_assignable_to(Intersection[Child1, Child2], Intersection[Child2, Child1]))
 static_assert(is_assignable_to(Grandchild, Intersection[Child1, Child2]))
+static_assert(not is_assignable_to(Intersection[Child1, Child2], Intersection[Parent, Unrelated]))

 static_assert(not is_assignable_to(Parent, Intersection[Parent, Unrelated]))
 static_assert(not is_assignable_to(int, Intersection[int, Not[Literal[1]]]))
+# The literal `1` is not assignable to `Parent`, so the intersection of int and Parent is definitely an int that is not `1`
+static_assert(is_assignable_to(Intersection[int, Parent], Intersection[int, Not[Literal[1]]]))
 static_assert(not is_assignable_to(int, Not[int]))
 static_assert(not is_assignable_to(int, Not[Literal[1]]))

-static_assert(not is_assignable_to(Intersection[Any, Parent], Unrelated))
-static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Any]))
-static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]]))
+# Intersection with `Any` dominates the left hand side of intersections
+static_assert(is_assignable_to(Intersection[Any, Parent], Parent))
+static_assert(is_assignable_to(Intersection[Any, Child1], Parent))
+static_assert(is_assignable_to(Intersection[Any, Child2, Not[Child1]], Parent))
+static_assert(is_assignable_to(Intersection[Any, Parent], Unrelated))
+static_assert(is_assignable_to(Intersection[Any, Parent], Intersection[Parent, Unrelated]))
+static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Parent))
+static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersection[Parent, Unrelated]))

-# TODO: The following assertions should not fail (see https://github.com/astral-sh/ruff/issues/14899)
-# error: [static-assert-error]
-static_assert(is_assignable_to(Intersection[Any, int], int))
-# error: [static-assert-error]
-static_assert(is_assignable_to(Intersection[Unrelated, Any], Not[tuple[Unrelated, Any]]))
+# Even Any & Not[Parent] is assignable to Parent, since it could be Never
+static_assert(is_assignable_to(Intersection[Any, Not[Parent]], Parent))
+
+# Intersection with `Any` is effectively ignored on the right hand side for the sake of assignment
+static_assert(is_assignable_to(Parent, Intersection[Any, Parent]))
+static_assert(is_assignable_to(Parent, Parent | Intersection[Any, Unrelated]))
+static_assert(is_assignable_to(Child1, Intersection[Any, Parent]))
+static_assert(not is_assignable_to(Literal[1], Intersection[Any, Parent]))
+static_assert(not is_assignable_to(Unrelated, Intersection[Any, Parent]))
+
+# Intersections with Any on both sides combine the above logic - the LHS dominates and Any is ignored on the right hand side
+static_assert(is_assignable_to(Intersection[Any, Parent], Intersection[Any, Parent]))
+static_assert(is_assignable_to(Intersection[Any, Unrelated], Intersection[Any, Parent]))
+static_assert(is_assignable_to(Intersection[Any, Parent, Unrelated], Intersection[Any, Parent, Unrelated]))
+static_assert(is_assignable_to(Intersection[Unrelated, Any], Intersection[Unrelated, Not[Any]]))
+static_assert(is_assignable_to(Intersection[Literal[1], Any], Intersection[Unrelated, Not[Any]]))
 ```

 ## General properties
--- a/crates/red_knot_python_semantic/src/types.rs
+++ b/crates/red_knot_python_semantic/src/types.rs
@@ -802,6 +802,28 @@ impl<'db> Type<'db> {
                .iter()
                .any(|&elem_ty| ty.is_assignable_to(db, elem_ty)),

+            // A type S is assignable to an intersection type T if
+            // S is assignable to all positive elements of T (e.g. `str & int` is assignable to `str & Any`), and
+            // S is disjoint from all negative elements of T (e.g. `int` is not assignable to Intersection[int, Not[Literal[1]]]).
+            (ty, Type::Intersection(intersection)) => {
+                intersection
+                    .positive(db)
+                    .iter()
+                    .all(|&elem_ty| ty.is_assignable_to(db, elem_ty))
+                    && intersection
+                        .negative(db)
+                        .iter()
+                        .all(|&neg_ty| ty.is_disjoint_from(db, neg_ty))
+            }
+
+            // An intersection type S is assignable to a type T if
+            // Any element of S is assignable to T (e.g. `A & B` is assignable to `A`)
+            // Negative elements do not have an effect on assignability - if S is assignable to T then S & ~P is also assignable to T.
+            (Type::Intersection(intersection), ty) => intersection
+                .positive(db)
+                .iter()
+                .any(|&elem_ty| elem_ty.is_assignable_to(db, ty)),
+
            // A tuple type S is assignable to a tuple type T if their lengths are the same, and
            // each element of S is assignable to the corresponding element of T.
            (Type::Tuple(self_tuple), Type::Tuple(target_tuple)) => {