From f2c3ddc5eaa2ce107a200e134be82fc36afce06b Mon Sep 17 00:00:00 2001 From: David Peter Date: Fri, 10 Jan 2025 14:04:03 +0100 Subject: [PATCH] [red-knot] Move intersection type tests to Markdown (#15396) ## Summary [**Rendered version of the new test suite**](https://github.com/astral-sh/ruff/blob/david/intersection-type-tests/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md) Moves most of our existing intersection-types tests to a dedicated Markdown test suite, extends the test coverage, unifies the notation for these tests, groups tests into a proper structure, and adds some explanations for various simplification strategies. This changeset also: - Adds a new simplification where `~Never` is removed from intersections. - Adds a new simplification where adding `~object` simplifies the whole intersection to `Never` - Avoids unnecessary assignment-checks between inferred and declared type. This was added to this changeset to avoid many false positive errors in this test suite. Resolves the task described in this old comment [here](https://github.com/astral-sh/ruff/pull/13962/files/e01da82a5a0ef6a2af0aa4dc50f898cffadb4a33..e7e432bca2b3f24979da55a9a34ad765aaaae8d1#r1819924085). ## Test Plan Running the new Markdown tests --------- Co-authored-by: Alex Waygood --- .../resources/mdtest/intersection_types.md | 747 ++++++++++++++++++ .../resources/mdtest/union_types.md | 18 + .../src/types/builder.rs | 599 +------------- .../src/types/infer.rs | 144 +++- 4 files changed, 888 insertions(+), 620 deletions(-) create mode 100644 crates/red_knot_python_semantic/resources/mdtest/intersection_types.md diff --git a/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md new file mode 100644 index 0000000000000..64c97adb5b45d --- /dev/null +++ b/crates/red_knot_python_semantic/resources/mdtest/intersection_types.md @@ -0,0 +1,747 @@ +# Intersection types + +## Introduction + +This test suite covers certain properties of intersection types and makes sure that we can apply +various simplification strategies. We use `Intersection` (`&`) and `Not` (`~`) to construct +intersection types (note that we display negative contributions at the end; the order does not +matter): + +```py +from knot_extensions import Intersection, Not + +class P: ... +class Q: ... + +def _( + i1: Intersection[P, Q], + i2: Intersection[P, Not[Q]], + i3: Intersection[Not[P], Q], + i4: Intersection[Not[P], Not[Q]], +) -> None: + reveal_type(i1) # revealed: P & Q + reveal_type(i2) # revealed: P & ~Q + reveal_type(i3) # revealed: Q & ~P + reveal_type(i4) # revealed: ~P & ~Q +``` + +## Notation + +Throughout this document, we use the following types as representatives for certain equivalence +classes. + +### Non-disjoint types + +We use `P`, `Q`, `R`, … to denote types that are non-disjoint: + +```py +from knot_extensions import static_assert, is_disjoint_from + +class P: ... +class Q: ... +class R: ... + +static_assert(not is_disjoint_from(P, Q)) +static_assert(not is_disjoint_from(P, R)) +static_assert(not is_disjoint_from(Q, R)) +``` + +Although `P` is not a subtype of `Q` and `Q` is not a subtype of `P`, the two types are not disjoint +because it would be possible to create a class `S` that inherits from both `P` and `Q` using +multiple inheritance. An instance of `S` would be a member of the `P` type _and_ the `Q` type. + +### Disjoint types + +We use `Literal[1]`, `Literal[2]`, … as examples of pairwise-disjoint types, and `int` as a joint +supertype of these: + +```py +from knot_extensions import static_assert, is_disjoint_from, is_subtype_of +from typing import Literal + +static_assert(is_disjoint_from(Literal[1], Literal[2])) +static_assert(is_disjoint_from(Literal[1], Literal[3])) +static_assert(is_disjoint_from(Literal[2], Literal[3])) + +static_assert(is_subtype_of(Literal[1], int)) +static_assert(is_subtype_of(Literal[2], int)) +static_assert(is_subtype_of(Literal[3], int)) +``` + +### Subtypes + +Finally, we use `A <: B <: C` and `A <: B1`, `A <: B2` to denote hierarchies of (proper) subtypes: + +```py +from knot_extensions import static_assert, is_subtype_of, is_disjoint_from + +class A: ... +class B(A): ... +class C(B): ... + +static_assert(is_subtype_of(B, A)) +static_assert(is_subtype_of(C, B)) +static_assert(is_subtype_of(C, A)) + +static_assert(not is_subtype_of(A, B)) +static_assert(not is_subtype_of(B, C)) +static_assert(not is_subtype_of(A, C)) + +class B1(A): ... +class B2(A): ... + +static_assert(is_subtype_of(B1, A)) +static_assert(is_subtype_of(B2, A)) + +static_assert(not is_subtype_of(A, B1)) +static_assert(not is_subtype_of(A, B2)) + +static_assert(not is_subtype_of(B1, B2)) +static_assert(not is_subtype_of(B2, B1)) +``` + +## Structural properties + +This section covers structural properties of intersection types and documents some decisions on how +to represent mixtures of intersections and unions. + +### Single-element unions + +If we have a union of a single element, we can simplify to that element. Similarly, we show an +intersection with a single negative contribution as just the negation of that element. + +```py +from knot_extensions import Intersection, Not + +class P: ... + +def _( + i1: Intersection[P], + i2: Intersection[Not[P]], +) -> None: + reveal_type(i1) # revealed: P + reveal_type(i2) # revealed: ~P +``` + +### Flattening of nested intersections + +We eagerly flatten nested intersections types. + +```py +from knot_extensions import Intersection, Not + +class P: ... +class Q: ... +class R: ... +class S: ... + +def positive_contributions( + i1: Intersection[P, Intersection[Q, R]], + i2: Intersection[Intersection[P, Q], R], +) -> None: + reveal_type(i1) # revealed: P & Q & R + reveal_type(i2) # revealed: P & Q & R + +def negative_contributions( + i1: Intersection[Not[P], Intersection[Not[Q], Not[R]]], + i2: Intersection[Intersection[Not[P], Not[Q]], Not[R]], +) -> None: + reveal_type(i1) # revealed: ~P & ~Q & ~R + reveal_type(i2) # revealed: ~P & ~Q & ~R + +def mixed( + i1: Intersection[P, Intersection[Not[Q], R]], + i2: Intersection[Intersection[P, Not[Q]], R], + i3: Intersection[Not[P], Intersection[Q, Not[R]]], + i4: Intersection[Intersection[Q, Not[R]], Not[P]], +) -> None: + reveal_type(i1) # revealed: P & R & ~Q + reveal_type(i2) # revealed: P & R & ~Q + reveal_type(i3) # revealed: Q & ~P & ~R + reveal_type(i4) # revealed: Q & ~R & ~P + +def multiple( + i1: Intersection[Intersection[P, Q], Intersection[R, S]], +): + reveal_type(i1) # revealed: P & Q & R & S + +def nested( + i1: Intersection[Intersection[Intersection[P, Q], R], S], + i2: Intersection[P, Intersection[Q, Intersection[R, S]]], +): + reveal_type(i1) # revealed: P & Q & R & S + reveal_type(i2) # revealed: P & Q & R & S +``` + +### Union of intersections + +We always normalize our representation to a _union of intersections_, so when we add a _union to an +intersection_, we distribute the union over the respective elements: + +```py +from knot_extensions import Intersection, Not + +class P: ... +class Q: ... +class R: ... +class S: ... + +def _( + i1: Intersection[P, Q | R | S], + i2: Intersection[P | Q | R, S], + i3: Intersection[P | Q, R | S], +) -> None: + reveal_type(i1) # revealed: P & Q | P & R | P & S + reveal_type(i2) # revealed: P & S | Q & S | R & S + reveal_type(i3) # revealed: P & R | Q & R | P & S | Q & S + +def simplifications_for_same_elements( + i1: Intersection[P, Q | P], + i2: Intersection[Q, P | Q], + i3: Intersection[P | Q, Q | R], + i4: Intersection[P | Q, P | Q], + i5: Intersection[P | Q, Q | P], +) -> None: + # P & (Q | P) + # = P & Q | P & P + # = P & Q | P + # = P + # (because P is a supertype of P & Q) + reveal_type(i1) # revealed: P + # similar here: + reveal_type(i2) # revealed: Q + + # (P | Q) & (Q | R) + # = P & Q | P & R | Q & Q | Q & R + # = P & Q | P & R | Q | Q & R + # = Q | P & R + # (again, because Q is a supertype of P & Q and of Q & R) + reveal_type(i3) # revealed: Q | P & R + + # (P | Q) & (P | Q) + # = P & P | P & Q | Q & P | Q & Q + # = P | P & Q | Q + # = P | Q + reveal_type(i4) # revealed: P | Q +``` + +### Negation distributes over union + +Distribution also applies to a negation operation. This is a manifestation of one of +[De Morgan's laws], namely `~(P | Q) = ~P & ~Q`: + +```py +from knot_extensions import Not +from typing import Literal + +class P: ... +class Q: ... +class R: ... + +def _(i1: Not[P | Q], i2: Not[P | Q | R]) -> None: + reveal_type(i1) # revealed: ~P & ~Q + reveal_type(i2) # revealed: ~P & ~Q & ~R + +def example_literals(i: Not[Literal[1, 2]]) -> None: + reveal_type(i) # revealed: ~Literal[1] & ~Literal[2] +``` + +### Negation of intersections + +The other of [De Morgan's laws], `~(P & Q) = ~P | ~Q`, also holds: + +```py +from knot_extensions import Intersection, Not + +class P: ... +class Q: ... +class R: ... + +def _( + i1: Not[Intersection[P, Q]], + i2: Not[Intersection[P, Q, R]], +) -> None: + reveal_type(i1) # revealed: ~P | ~Q + reveal_type(i2) # revealed: ~P | ~Q | ~R +``` + +### `Never` is dual to `object` + +`Never` represents the empty set of values, while `object` represents the set of all values, so +`~Never` is equivalent to `object`, and `~object` is equivalent to `Never`. This is a manifestation +of the [complement laws] of set theory. + +```py +from knot_extensions import Intersection, Not +from typing_extensions import Never + +def _( + not_never: Not[Never], + not_object: Not[object], +) -> None: + reveal_type(not_never) # revealed: object + reveal_type(not_object) # revealed: Never +``` + +### Intersection of a type and its negation + +Continuing with more [complement laws], if we see both `P` and `~P` in an intersection, we can +simplify to `Never`, even in the presence of other types: + +```py +from knot_extensions import Intersection, Not +from typing import Any + +class P: ... +class Q: ... + +def _( + i1: Intersection[P, Not[P]], + i2: Intersection[Not[P], P], + i3: Intersection[P, Q, Not[P]], + i4: Intersection[Not[P], Q, P], + i5: Intersection[P, Any, Not[P]], + i6: Intersection[Not[P], Any, P], +) -> None: + reveal_type(i1) # revealed: Never + reveal_type(i2) # revealed: Never + reveal_type(i3) # revealed: Never + reveal_type(i4) # revealed: Never + reveal_type(i5) # revealed: Never + reveal_type(i6) # revealed: Never +``` + +### Union of a type and its negation + +Similarly, if we have both `P` and `~P` in a _union_, we could simplify that to `object`. However, +this is a rather costly operation which would require us to build the negation of each type that we +add to a union, so this is not implemented at the moment. + +```py +from knot_extensions import Intersection, Not + +class P: ... + +def _( + i1: P | Not[P], + i2: Not[P] | P, +) -> None: + # These could be simplified to `object` + reveal_type(i1) # revealed: P | ~P + reveal_type(i2) # revealed: ~P | P +``` + +### Negation is an involution + +The final of the [complement laws] states that negating twice is equivalent to not negating at all: + +```py +from knot_extensions import Not + +class P: ... + +def _( + i1: Not[P], + i2: Not[Not[P]], + i3: Not[Not[Not[P]]], + i4: Not[Not[Not[Not[P]]]], +) -> None: + reveal_type(i1) # revealed: ~P + reveal_type(i2) # revealed: P + reveal_type(i3) # revealed: ~P + reveal_type(i4) # revealed: P +``` + +## Simplification strategies + +In this section, we present various simplification strategies that go beyond the structure of the +representation. + +### `Never` in intersections + +If we intersect with `Never`, we can simplify the whole intersection to `Never`, even if there are +dynamic types involved: + +```py +from knot_extensions import Intersection, Not +from typing_extensions import Never, Any + +class P: ... +class Q: ... + +def _( + i1: Intersection[P, Never], + i2: Intersection[Never, P], + i3: Intersection[Any, Never], + i4: Intersection[Never, Not[Any]], +) -> None: + reveal_type(i1) # revealed: Never + reveal_type(i2) # revealed: Never + reveal_type(i3) # revealed: Never + reveal_type(i4) # revealed: Never +``` + +### Simplifications using disjointness + +#### Positive contributions + +If we intersect disjoint types, we can simplify to `Never`, even in the presence of other types: + +```py +from knot_extensions import Intersection, Not +from typing import Literal, Any + +class P: ... + +def _( + i01: Intersection[Literal[1], Literal[2]], + i02: Intersection[Literal[2], Literal[1]], + i03: Intersection[Literal[1], Literal[2], P], + i04: Intersection[Literal[1], P, Literal[2]], + i05: Intersection[P, Literal[1], Literal[2]], + i06: Intersection[Literal[1], Literal[2], Any], + i07: Intersection[Literal[1], Any, Literal[2]], + i08: Intersection[Any, Literal[1], Literal[2]], +) -> None: + reveal_type(i01) # revealed: Never + reveal_type(i02) # revealed: Never + reveal_type(i03) # revealed: Never + reveal_type(i04) # revealed: Never + reveal_type(i05) # revealed: Never + reveal_type(i06) # revealed: Never + reveal_type(i07) # revealed: Never + reveal_type(i08) # revealed: Never + +# `bool` is final and can not be subclassed, so `type[bool]` is equivalent to `Literal[bool]`, which +# is disjoint from `type[str]`: +def example_type_bool_type_str( + i: Intersection[type[bool], type[str]], +) -> None: + reveal_type(i) # revealed: Never +``` + +#### Positive and negative contributions + +If we intersect a type `X` with the negation of a disjoint type `Y`, we can remove the negative +contribution `~Y`, as it necessarily overlaps with the positive contribution `X`: + +```py +from knot_extensions import Intersection, Not +from typing import Literal + +def _( + i1: Intersection[Literal[1], Not[Literal[2]]], + i2: Intersection[Not[Literal[2]], Literal[1]], + i3: Intersection[Literal[1], Not[Literal[2]], int], + i4: Intersection[Literal[1], int, Not[Literal[2]]], + i5: Intersection[int, Literal[1], Not[Literal[2]]], +) -> None: + reveal_type(i1) # revealed: Literal[1] + reveal_type(i2) # revealed: Literal[1] + reveal_type(i3) # revealed: Literal[1] + reveal_type(i4) # revealed: Literal[1] + reveal_type(i5) # revealed: Literal[1] + +# None is disjoint from int, so this simplification applies here +def example_none( + i1: Intersection[int, Not[None]], + i2: Intersection[Not[None], int], +) -> None: + reveal_type(i1) # revealed: int + reveal_type(i2) # revealed: int +``` + +### Simplifications using subtype relationships + +#### Positive type and positive subtype + +Subtypes are contained within their supertypes, so we can simplify intersections by removing +superfluous supertypes: + +```py +from knot_extensions import Intersection, Not +from typing import Any + +class A: ... +class B(A): ... +class C(B): ... +class Unrelated: ... + +def _( + i01: Intersection[A, B], + i02: Intersection[B, A], + i03: Intersection[A, C], + i04: Intersection[C, A], + i05: Intersection[B, C], + i06: Intersection[C, B], + i07: Intersection[A, B, C], + i08: Intersection[C, B, A], + i09: Intersection[B, C, A], + i10: Intersection[A, B, Unrelated], + i11: Intersection[B, A, Unrelated], + i12: Intersection[B, Unrelated, A], + i13: Intersection[A, Unrelated, B], + i14: Intersection[Unrelated, A, B], + i15: Intersection[Unrelated, B, A], + i16: Intersection[A, B, Any], + i17: Intersection[B, A, Any], + i18: Intersection[B, Any, A], + i19: Intersection[A, Any, B], + i20: Intersection[Any, A, B], + i21: Intersection[Any, B, A], +) -> None: + reveal_type(i01) # revealed: B + reveal_type(i02) # revealed: B + reveal_type(i03) # revealed: C + reveal_type(i04) # revealed: C + reveal_type(i05) # revealed: C + reveal_type(i06) # revealed: C + reveal_type(i07) # revealed: C + reveal_type(i08) # revealed: C + reveal_type(i09) # revealed: C + reveal_type(i10) # revealed: B & Unrelated + reveal_type(i11) # revealed: B & Unrelated + reveal_type(i12) # revealed: B & Unrelated + reveal_type(i13) # revealed: Unrelated & B + reveal_type(i14) # revealed: Unrelated & B + reveal_type(i15) # revealed: Unrelated & B + reveal_type(i16) # revealed: B & Any + reveal_type(i17) # revealed: B & Any + reveal_type(i18) # revealed: B & Any + reveal_type(i19) # revealed: Any & B + reveal_type(i20) # revealed: Any & B + reveal_type(i21) # revealed: Any & B +``` + +#### Negative type and negative subtype + +For negative contributions, this property is reversed. Here we can get remove superfluous +_subtypes_: + +```py +from knot_extensions import Intersection, Not +from typing import Any + +class A: ... +class B(A): ... +class C(B): ... +class Unrelated: ... + +def _( + i01: Intersection[Not[B], Not[A]], + i02: Intersection[Not[A], Not[B]], + i03: Intersection[Not[A], Not[C]], + i04: Intersection[Not[C], Not[A]], + i05: Intersection[Not[B], Not[C]], + i06: Intersection[Not[C], Not[B]], + i07: Intersection[Not[A], Not[B], Not[C]], + i08: Intersection[Not[C], Not[B], Not[A]], + i09: Intersection[Not[B], Not[C], Not[A]], + i10: Intersection[Not[B], Not[A], Unrelated], + i11: Intersection[Not[A], Not[B], Unrelated], + i12: Intersection[Not[A], Unrelated, Not[B]], + i13: Intersection[Not[B], Unrelated, Not[A]], + i14: Intersection[Unrelated, Not[A], Not[B]], + i15: Intersection[Unrelated, Not[B], Not[A]], + i16: Intersection[Not[B], Not[A], Any], + i17: Intersection[Not[A], Not[B], Any], + i18: Intersection[Not[A], Any, Not[B]], + i19: Intersection[Not[B], Any, Not[A]], + i20: Intersection[Any, Not[A], Not[B]], + i21: Intersection[Any, Not[B], Not[A]], +) -> None: + reveal_type(i01) # revealed: ~A + reveal_type(i02) # revealed: ~A + reveal_type(i03) # revealed: ~A + reveal_type(i04) # revealed: ~A + reveal_type(i05) # revealed: ~B + reveal_type(i06) # revealed: ~B + reveal_type(i07) # revealed: ~A + reveal_type(i08) # revealed: ~A + reveal_type(i09) # revealed: ~A + reveal_type(i10) # revealed: Unrelated & ~A + reveal_type(i11) # revealed: Unrelated & ~A + reveal_type(i12) # revealed: Unrelated & ~A + reveal_type(i13) # revealed: Unrelated & ~A + reveal_type(i14) # revealed: Unrelated & ~A + reveal_type(i15) # revealed: Unrelated & ~A + reveal_type(i16) # revealed: Any & ~A + reveal_type(i17) # revealed: Any & ~A + reveal_type(i18) # revealed: Any & ~A + reveal_type(i19) # revealed: Any & ~A + reveal_type(i20) # revealed: Any & ~A + reveal_type(i21) # revealed: Any & ~A +``` + +#### Negative type and multiple negative subtypes + +If there are multiple negative subtypes, all of them can be removed: + +```py +from knot_extensions import Intersection, Not + +class A: ... +class B1(A): ... +class B2(A): ... + +def _( + i1: Intersection[Not[A], Not[B1], Not[B2]], + i2: Intersection[Not[A], Not[B2], Not[B1]], + i3: Intersection[Not[B1], Not[A], Not[B2]], + i4: Intersection[Not[B1], Not[B2], Not[A]], + i5: Intersection[Not[B2], Not[A], Not[B1]], + i6: Intersection[Not[B2], Not[B1], Not[A]], +) -> None: + reveal_type(i1) # revealed: ~A + reveal_type(i2) # revealed: ~A + reveal_type(i3) # revealed: ~A + reveal_type(i4) # revealed: ~A + reveal_type(i5) # revealed: ~A + reveal_type(i6) # revealed: ~A +``` + +#### Negative type and positive subtype + +When `A` is a supertype of `B`, its negation `~A` is disjoint from `B`, so we can simplify the +intersection to `Never`: + +```py +from knot_extensions import Intersection, Not +from typing import Any + +class A: ... +class B(A): ... +class C(B): ... +class Unrelated: ... + +def _( + i1: Intersection[Not[A], B], + i2: Intersection[B, Not[A]], + i3: Intersection[Not[A], C], + i4: Intersection[C, Not[A]], + i5: Intersection[Unrelated, Not[A], B], + i6: Intersection[B, Not[A], Not[Unrelated]], + i7: Intersection[Any, Not[A], B], + i8: Intersection[B, Not[A], Not[Any]], +) -> None: + reveal_type(i1) # revealed: Never + reveal_type(i2) # revealed: Never + reveal_type(i3) # revealed: Never + reveal_type(i4) # revealed: Never + reveal_type(i5) # revealed: Never + reveal_type(i6) # revealed: Never + reveal_type(i7) # revealed: Never + reveal_type(i8) # revealed: Never +``` + +## Non fully-static types + +### Negation of dynamic types + +`Any` represents the dynamic type, an unknown set of runtime values. The negation of that, `~Any`, +is still an unknown set of runtime values, so `~Any` is equivalent to `Any`. We therefore eagerly +simplify `~Any` to `Any` in intersections. The same applies to `Unknown`. + +```py +from knot_extensions import Intersection, Not, Unknown +from typing_extensions import Any, Never + +class P: ... + +def any( + i1: Not[Any], + i2: Intersection[P, Not[Any]], + i3: Intersection[Never, Not[Any]], +) -> None: + reveal_type(i1) # revealed: Any + reveal_type(i2) # revealed: P & Any + reveal_type(i3) # revealed: Never + +def unknown( + i1: Not[Unknown], + i2: Intersection[P, Not[Unknown]], + i3: Intersection[Never, Not[Unknown]], +) -> None: + reveal_type(i1) # revealed: Unknown + reveal_type(i2) # revealed: P & Unknown + reveal_type(i3) # revealed: Never +``` + +### Collapsing of multiple `Any`/`Unknown` contributions + +The intersection of an unknown set of runtime values with (another) unknown set of runtime values is +still an unknown set of runtime values: + +```py +from knot_extensions import Intersection, Not, Unknown +from typing_extensions import Any + +class P: ... + +def any( + i1: Intersection[Any, Any], + i2: Intersection[P, Any, Any], + i3: Intersection[Any, P, Any], + i4: Intersection[Any, Any, P], +) -> None: + reveal_type(i1) # revealed: Any + reveal_type(i2) # revealed: P & Any + reveal_type(i3) # revealed: Any & P + reveal_type(i4) # revealed: Any & P + +def unknown( + i1: Intersection[Unknown, Unknown], + i2: Intersection[P, Unknown, Unknown], + i3: Intersection[Unknown, P, Unknown], + i4: Intersection[Unknown, Unknown, P], +) -> None: + reveal_type(i1) # revealed: Unknown + reveal_type(i2) # revealed: P & Unknown + reveal_type(i3) # revealed: Unknown & P + reveal_type(i4) # revealed: Unknown & P +``` + +### No self-cancellation + +Dynamic types do not cancel each other out. Intersecting an unknown set of values with the negation +of another unknown set of values is not necessarily empty, so we keep the positive contribution: + +```py +from knot_extensions import Intersection, Not, Unknown + +def any( + i1: Intersection[Any, Not[Any]], + i2: Intersection[Not[Any], Any], +) -> None: + reveal_type(i1) # revealed: Any + reveal_type(i2) # revealed: Any + +def unknown( + i1: Intersection[Unknown, Not[Unknown]], + i2: Intersection[Not[Unknown], Unknown], +) -> None: + reveal_type(i1) # revealed: Unknown + reveal_type(i2) # revealed: Unknown +``` + +### Mixed dynamic types + +We currently do not simplify mixed dynamic types, but might consider doing so in the future: + +```py +from knot_extensions import Intersection, Not, Unknown + +def mixed( + i1: Intersection[Any, Unknown], + i2: Intersection[Any, Not[Unknown]], + i3: Intersection[Not[Any], Unknown], + i4: Intersection[Not[Any], Not[Unknown]], +) -> None: + reveal_type(i1) # revealed: Any & Unknown + reveal_type(i2) # revealed: Any & Unknown + reveal_type(i3) # revealed: Any & Unknown + reveal_type(i4) # revealed: Any & Unknown +``` + +[complement laws]: https://en.wikipedia.org/wiki/Complement_(set_theory) +[de morgan's laws]: https://en.wikipedia.org/wiki/De_Morgan%27s_laws diff --git a/crates/red_knot_python_semantic/resources/mdtest/union_types.md b/crates/red_knot_python_semantic/resources/mdtest/union_types.md index b13dc527f9735..2fa27ca2113de 100644 --- a/crates/red_knot_python_semantic/resources/mdtest/union_types.md +++ b/crates/red_knot_python_semantic/resources/mdtest/union_types.md @@ -123,3 +123,21 @@ from knot_extensions import Unknown def _(u1: str | Unknown | int | object): reveal_type(u1) # revealed: Unknown | object ``` + +## Union of intersections + +We can simplify unions of intersections: + +```py +from knot_extensions import Intersection, Not + +class P: ... +class Q: ... + +def _( + i1: Intersection[P, Q] | Intersection[P, Q], + i2: Intersection[P, Q] | Intersection[Q, P], +) -> None: + reveal_type(i1) # revealed: P & Q + reveal_type(i2) # revealed: P & Q +``` diff --git a/crates/red_knot_python_semantic/src/types/builder.rs b/crates/red_knot_python_semantic/src/types/builder.rs index a24b7450905d4..9671e1ba8dac9 100644 --- a/crates/red_knot_python_semantic/src/types/builder.rs +++ b/crates/red_knot_python_semantic/src/types/builder.rs @@ -321,6 +321,14 @@ impl<'db> InnerIntersectionBuilder<'db> { self.add_positive(db, *neg); } } + Type::Never => { + // Adding ~Never to an intersection is a no-op. + } + Type::Instance(instance) if instance.class.is_known(db, KnownClass::Object) => { + // Adding ~object to an intersection results in Never. + *self = Self::default(); + self.positive.insert(Type::Never); + } ty @ Type::Dynamic(_) => { // Adding any of these types to the negative side of an intersection // is equivalent to adding it to the positive side. We do this to @@ -386,33 +394,34 @@ impl<'db> InnerIntersectionBuilder<'db> { #[cfg(test)] mod tests { - use super::{IntersectionBuilder, IntersectionType, Type, UnionType}; + use super::{IntersectionBuilder, Type, UnionBuilder, UnionType}; - use crate::db::tests::{setup_db, TestDb}; - use crate::types::{global_symbol, todo_type, KnownClass, Truthiness, UnionBuilder}; + use crate::db::tests::setup_db; + use crate::types::{KnownClass, Truthiness}; - use ruff_db::files::system_path_to_file; - use ruff_db::system::DbWithTestSystem; use test_case::test_case; #[test] fn build_union_no_elements() { let db = setup_db(); - let ty = UnionBuilder::new(&db).build(); - assert_eq!(ty, Type::Never); + + let empty_union = UnionBuilder::new(&db).build(); + assert_eq!(empty_union, Type::Never); } #[test] fn build_union_single_element() { let db = setup_db(); + let t0 = Type::IntLiteral(0); - let ty = UnionType::from_elements(&db, [t0]); - assert_eq!(ty, t0); + let union = UnionType::from_elements(&db, [t0]); + assert_eq!(union, t0); } #[test] fn build_union_two_elements() { let db = setup_db(); + let t0 = Type::IntLiteral(0); let t1 = Type::IntLiteral(1); let union = UnionType::from_elements(&db, [t0, t1]).expect_union(); @@ -420,499 +429,12 @@ mod tests { assert_eq!(union.elements(&db), &[t0, t1]); } - impl<'db> IntersectionType<'db> { - fn pos_vec(self, db: &'db TestDb) -> Vec> { - self.positive(db).into_iter().copied().collect() - } - - fn neg_vec(self, db: &'db TestDb) -> Vec> { - self.negative(db).into_iter().copied().collect() - } - } - - #[test] - fn build_intersection() { - let db = setup_db(); - let t0 = Type::IntLiteral(0); - let ta = Type::any(); - let intersection = IntersectionBuilder::new(&db) - .add_positive(ta) - .add_negative(t0) - .build() - .expect_intersection(); - - assert_eq!(intersection.pos_vec(&db), &[ta]); - assert_eq!(intersection.neg_vec(&db), &[t0]); - } - #[test] fn build_intersection_empty_intersection_equals_object() { let db = setup_db(); - let ty = IntersectionBuilder::new(&db).build(); - - assert_eq!(ty, KnownClass::Object.to_instance(&db)); - } - - #[test] - fn build_intersection_flatten_positive() { - let db = setup_db(); - let ta = Type::any(); - let t1 = Type::IntLiteral(1); - let t2 = Type::IntLiteral(2); - let i0 = IntersectionBuilder::new(&db) - .add_positive(ta) - .add_negative(t1) - .build(); - let intersection = IntersectionBuilder::new(&db) - .add_positive(t2) - .add_positive(i0) - .build() - .expect_intersection(); - - assert_eq!(intersection.pos_vec(&db), &[t2, ta]); - assert_eq!(intersection.neg_vec(&db), &[]); - } - - #[test] - fn build_intersection_flatten_negative() { - let db = setup_db(); - let ta = Type::any(); - let t1 = Type::IntLiteral(1); - let t2 = KnownClass::Int.to_instance(&db); - // i0 = Any & ~Literal[1] - let i0 = IntersectionBuilder::new(&db) - .add_positive(ta) - .add_negative(t1) - .build(); - // ta_not_i0 = int & ~(Any & ~Literal[1]) - // -> int & (~Any | Literal[1]) - // (~Any is equivalent to Any) - // -> (int & Any) | (int & Literal[1]) - // -> (int & Any) | Literal[1] - let ta_not_i0 = IntersectionBuilder::new(&db) - .add_positive(t2) - .add_negative(i0) - .build(); - - assert_eq!(ta_not_i0.display(&db).to_string(), "int & Any | Literal[1]"); - } - - #[test] - fn build_intersection_simplify_negative_any() { - let db = setup_db(); - - let ty = IntersectionBuilder::new(&db) - .add_negative(Type::any()) - .build(); - assert_eq!(ty, Type::any()); - - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::Never) - .add_negative(Type::any()) - .build(); - assert_eq!(ty, Type::Never); - } - - #[test] - fn build_intersection_simplify_multiple_unknown() { - let db = setup_db(); - - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::unknown()) - .add_positive(Type::unknown()) - .build(); - assert_eq!(ty, Type::unknown()); - - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::unknown()) - .add_negative(Type::unknown()) - .build(); - assert_eq!(ty, Type::unknown()); - - let ty = IntersectionBuilder::new(&db) - .add_negative(Type::unknown()) - .add_negative(Type::unknown()) - .build(); - assert_eq!(ty, Type::unknown()); - - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::unknown()) - .add_positive(Type::IntLiteral(0)) - .add_negative(Type::unknown()) - .build(); - assert_eq!( - ty, - IntersectionBuilder::new(&db) - .add_positive(Type::unknown()) - .add_positive(Type::IntLiteral(0)) - .build() - ); - } - - #[test] - fn intersection_distributes_over_union() { - let db = setup_db(); - let t0 = Type::IntLiteral(0); - let t1 = Type::IntLiteral(1); - let ta = Type::any(); - let u0 = UnionType::from_elements(&db, [t0, t1]); - - let union = IntersectionBuilder::new(&db) - .add_positive(ta) - .add_positive(u0) - .build() - .expect_union(); - let [Type::Intersection(i0), Type::Intersection(i1)] = union.elements(&db)[..] else { - panic!("expected a union of two intersections"); - }; - assert_eq!(i0.pos_vec(&db), &[ta, t0]); - assert_eq!(i1.pos_vec(&db), &[ta, t1]); - } - - #[test] - fn intersection_negation_distributes_over_union() { - let mut db = setup_db(); - db.write_dedented( - "/src/module.py", - r#" - class A: ... - class B: ... - "#, - ) - .unwrap(); - let module = ruff_db::files::system_path_to_file(&db, "/src/module.py").unwrap(); - - let a = global_symbol(&db, module, "A") - .expect_type() - .to_instance(&db); - let b = global_symbol(&db, module, "B") - .expect_type() - .to_instance(&db); - - // intersection: A & B - let intersection = IntersectionBuilder::new(&db) - .add_positive(a) - .add_positive(b) - .build() - .expect_intersection(); - assert_eq!(intersection.pos_vec(&db), &[a, b]); - assert_eq!(intersection.neg_vec(&db), &[]); - - // ~intersection => ~A | ~B - let negated_intersection = IntersectionBuilder::new(&db) - .add_negative(Type::Intersection(intersection)) - .build() - .expect_union(); - - // should have as elements ~A and ~B - let not_a = a.negate(&db); - let not_b = b.negate(&db); - assert_eq!(negated_intersection.elements(&db), &[not_a, not_b]); - } - - #[test] - fn mixed_intersection_negation_distributes_over_union() { - let mut db = setup_db(); - db.write_dedented( - "/src/module.py", - r#" - class A: ... - class B: ... - "#, - ) - .unwrap(); - let module = ruff_db::files::system_path_to_file(&db, "/src/module.py").unwrap(); - - let a = global_symbol(&db, module, "A") - .expect_type() - .to_instance(&db); - let b = global_symbol(&db, module, "B") - .expect_type() - .to_instance(&db); - let int = KnownClass::Int.to_instance(&db); - - // a_not_b: A & ~B - let a_not_b = IntersectionBuilder::new(&db) - .add_positive(a) - .add_negative(b) - .build() - .expect_intersection(); - assert_eq!(a_not_b.pos_vec(&db), &[a]); - assert_eq!(a_not_b.neg_vec(&db), &[b]); - - // let's build - // int & ~(A & ~B) - // = int & ~(A & ~B) - // = int & (~A | B) - // = (int & ~A) | (int & B) - let t = IntersectionBuilder::new(&db) - .add_positive(int) - .add_negative(Type::Intersection(a_not_b)) - .build(); - assert_eq!(t.display(&db).to_string(), "int & ~A | int & B"); - } - - #[test] - fn build_intersection_self_negation() { - let db = setup_db(); - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::none(&db)) - .add_negative(Type::none(&db)) - .build(); - - assert_eq!(ty, Type::Never); - } - - #[test] - fn build_intersection_simplify_negative_never() { - let db = setup_db(); - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::none(&db)) - .add_negative(Type::Never) - .build(); - - assert_eq!(ty, Type::none(&db)); - } - - #[test] - fn build_intersection_simplify_positive_never() { - let db = setup_db(); - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::none(&db)) - .add_positive(Type::Never) - .build(); - - assert_eq!(ty, Type::Never); - } - - #[test] - fn build_intersection_simplify_negative_none() { - let db = setup_db(); - - let ty = IntersectionBuilder::new(&db) - .add_negative(Type::none(&db)) - .add_positive(Type::IntLiteral(1)) - .build(); - assert_eq!(ty, Type::IntLiteral(1)); - - let ty = IntersectionBuilder::new(&db) - .add_positive(Type::IntLiteral(1)) - .add_negative(Type::none(&db)) - .build(); - assert_eq!(ty, Type::IntLiteral(1)); - } - - #[test] - fn build_negative_union_de_morgan() { - let db = setup_db(); - - let union = UnionBuilder::new(&db) - .add(Type::IntLiteral(1)) - .add(Type::IntLiteral(2)) - .build(); - assert_eq!(union.display(&db).to_string(), "Literal[1, 2]"); - - let ty = IntersectionBuilder::new(&db).add_negative(union).build(); - - let expected = IntersectionBuilder::new(&db) - .add_negative(Type::IntLiteral(1)) - .add_negative(Type::IntLiteral(2)) - .build(); - - assert_eq!(ty.display(&db).to_string(), "~Literal[1] & ~Literal[2]"); - assert_eq!(ty, expected); - } - - #[test] - fn build_intersection_simplify_positive_type_and_positive_subtype() { - let db = setup_db(); - - let t = KnownClass::Str.to_instance(&db); - let s = Type::LiteralString; - - let ty = IntersectionBuilder::new(&db) - .add_positive(t) - .add_positive(s) - .build(); - assert_eq!(ty, s); - - let ty = IntersectionBuilder::new(&db) - .add_positive(s) - .add_positive(t) - .build(); - assert_eq!(ty, s); - - let literal = Type::string_literal(&db, "a"); - let expected = IntersectionBuilder::new(&db) - .add_positive(s) - .add_negative(literal) - .build(); - - let ty = IntersectionBuilder::new(&db) - .add_positive(t) - .add_negative(literal) - .add_positive(s) - .build(); - assert_eq!(ty, expected); - - let ty = IntersectionBuilder::new(&db) - .add_positive(s) - .add_negative(literal) - .add_positive(t) - .build(); - assert_eq!(ty, expected); - } - - #[test] - fn build_intersection_simplify_negative_type_and_negative_subtype() { - let db = setup_db(); - - let t = KnownClass::Str.to_instance(&db); - let s = Type::LiteralString; - - let expected = IntersectionBuilder::new(&db).add_negative(t).build(); - - let ty = IntersectionBuilder::new(&db) - .add_negative(t) - .add_negative(s) - .build(); - assert_eq!(ty, expected); - - let ty = IntersectionBuilder::new(&db) - .add_negative(s) - .add_negative(t) - .build(); - assert_eq!(ty, expected); - - let object = KnownClass::Object.to_instance(&db); - let expected = IntersectionBuilder::new(&db) - .add_negative(t) - .add_positive(object) - .build(); - - let ty = IntersectionBuilder::new(&db) - .add_negative(t) - .add_positive(object) - .add_negative(s) - .build(); - assert_eq!(ty, expected); - } - - #[test] - fn build_intersection_simplify_negative_type_and_multiple_negative_subtypes() { - let db = setup_db(); - - let s1 = Type::IntLiteral(1); - let s2 = Type::IntLiteral(2); - let t = KnownClass::Int.to_instance(&db); - - let expected = IntersectionBuilder::new(&db).add_negative(t).build(); - - let ty = IntersectionBuilder::new(&db) - .add_negative(s1) - .add_negative(s2) - .add_negative(t) - .build(); - assert_eq!(ty, expected); - } - - #[test] - fn build_intersection_simplify_negative_type_and_positive_subtype() { - let db = setup_db(); - - let t = KnownClass::Str.to_instance(&db); - let s = Type::LiteralString; - - let ty = IntersectionBuilder::new(&db) - .add_negative(t) - .add_positive(s) - .build(); - assert_eq!(ty, Type::Never); - - let ty = IntersectionBuilder::new(&db) - .add_positive(s) - .add_negative(t) - .build(); - assert_eq!(ty, Type::Never); - - // This should also work in the presence of additional contributions: - let ty = IntersectionBuilder::new(&db) - .add_positive(KnownClass::Object.to_instance(&db)) - .add_negative(t) - .add_positive(s) - .build(); - assert_eq!(ty, Type::Never); - - let ty = IntersectionBuilder::new(&db) - .add_positive(s) - .add_negative(Type::string_literal(&db, "a")) - .add_negative(t) - .build(); - assert_eq!(ty, Type::Never); - } - - #[test] - fn build_intersection_simplify_disjoint_positive_types() { - let db = setup_db(); - - let t1 = Type::IntLiteral(1); - let t2 = Type::none(&db); - - let ty = IntersectionBuilder::new(&db) - .add_positive(t1) - .add_positive(t2) - .build(); - assert_eq!(ty, Type::Never); - - // If there are any negative contributions, they should - // be removed too. - let ty = IntersectionBuilder::new(&db) - .add_positive(KnownClass::Str.to_instance(&db)) - .add_negative(Type::LiteralString) - .add_positive(t2) - .build(); - assert_eq!(ty, Type::Never); - } - - #[test] - fn build_intersection_simplify_disjoint_positive_and_negative_types() { - let db = setup_db(); - - let t_p = KnownClass::Int.to_instance(&db); - let t_n = Type::string_literal(&db, "t_n"); - - let ty = IntersectionBuilder::new(&db) - .add_positive(t_p) - .add_negative(t_n) - .build(); - assert_eq!(ty, t_p); - - let ty = IntersectionBuilder::new(&db) - .add_negative(t_n) - .add_positive(t_p) - .build(); - assert_eq!(ty, t_p); - - let int_literal = Type::IntLiteral(1); - let expected = IntersectionBuilder::new(&db) - .add_positive(t_p) - .add_negative(int_literal) - .build(); - - let ty = IntersectionBuilder::new(&db) - .add_positive(t_p) - .add_negative(int_literal) - .add_negative(t_n) - .build(); - assert_eq!(ty, expected); - - let ty = IntersectionBuilder::new(&db) - .add_negative(t_n) - .add_negative(int_literal) - .add_positive(t_p) - .build(); - assert_eq!(ty, expected); + let intersection = IntersectionBuilder::new(&db).build(); + assert_eq!(intersection, KnownClass::Object.to_instance(&db)); } #[test_case(Type::BooleanLiteral(true))] @@ -957,85 +479,4 @@ mod tests { .build(); assert_eq!(ty, Type::BooleanLiteral(!bool_value)); } - - #[test_case(Type::any())] - #[test_case(Type::unknown())] - #[test_case(todo_type!())] - fn build_intersection_t_and_negative_t_does_not_simplify(ty: Type) { - let db = setup_db(); - - let result = IntersectionBuilder::new(&db) - .add_positive(ty) - .add_negative(ty) - .build(); - assert_eq!(result, ty); - - let result = IntersectionBuilder::new(&db) - .add_negative(ty) - .add_positive(ty) - .build(); - assert_eq!(result, ty); - } - - #[test] - fn build_intersection_of_two_unions_simplify() { - let mut db = setup_db(); - db.write_dedented( - "/src/module.py", - " - class A: ... - class B: ... - a = A() - b = B() - ", - ) - .unwrap(); - - let file = system_path_to_file(&db, "src/module.py").expect("file to exist"); - - let a = global_symbol(&db, file, "a").expect_type(); - let b = global_symbol(&db, file, "b").expect_type(); - let union = UnionBuilder::new(&db).add(a).add(b).build(); - assert_eq!(union.display(&db).to_string(), "A | B"); - let reversed_union = UnionBuilder::new(&db).add(b).add(a).build(); - assert_eq!(reversed_union.display(&db).to_string(), "B | A"); - let intersection = IntersectionBuilder::new(&db) - .add_positive(union) - .add_positive(reversed_union) - .build(); - assert_eq!(intersection.display(&db).to_string(), "B | A"); - } - - #[test] - fn build_union_of_two_intersections_simplify() { - let mut db = setup_db(); - db.write_dedented( - "/src/module.py", - " - class A: ... - class B: ... - a = A() - b = B() - ", - ) - .unwrap(); - - let file = system_path_to_file(&db, "src/module.py").expect("file to exist"); - - let a = global_symbol(&db, file, "a").expect_type(); - let b = global_symbol(&db, file, "b").expect_type(); - let intersection = IntersectionBuilder::new(&db) - .add_positive(a) - .add_positive(b) - .build(); - let reversed_intersection = IntersectionBuilder::new(&db) - .add_positive(b) - .add_positive(a) - .build(); - let union = UnionBuilder::new(&db) - .add(intersection) - .add(reversed_intersection) - .build(); - assert_eq!(union.display(&db).to_string(), "A & B"); - } } diff --git a/crates/red_knot_python_semantic/src/types/infer.rs b/crates/red_knot_python_semantic/src/types/infer.rs index fd263a883619d..4dea24874dec4 100644 --- a/crates/red_knot_python_semantic/src/types/infer.rs +++ b/crates/red_knot_python_semantic/src/types/infer.rs @@ -310,6 +310,18 @@ enum IntersectionOn { Right, } +/// A helper to track if we already know that declared and inferred types are the same. +#[derive(Debug, Clone, PartialEq, Eq)] +enum DeclaredAndInferredType<'db> { + /// We know that both the declared and inferred types are the same. + AreTheSame(Type<'db>), + /// Declared and inferred types might be different, we need to check assignability. + MightBeDifferent { + declared_ty: Type<'db>, + inferred_ty: Type<'db>, + }, +} + /// Builder to infer all types in a region. /// /// A builder is used by creating it with [`new()`](TypeInferenceBuilder::new), and then calling @@ -895,20 +907,28 @@ impl<'db> TypeInferenceBuilder<'db> { &mut self, node: AnyNodeRef, definition: Definition<'db>, - declared_ty: Type<'db>, - inferred_ty: Type<'db>, + declared_and_inferred_ty: &DeclaredAndInferredType<'db>, ) { debug_assert!(definition.is_binding(self.db())); debug_assert!(definition.is_declaration(self.db())); - let inferred_ty = if inferred_ty.is_assignable_to(self.db(), declared_ty) { - inferred_ty - } else { - report_invalid_assignment(&self.context, node, declared_ty, inferred_ty); - // if the assignment is invalid, fall back to assuming the annotation is correct - declared_ty + + let (declared_ty, inferred_ty) = match declared_and_inferred_ty { + DeclaredAndInferredType::AreTheSame(ty) => (ty, ty), + DeclaredAndInferredType::MightBeDifferent { + declared_ty, + inferred_ty, + } => { + if inferred_ty.is_assignable_to(self.db(), *declared_ty) { + (declared_ty, inferred_ty) + } else { + report_invalid_assignment(&self.context, node, *declared_ty, *inferred_ty); + // if the assignment is invalid, fall back to assuming the annotation is correct + (declared_ty, declared_ty) + } + } }; - self.types.declarations.insert(definition, declared_ty); - self.types.bindings.insert(definition, inferred_ty); + self.types.declarations.insert(definition, *declared_ty); + self.types.bindings.insert(definition, *inferred_ty); } fn add_unknown_declaration_with_binding( @@ -916,7 +936,11 @@ impl<'db> TypeInferenceBuilder<'db> { node: AnyNodeRef, definition: Definition<'db>, ) { - self.add_declaration_with_binding(node, definition, Type::unknown(), Type::unknown()); + self.add_declaration_with_binding( + node, + definition, + &DeclaredAndInferredType::AreTheSame(Type::unknown()), + ); } fn infer_module(&mut self, module: &ast::ModModule) { @@ -1097,7 +1121,11 @@ impl<'db> TypeInferenceBuilder<'db> { decorator_tys.into_boxed_slice(), )); - self.add_declaration_with_binding(function.into(), definition, function_ty, function_ty); + self.add_declaration_with_binding( + function.into(), + definition, + &DeclaredAndInferredType::AreTheSame(function_ty), + ); } fn infer_parameters(&mut self, parameters: &ast::Parameters) { @@ -1188,15 +1216,18 @@ impl<'db> TypeInferenceBuilder<'db> { .map(|default| self.file_expression_ty(default)); if let Some(annotation) = parameter.annotation.as_ref() { let declared_ty = self.file_expression_ty(annotation); - let inferred_ty = if let Some(default_ty) = default_ty { + let declared_and_inferred_ty = if let Some(default_ty) = default_ty { if default_ty.is_assignable_to(self.db(), declared_ty) { - UnionType::from_elements(self.db(), [declared_ty, default_ty]) + DeclaredAndInferredType::MightBeDifferent { + declared_ty, + inferred_ty: UnionType::from_elements(self.db(), [declared_ty, default_ty]), + } } else if self.in_stub() && default .as_ref() .is_some_and(|d| d.is_ellipsis_literal_expr()) { - declared_ty + DeclaredAndInferredType::AreTheSame(declared_ty) } else { self.context.report_lint( &INVALID_PARAMETER_DEFAULT, @@ -1205,16 +1236,15 @@ impl<'db> TypeInferenceBuilder<'db> { "Default value of type `{}` is not assignable to annotated parameter type `{}`", default_ty.display(self.db()), declared_ty.display(self.db())), ); - declared_ty + DeclaredAndInferredType::AreTheSame(declared_ty) } } else { - declared_ty + DeclaredAndInferredType::AreTheSame(declared_ty) }; self.add_declaration_with_binding( parameter.into(), definition, - declared_ty, - inferred_ty, + &declared_and_inferred_ty, ); } else { let ty = if let Some(default_ty) = default_ty { @@ -1240,7 +1270,11 @@ impl<'db> TypeInferenceBuilder<'db> { let _annotated_ty = self.file_expression_ty(annotation); // TODO `tuple[annotated_ty, ...]` let ty = KnownClass::Tuple.to_instance(self.db()); - self.add_declaration_with_binding(parameter.into(), definition, ty, ty); + self.add_declaration_with_binding( + parameter.into(), + definition, + &DeclaredAndInferredType::AreTheSame(ty), + ); } else { self.add_binding( parameter.into(), @@ -1265,7 +1299,11 @@ impl<'db> TypeInferenceBuilder<'db> { let _annotated_ty = self.file_expression_ty(annotation); // TODO `dict[str, annotated_ty]` let ty = KnownClass::Dict.to_instance(self.db()); - self.add_declaration_with_binding(parameter.into(), definition, ty, ty); + self.add_declaration_with_binding( + parameter.into(), + definition, + &DeclaredAndInferredType::AreTheSame(ty), + ); } else { self.add_binding( parameter.into(), @@ -1308,7 +1346,11 @@ impl<'db> TypeInferenceBuilder<'db> { let class = Class::new(self.db(), &name.id, body_scope, maybe_known_class); let class_ty = Type::class_literal(class); - self.add_declaration_with_binding(class_node.into(), definition, class_ty, class_ty); + self.add_declaration_with_binding( + class_node.into(), + definition, + &DeclaredAndInferredType::AreTheSame(class_ty), + ); // if there are type parameters, then the keywords and bases are within that scope // and we don't need to run inference here @@ -1365,8 +1407,7 @@ impl<'db> TypeInferenceBuilder<'db> { self.add_declaration_with_binding( type_alias.into(), definition, - type_alias_ty, - type_alias_ty, + &DeclaredAndInferredType::AreTheSame(type_alias_ty), ); } @@ -1718,7 +1759,11 @@ impl<'db> TypeInferenceBuilder<'db> { bound_or_constraint, default_ty, ))); - self.add_declaration_with_binding(node.into(), definition, ty, ty); + self.add_declaration_with_binding( + node.into(), + definition, + &DeclaredAndInferredType::AreTheSame(ty), + ); } fn infer_paramspec_definition( @@ -1733,7 +1778,11 @@ impl<'db> TypeInferenceBuilder<'db> { } = node; self.infer_optional_expression(default.as_deref()); let pep_695_todo = todo_type!("PEP-695 ParamSpec definition types"); - self.add_declaration_with_binding(node.into(), definition, pep_695_todo, pep_695_todo); + self.add_declaration_with_binding( + node.into(), + definition, + &DeclaredAndInferredType::AreTheSame(pep_695_todo), + ); } fn infer_typevartuple_definition( @@ -1748,7 +1797,11 @@ impl<'db> TypeInferenceBuilder<'db> { } = node; self.infer_optional_expression(default.as_deref()); let pep_695_todo = todo_type!("PEP-695 TypeVarTuple definition types"); - self.add_declaration_with_binding(node.into(), definition, pep_695_todo, pep_695_todo); + self.add_declaration_with_binding( + node.into(), + definition, + &DeclaredAndInferredType::AreTheSame(pep_695_todo), + ); } fn infer_match_statement(&mut self, match_statement: &ast::StmtMatch) { @@ -2006,13 +2059,13 @@ impl<'db> TypeInferenceBuilder<'db> { simple: _, } = assignment; - let mut annotation_ty = self.infer_annotation_expression( + let mut declared_ty = self.infer_annotation_expression( annotation, DeferredExpressionState::from(self.are_all_types_deferred()), ); // Handle various singletons. - if let Type::Instance(InstanceType { class }) = annotation_ty { + if let Type::Instance(InstanceType { class }) = declared_ty { if class.is_known(self.db(), KnownClass::SpecialForm) { if let Some(name_expr) = target.as_name_expr() { if let Some(known_instance) = KnownInstanceType::try_from_file_and_name( @@ -2020,27 +2073,29 @@ impl<'db> TypeInferenceBuilder<'db> { self.file(), &name_expr.id, ) { - annotation_ty = Type::KnownInstance(known_instance); + declared_ty = Type::KnownInstance(known_instance); } } } } if let Some(value) = value.as_deref() { - let value_ty = self.infer_expression(value); - let value_ty = if self.in_stub() && value.is_ellipsis_literal_expr() { - annotation_ty + let inferred_ty = self.infer_expression(value); + let inferred_ty = if self.in_stub() && value.is_ellipsis_literal_expr() { + declared_ty } else { - value_ty + inferred_ty }; self.add_declaration_with_binding( assignment.into(), definition, - annotation_ty, - value_ty, + &DeclaredAndInferredType::MightBeDifferent { + declared_ty, + inferred_ty, + }, ); } else { - self.add_declaration(assignment.into(), definition, annotation_ty); + self.add_declaration(assignment.into(), definition, declared_ty); } self.infer_expression(target); @@ -2294,7 +2349,11 @@ impl<'db> TypeInferenceBuilder<'db> { full_module_ty }; - self.add_declaration_with_binding(alias.into(), definition, binding_ty, binding_ty); + self.add_declaration_with_binding( + alias.into(), + definition, + &DeclaredAndInferredType::AreTheSame(binding_ty), + ); } fn infer_import_from_statement(&mut self, import: &ast::StmtImportFrom) { @@ -2470,7 +2529,11 @@ impl<'db> TypeInferenceBuilder<'db> { format_args!("Member `{name}` of module `{module_name}` is possibly unbound",), ); } - self.add_declaration_with_binding(alias.into(), definition, ty, ty); + self.add_declaration_with_binding( + alias.into(), + definition, + &DeclaredAndInferredType::AreTheSame(ty), + ); return; }; @@ -2496,8 +2559,7 @@ impl<'db> TypeInferenceBuilder<'db> { self.add_declaration_with_binding( alias.into(), definition, - submodule_ty, - submodule_ty, + &DeclaredAndInferredType::AreTheSame(submodule_ty), ); return; }