[red knot] Fix narrowing for '… is not …' type guards, add '… is …' type guards#13758
[red knot] Fix narrowing for '… is not …' type guards, add '… is …' type guards#13758
Conversation
crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md
Show resolved
Hide resolved
|
MichaReiser
left a comment
There was a problem hiding this comment.
LGTM, but let's wait for at least one review from @AlexWaygood or @carljm to verify that it has the correct semantics
AlexWaygood
left a comment
There was a problem hiding this comment.
Thanks! This mostly looks good, but there's an important correctness thing we need to fix involving tuples. I also left a couple of minor nitpick comments as well :-)
As well as the language reference, Brett Cannon's blog series unravelling syntactic sugar is also an invaluable resource for understanding what these operators are doing under the hood. His article unravelling is and is not is one of the shorter ones, but it's here: https://snarky.ca/unravelling-is-and-is-not/
crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md
Outdated
Show resolved
Hide resolved
crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md
Outdated
Show resolved
Hide resolved
crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md
Show resolved
Hide resolved
AlexWaygood
left a comment
There was a problem hiding this comment.
A couple more nits, but this LGTM now overall. Thanks!
| // We deliberately deviate from the language specification [1] here and claim | ||
| // that the empty tuple type is a singleton type. The reasoning is that `()` | ||
| // is often used as a sentinel value in user code. Declaring the empty tuple to | ||
| // be of singleton type allows us to narrow types in `is not ()` conditionals. | ||
| // | ||
| // [1] https://docs.python.org/3/reference/expressions.html#parenthesized-forms | ||
| tuple.elements(db).is_empty() |
There was a problem hiding this comment.
I'm not sure we'll want to stick with this conclusion, given the response to https://discuss.python.org/t/should-we-specify-in-the-language-reference-that-the-empty-tuple-is-a-singleton/67957/7 -- in particular the fact that is comparisons with tuples are now a syntax warning in recent Python versions, and that there are Python implementations (GraalPy) for which the empty tuple is not a singleton. But we can leave it for now, I don't think it's particularly critical either way.
There was a problem hiding this comment.
yeah. Though strictly speaking the narrowing is still safe on all popular Python implementations, and probably always will be. But probably not worth carving out a special case for, given the language appears to be actively discouraging it now.
| // all singleton types, but it is not straightforward to compute this. Again, | ||
| // we simply return false. | ||
| // | ||
| // bool & ~Literal[False]` |
There was a problem hiding this comment.
We should (but don't yet) simplify this to just Literal[True] in intersection builder.
| // we simply return false. | ||
| // | ||
| // bool & ~Literal[False]` | ||
| // None & (None | int) |
There was a problem hiding this comment.
This type also cannot occur in our representation, because we normalize to disjunctive normal form (union of intersections), so this would become (None & None) | (None & int) and then None | (None & int) and then (this step not yet implemented) None | Never and thus just None.
| // | ||
| // bool & ~Literal[False]` | ||
| // None & (None | int) | ||
| // (A | B) & (B | C) with A, B, C disjunct and B a singleton |
There was a problem hiding this comment.
We already always normalize this to (A & B) | (A & C) | (B & B) | (B & C) -> (A & B) | (A & C) | B | (B & C), which should (though I'm not sure if it would yet?) become (A & C) | B, which (if we know A and C are disjoint -- this part not yet implemented) should become just B -- so then would return true from this method :)
Summary
Fix a bug with
… is not …type guards.Previously, in an example like
we would infer a type of
list[int] & ~list[int] == Neverforxinside the conditional (instead oflist[int]), since we built a (negative) intersection with the type of the right hand side (y). However, as this example shows, this assumption can only be made for singleton types (types with a single inhabitant) such asNone.Add support for
… is …type guards.closes #13715
Test Plan
Moved existing
narrow_…tests to Markdown-based tests and added new ones (including a regression test for the bug described above). Note that will create some conflicts with #13719. I tried to establish the correct organizational structure as proposed in this comment