[red-knot] Handle gradual intersection types in assignability #16611
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
jgeralnik
requested review from
AlexWaygood,
MichaReiser,
carljm and
sharkdp
as code owners
Contributor
|
carljm
reviewed
Mar 11, 2025
Contributor
carljm
left a comment
carljm
left a comment
There was a problem hiding this comment.
Nice work, and thank you for the contribution!
This mostly looks right, I think there's just one area that needs tweaking.
Comment on lines
288
to
292
| # TODO: The following assertion should not fail (see https://github.com/astral-sh/ruff/issues/14899) | ||
| # error: [static-assert-error] | ||
| static_assert(is_assignable_to(Intersection[Unrelated, Any], Not[tuple[Unrelated, Any]])) | ||
| # error: [static-assert-error] | ||
| static_assert(is_assignable_to(Unrelated, Not[tuple[Unrelated]])) |
Contributor
There was a problem hiding this comment.
Nice work on figuring out the real root cause here!
I think, however, that as written these errors are correct. We cannot say that Unrelated is disjoint from tuple (even though it doesn't itself inherit tuple) because there may be a subclass of Unrelated that also multiply-inherits tuple. We could only say this if we also know that Unrelated is final.
This is already implemented correctly by is_disjoint_from, and also tested in its tests. Since these examples aren't demonstrating a behavior that is specific to is_assignable_to, I think we should just remove these examples from this test.
Suggested change
| # TODO: The following assertion should not fail (see https://github.com/astral-sh/ruff/issues/14899) | |
| # error: [static-assert-error] | |
| static_assert(is_assignable_to(Intersection[Unrelated, Any], Not[tuple[Unrelated, Any]])) | |
| # error: [static-assert-error] | |
| static_assert(is_assignable_to(Unrelated, Not[tuple[Unrelated]])) |
| 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)) |
Contributor
There was a problem hiding this comment.
This assertion is pre-existing, and wasn't labeled with a TODO, but it is wrong (which I'm sure made things confusing in terms of the desired behavior). Any can materialize to any type, which means that Any & Parent could be Never & Parent (that is, Never), or it could be Unrelated & Parent. Both of those are assignable to Unrelated. So Any & Parent should be assignable to Unrelated.
Contributor
Author
There was a problem hiding this comment.
I'm not 100% sure I agree. Take the following code:
def f(x: str): ...
def g(x: Any):
if isinstance(x, str):
f(x)
def h(x: Any):
if isinstance(x, int):
f(x)
The goal of this PR is to solve the call in g, which is done because we allow assigning str & Any to str.
Should the call in h also succeed or should we raise an error?
I can see the argument you're making - just because x is an int doesn't mean it's not a str, so in theory a caller could pass an str & int into h, and since h is untyped we can't assume what arguments it gets.
On the other hand, the more helpful thing to the enduser is probably to effectively assume that x is an int here and not allow the assignment, since it's almost certainly incorrect.
For what it's worth mypy seems to agree with me, and raises an error here:
error: Argument 1 to "f" has incompatible type "int"; expected "str" [arg-type]
Contributor
There was a problem hiding this comment.
Technically, the call in h should fail, once we add the ability (which we don't yet have) to recognize that certain C extension or builtin types (or Python types with __slots__) can't be multiply-inherited together at runtime due to incompatible memory layout.
But with two arbitrary types A and B (which are neither final nor use __slots__) in place of int and str, the call in h should succeed. That's simply the nature of Any; there's no consistent theoretical basis for any other behavior. Not implementing this assignability breaks the gradual guarantee (which is a foundational -- perhaps the foundational -- principle of gradual typing): that replacing a static type annotation with Any should not cause new type errors to appear. It's easy to see that in the following code the gradual guarantee would be broken:
class A: pass
class B: pass
def f(x: B):
pass
def h(x: B):
if isinstance(x, A):
f(x)This code should type-check as-is, because A & B is assignable to B. If we don't consistently implement Any in intersections, replacing the annotation x: B with x: Any would cause a new type error to appear. This violates the gradual guarantee.
Mypy does not really implement intersection types, its narrowing behavior is more ad-hoc, and it has decided to incorrectly eliminate Any in intersections, but we are not going to follow that behavior.
Contributor
Author
There was a problem hiding this comment.
Alright, makes sense as a design philosophy. The alternative philosophy is "provide as much value as reasonably possible to a codebase without typing" but I can understand why it makes sense to optimize on soundness.
Will update the PR
| 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(not is_assignable_to(Intersection[Any, Parent], Unrelated)) |
Contributor
There was a problem hiding this comment.
This is a duplicate of the line commented above, and is also wrong; this should be assignable.
| # 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)) | ||
| # Intersection with `Any` is effectively ignored for the sake of assignment |
Contributor
There was a problem hiding this comment.
This comment isn't right. Intersection with Any is not ignored, rather it dominates, in the sense that Any & T is assignable to any type, regardless of T. (Any & T is even assignable to a type S that is disjoint from T, because Any could represent S, and S & T is Never, which is assignable to S.)
Suggested change
| # Intersection with `Any` is effectively ignored for the sake of assignment |
| static_assert(is_assignable_to(Parent, Parent | Intersection[Any, Unrelated])) | ||
|
|
||
| static_assert(not is_assignable_to(Intersection[Child1, Child2], Intersection[Parent, Unrelated])) | ||
| static_assert(not is_assignable_to(Intersection[Parent, Any], Intersection[Parent, Unrelated])) |
Contributor
There was a problem hiding this comment.
Similar to the above cases, this should be assignable.
Comment on lines
820
to
826
| // Any non-dynamic element of S is assignable to T (e.g. `int & Any` is assignable to `int` (but not to `str`)) | ||
| // 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| { | ||
| !matches!(elem_ty, Type::Dynamic(_)) && elem_ty.is_assignable_to(db, ty) | ||
| }) | ||
| } |
Contributor
There was a problem hiding this comment.
As discussed above, the special handling of dynamic types here is not correct. I think the right behavior falls out from just simplifying this code to eliminate that special case.
Suggested change
| // Any non-dynamic element of S is assignable to T (e.g. `int & Any` is assignable to `int` (but not to `str`)) | |
| // 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| { | |
| !matches!(elem_ty, Type::Dynamic(_)) && elem_ty.is_assignable_to(db, ty) | |
| }) | |
| } | |
| // Any element of S is assignable to T (e.g. `int & Any` is assignable to `int` (but not to `str`)) | |
| // 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) | |
| }) | |
| } |
CodSpeed Performance ReportMerging #16611 will improve performances by 14.88%Comparing Summary
Benchmarks breakdown
|
Contributor
Author
|
Fixed the code, which also fixed a diagnostic we were raising in ruff_benchmark. This fixed diagnostic completely convinced me that you are right about the desired behavior, by the way - the code was effectively: which my original version incorrectly typed as effectively equivalent to ~AlwaysFalsy and failed on because ~AlwaysFalsy is not assignable to str. |
Contributor
|
carljm
approved these changes
Mar 11, 2025
Contributor
carljm
left a comment
carljm
left a comment
There was a problem hiding this comment.
Awesome, thank you so much for the PR!
dcreager
added a commit
that referenced
this pull request
Mar 11, 2025
* main: [red-knot] Rework `Type::to_instance()` to return `Option<Type>` (#16428) [red-knot] Add tests asserting that `KnownClass::to_instance()` doesn't unexpectedly fallback to `Type::Unknown` with full typeshed stubs (#16608) [red-knot] Handle gradual intersection types in assignability (#16611) [red-knot] mypy_primer: split installation and execution (#16622) [red-knot] mypy_primer: pipeline improvements (#16620) [red-knot] Infer `lambda` expression (#16547) [red-knot] mypy_primer: strip ANSI codes (#16604) [red-knot] mypy_primer: comment on PRs (#16599)
carljm
added a commit
that referenced
this pull request
Mar 12, 2025
## Summary Background - as a follow up to #16611 I noticed that there's a lot of code duplicated between the `is_assignable_to` and `is_subtype_of` functions and considered trying to merge them. [A subtype and an assignable type are pretty much the same](https://typing.python.org/en/latest/spec/concepts.html#the-assignable-to-or-consistent-subtyping-relation), except that subtypes are by definition fully static, so I think we can replace the whole of `is_subtype_of` with: ``` if !self.is_fully_static(db) || !target.is_fully_static(db) { return false; } return self.is_assignable_to(target) ``` if we move all of the logic to is_assignable_to and delete duplicate code. Then we can discuss if it even makes sense to have a separate is_subtype_of function (I think the answer is yes since it's used by a bunch of other places, but we may be able to basically rip out the concept). Anyways while playing with combining the functions I noticed is that the handling of Intersections in `is_subtype_of` has a special case for two intersections, which I didn't include in the last PR - rather I first handled right hand intersections before left hand, which should properly handle double intersections (hand-wavy explanation I can justify if needed - (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)). I took a look at what breaks if I remove the handling for double intersections, and the reason it is needed is because is_disjoint does not properly handle intersections with negative conditions (so instead `is_subtype_of` basically implements the check correctly). This PR adds support to is_disjoint for properly checking negative branches, which also lets us simplify `is_subtype_of`, bringing it in line with `is_assignable_to` ## Test Plan Added a bunch of tests, most of which failed before this fix --------- Co-authored-by: Carl Meyer <carl@astral.sh>
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
3 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
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:
The desired behavior is pretty much to ignore Any/Unknown when resolving intersection assignability -
Any & strshould be assignable tostr, andstrshould be assignable tostr & AnyThe 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:
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:
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.