[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](e01da82a5a..e7e432bca2 (r1819924085)).

## Test Plan

Running the new Markdown tests

---------

Co-authored-by: Alex Waygood <Alex.Waygood@Gmail.com>

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

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
+```

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::db::tests::setup_db;
-    use crate::types::{global_symbol, todo_type, KnownClass, Truthiness, UnionBuilder};
+    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]);
+        let union = UnionType::from_elements(&db, [t0]);
-        assert_eq!(ty, 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<Type<'db>> {
-            self.positive(db).into_iter().copied().collect()
-        }
-
-        fn neg_vec(self, db: &'db TestDb) -> Vec<Type<'db>> {
-            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();
+        let intersection = IntersectionBuilder::new(&db).build();
-
+        assert_eq!(intersection, KnownClass::Object.to_instance(&db));
-        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);
     }
 
     #[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");
-    }
 }

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>,
+        declared_and_inferred_ty: &DeclaredAndInferredType<'db>,
-        inferred_ty: Type<'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
+        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);
+                    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, declared_ty)
+                }
+            }
         };
-        self.types.declarations.insert(definition, declared_ty);
+        self.types.declarations.insert(definition, *declared_ty);
-        self.types.bindings.insert(definition, inferred_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,
+                &declared_and_inferred_ty,
-                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,
+            &DeclaredAndInferredType::AreTheSame(type_alias_ty),
-            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 inferred_ty = self.infer_expression(value);
-            let value_ty = if self.in_stub() && value.is_ellipsis_literal_expr() {
+            let inferred_ty = if self.in_stub() && value.is_ellipsis_literal_expr() {
-                annotation_ty
+                declared_ty
             } else {
-                value_ty
+                inferred_ty
             };
             self.add_declaration_with_binding(
                 assignment.into(),
                 definition,
-                annotation_ty,
+                &DeclaredAndInferredType::MightBeDifferent {
-                value_ty,
+                    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,
+                    &DeclaredAndInferredType::AreTheSame(submodule_ty),
-                    submodule_ty,
                 );
                 return;
             }