[red knot] add Type::is_disjoint_from and intersection simplifications (#13775)

## Summary

- Add `Type::is_disjoint_from` as a way to test whether two types
overlap
- Add a first set of simplification rules for intersection types
  - `S & T = S` for `S <: T`
  - `S & ~T = Never` for `S <: T`
  - `~S & ~T = ~T` for `S <: T`
  - `A & ~B = A` for `A` disjoint from `B`
  - `A & B = Never` for `A` disjoint from `B`
  - `bool & ~Literal[bool] = Literal[!bool]`

resolves one item in #12694

## Open questions:

- Can we somehow leverage the (anti) symmetry between `positive` and
`negative` contributions? I could imagine that there would be a way if
we had `Type::Not(type)`/`Type::Negative(type)`, but with the
`positive`/`negative` architecture, I'm not sure. Note that there is a
certain duplication in the `add_positive`/`add_negative` functions (e.g.
`S & ~T = Never` is implemented twice), but other rules are actually not
perfectly symmetric: `S & T = S` vs `~S & ~T = ~T`.
- I'm not particularly proud of the way `add_positive`/`add_negative`
turned out. They are long imperative-style functions with some
mutability mixed in (`to_remove`). I'm happy to look into ways to
improve this code *if we decide to go with this approach* of
implementing a set of ad-hoc rules for simplification.
- ~~Is it useful to perform simplifications eagerly in
`add_positive`/`add_negative`? (@carljm)~~ This is what I did for now.

## Test Plan

- Unit tests for `Type::is_disjoint_from`
- Observe changes in Markdown-based tests
- Unit tests for `IntersectionBuilder::build()`

---------

Co-authored-by: Carl Meyer <carl@astral.sh>
This commit is contained in:
David Peter 2024-10-18 23:34:43 +02:00 committed by GitHub
parent c93a7c7878
commit 6964eef369
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
5 changed files with 626 additions and 63 deletions

View file

@ -6,8 +6,7 @@
x = None if flag else 1
if x is None:
# TODO the following should be simplified to 'None'
reveal_type(x) # revealed: None | Literal[1] & None
reveal_type(x) # revealed: None
reveal_type(x) # revealed: None | Literal[1]
```
@ -22,8 +21,7 @@ x = A()
y = x if flag else None
if y is x:
# TODO the following should be simplified to 'A'
reveal_type(y) # revealed: A | None & A
reveal_type(y) # revealed: A
reveal_type(y) # revealed: A | None
```

View file

@ -20,8 +20,7 @@ x = True if flag else False
reveal_type(x) # revealed: bool
if x is not False:
# TODO the following should be `Literal[True]`
reveal_type(x) # revealed: bool & ~Literal[False]
reveal_type(x) # revealed: Literal[True]
```
## `is not` for non-singleton types

View file

@ -12,6 +12,5 @@ match x:
case None:
y = x
# TODO intersection simplification: should be just Literal[0] | None
reveal_type(y) # revealed: Literal[0] | None | Literal[1] & None
reveal_type(y) # revealed: Literal[0] | None
```