[red knot] Fix narrowing for '… is not …' type guards, add '… is …' type guards #13758

sharkdp · 2024-10-15T08:42:47Z

Summary

Fix a bug with … is not … type guards.

Previously, in an example like
```
x = [1]
y = [1]

if x is not y:
    reveal_type(x)
```
we would infer a type of list[int] & ~list[int] == Never for x inside the conditional (instead of list[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 as None.
Add support for … is … type guards.

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

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md

crates/red_knot_python_semantic/resources/mdtest/narrow/match.md

crates/red_knot_python_semantic/src/types.rs

github-actions · 2024-10-15T08:56:58Z

`ruff-ecosystem` results

Linter (stable)

✅ ecosystem check detected no linter changes.

Linter (preview)

✅ ecosystem check detected no linter changes.

MichaReiser

LGTM, but let's wait for at least one review from @AlexWaygood or @carljm to verify that it has the correct semantics

crates/red_knot_python_semantic/src/types.rs

AlexWaygood

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

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is.md

AlexWaygood

A couple more nits, but this LGTM now overall. Thanks!

crates/red_knot_python_semantic/src/types.rs

crates/red_knot_python_semantic/src/types/narrow.rs

crates/red_knot_python_semantic/src/types.rs

carljm · 2024-10-15T20:40:43Z

crates/red_knot_python_semantic/src/types.rs

+                // 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()


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.

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.

carljm · 2024-10-15T20:43:08Z

crates/red_knot_python_semantic/src/types.rs

+                // all singleton types, but it is not straightforward to compute this. Again,
+                // we simply return false.
+                //
+                //   bool & ~Literal[False]`


We should (but don't yet) simplify this to just Literal[True] in intersection builder.

carljm · 2024-10-15T20:44:48Z

crates/red_knot_python_semantic/src/types.rs

+                // we simply return false.
+                //
+                //   bool & ~Literal[False]`
+                //   None & (None | int)


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.

carljm · 2024-10-15T20:47:21Z

crates/red_knot_python_semantic/src/types.rs

+                //
+                //   bool & ~Literal[False]`
+                //   None & (None | int)
+                //   (A | B) & (B | C)          with A, B, C disjunct and B a singleton


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 :)

[red knot] Fix narrowing for 'is not' conditionals

09eeee9

sharkdp requested review from carljm, MichaReiser and AlexWaygood as code owners October 15, 2024 08:42

sharkdp added the red-knot Multi-file analysis & type inference label Oct 15, 2024

sharkdp commented Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/resources/mdtest/narrow/conditionals_is_not.md Show resolved Hide resolved

sharkdp commented Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/resources/mdtest/narrow/match.md Show resolved Hide resolved

sharkdp commented Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

sharkdp commented Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

sharkdp commented Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Show resolved Hide resolved

Move Type::Todo to the false-branch

e241c42

MichaReiser approved these changes Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

crates/red_knot_python_semantic/src/types.rs Show resolved Hide resolved

The empty tuple type is a singleton type

749f176

AlexWaygood requested changes Oct 15, 2024

View reviewed changes

sharkdp added 4 commits October 15, 2024 13:18

Fix behavior for tuple types

e069381

Use custom type instead of LiteralInt

a95b4d5

Add explanation to 'is not' test

b425e6a

Add TODO comment

da842bb

AlexWaygood approved these changes Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

crates/red_knot_python_semantic/src/types/narrow.rs Show resolved Hide resolved

sharkdp added 3 commits October 15, 2024 14:09

Shorten comment regarding union types

edfaf89

Add TODO comment

b219c6f

Handle non-singleton 'is not' case

79f809c

AlexWaygood reviewed Oct 15, 2024

View reviewed changes

crates/red_knot_python_semantic/src/types.rs Outdated Show resolved Hide resolved

Modules are singleton types as well

9169e35

AlexWaygood approved these changes Oct 15, 2024

View reviewed changes

sharkdp merged commit 74bf4b0 into main Oct 15, 2024
20 checks passed

sharkdp deleted the david/type-narrowing-updates branch October 15, 2024 12:49

This was referenced Oct 15, 2024

[red-knot] Port type inference tests to new test framework #13719

Merged

[red-knot] Support for not equal narrowing #13749

Merged

carljm reviewed Oct 15, 2024

View reviewed changes

sharkdp mentioned this pull request Oct 17, 2024

[red-knot] Test setup utilities #13789

Closed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[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

sharkdp commented Oct 15, 2024 •

edited

Loading

github-actions bot commented Oct 15, 2024 •

edited

Loading

MichaReiser left a comment

AlexWaygood left a comment

AlexWaygood left a comment

carljm Oct 15, 2024 •

edited

Loading

AlexWaygood Oct 15, 2024

carljm Oct 15, 2024

carljm Oct 15, 2024

carljm Oct 15, 2024 •

edited

Loading

[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

sharkdp commented Oct 15, 2024 • edited Loading

Summary

Test Plan

github-actions bot commented Oct 15, 2024 • edited Loading

ruff-ecosystem results

Linter (stable)

Linter (preview)

MichaReiser left a comment

Choose a reason for hiding this comment

AlexWaygood left a comment

Choose a reason for hiding this comment

AlexWaygood left a comment

Choose a reason for hiding this comment

carljm Oct 15, 2024 • edited Loading

Choose a reason for hiding this comment

AlexWaygood Oct 15, 2024

Choose a reason for hiding this comment

carljm Oct 15, 2024

Choose a reason for hiding this comment

carljm Oct 15, 2024

Choose a reason for hiding this comment

carljm Oct 15, 2024 • edited Loading

Choose a reason for hiding this comment

sharkdp commented Oct 15, 2024 •

edited

Loading

github-actions bot commented Oct 15, 2024 •

edited

Loading

`ruff-ecosystem` results

carljm Oct 15, 2024 •

edited

Loading

carljm Oct 15, 2024 •

edited

Loading