From b435a03da1224b659152b5bd752b845dd54be7ea Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Sun, 26 Jan 2025 12:57:45 +0000
Subject: [PATCH 01/10] Use union types instead of join in binder

---
 mypy/binder.py                      | 42 ++++++++++++-------------
 mypy/join.py                        | 49 -----------------------------
 mypy/test/testtypes.py              | 10 +++---
 test-data/unit/check-python310.test |  8 +++--
 test-data/unit/check-redefine.test  |  2 +-
 5 files changed, 31 insertions(+), 80 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 3d833153d628..82044bfb5f00 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -7,10 +7,10 @@
 from typing_extensions import TypeAlias as _TypeAlias
 
 from mypy.erasetype import remove_instance_last_known_values
-from mypy.join import join_simple
 from mypy.literals import Key, literal, literal_hash, subkeys
 from mypy.nodes import Expression, IndexExpr, MemberExpr, NameExpr, RefExpr, TypeInfo, Var
 from mypy.subtypes import is_same_type, is_subtype
+from mypy.typeops import make_simplified_union
 from mypy.types import (
     AnyType,
     Instance,
@@ -237,27 +237,25 @@ def update_from_options(self, frames: list[Frame]) -> bool:
                 ):
                     type = AnyType(TypeOfAny.from_another_any, source_any=declaration_type)
             else:
-                for other in resulting_values[1:]:
-                    assert other is not None
-                    type = join_simple(self.declarations[key], type, other.type)
-                    # Try simplifying resulting type for unions involving variadic tuples.
-                    # Technically, everything is still valid without this step, but if we do
-                    # not do this, this may create long unions after exiting an if check like:
-                    #     x: tuple[int, ...]
-                    #     if len(x) < 10:
-                    #         ...
-                    # We want the type of x to be tuple[int, ...] after this block (if it is
-                    # still equivalent to such type).
-                    if isinstance(type, UnionType):
-                        type = collapse_variadic_union(type)
-                    if isinstance(type, ProperType) and isinstance(type, UnionType):
-                        # Simplify away any extra Any's that were added to the declared
-                        # type when popping a frame.
-                        simplified = UnionType.make_union(
-                            [t for t in type.items if not isinstance(get_proper_type(t), AnyType)]
-                        )
-                        if simplified == self.declarations[key]:
-                            type = simplified
+                type = make_simplified_union([t.type for t in resulting_values])
+                # Try simplifying resulting type for unions involving variadic tuples.
+                # Technically, everything is still valid without this step, but if we do
+                # not do this, this may create long unions after exiting an if check like:
+                #     x: tuple[int, ...]
+                #     if len(x) < 10:
+                #         ...
+                # We want the type of x to be tuple[int, ...] after this block (if it is
+                # still equivalent to such type).
+                if isinstance(type, UnionType):
+                    type = collapse_variadic_union(type)
+                if isinstance(type, ProperType) and isinstance(type, UnionType):
+                    # Simplify away any extra Any's that were added to the declared
+                    # type when popping a frame.
+                    simplified = UnionType.make_union(
+                        [t for t in type.items if not isinstance(get_proper_type(t), AnyType)]
+                    )
+                    if simplified == self.declarations[key]:
+                        type = simplified
             if current_value is None or not is_same_type(type, current_value[0]):
                 self._put(key, type, from_assignment=True)
                 changed = True
diff --git a/mypy/join.py b/mypy/join.py
index 166434f58f8d..c8fcfb66934d 100644
--- a/mypy/join.py
+++ b/mypy/join.py
@@ -183,55 +183,6 @@ def join_instances_via_supertype(self, t: Instance, s: Instance) -> ProperType:
         return best
 
 
-def join_simple(declaration: Type | None, s: Type, t: Type) -> ProperType:
-    """Return a simple least upper bound given the declared type.
-
-    This function should be only used by binder, and should not recurse.
-    For all other uses, use `join_types()`.
-    """
-    declaration = get_proper_type(declaration)
-    s = get_proper_type(s)
-    t = get_proper_type(t)
-
-    if (s.can_be_true, s.can_be_false) != (t.can_be_true, t.can_be_false):
-        # if types are restricted in different ways, use the more general versions
-        s = mypy.typeops.true_or_false(s)
-        t = mypy.typeops.true_or_false(t)
-
-    if isinstance(s, AnyType):
-        return s
-
-    if isinstance(s, ErasedType):
-        return t
-
-    if is_proper_subtype(s, t, ignore_promotions=True):
-        return t
-
-    if is_proper_subtype(t, s, ignore_promotions=True):
-        return s
-
-    if isinstance(declaration, UnionType):
-        return mypy.typeops.make_simplified_union([s, t])
-
-    if isinstance(s, NoneType) and not isinstance(t, NoneType):
-        s, t = t, s
-
-    if isinstance(s, UninhabitedType) and not isinstance(t, UninhabitedType):
-        s, t = t, s
-
-    # Meets/joins require callable type normalization.
-    s, t = normalize_callables(s, t)
-
-    if isinstance(s, UnionType) and not isinstance(t, UnionType):
-        s, t = t, s
-
-    value = t.accept(TypeJoinVisitor(s))
-    if declaration is None or is_subtype(value, declaration):
-        return value
-
-    return declaration
-
-
 def trivial_join(s: Type, t: Type) -> Type:
     """Return one of types (expanded) if it is a supertype of other, otherwise top type."""
     if is_subtype(s, t):
diff --git a/mypy/test/testtypes.py b/mypy/test/testtypes.py
index 35102be80f5d..174441237ab4 100644
--- a/mypy/test/testtypes.py
+++ b/mypy/test/testtypes.py
@@ -7,7 +7,7 @@
 
 from mypy.erasetype import erase_type, remove_instance_last_known_values
 from mypy.indirection import TypeIndirectionVisitor
-from mypy.join import join_simple, join_types
+from mypy.join import join_types
 from mypy.meet import meet_types, narrow_declared_type
 from mypy.nodes import (
     ARG_NAMED,
@@ -817,12 +817,12 @@ def test_any_type(self) -> None:
             self.assert_join(t, self.fx.anyt, self.fx.anyt)
 
     def test_mixed_truth_restricted_type_simple(self) -> None:
-        # join_simple against differently restricted truthiness types drops restrictions.
+        # make_simplified_union against differently restricted truthiness types drops restrictions.
         true_a = true_only(self.fx.a)
         false_o = false_only(self.fx.o)
-        j = join_simple(self.fx.o, true_a, false_o)
-        assert j.can_be_true
-        assert j.can_be_false
+        u = make_simplified_union([true_a, false_o])
+        assert u.can_be_true
+        assert u.can_be_false
 
     def test_mixed_truth_restricted_type(self) -> None:
         # join_types against differently restricted truthiness types drops restrictions.
diff --git a/test-data/unit/check-python310.test b/test-data/unit/check-python310.test
index ea6cc7ffe56a..e10d0c76c717 100644
--- a/test-data/unit/check-python310.test
+++ b/test-data/unit/check-python310.test
@@ -1487,11 +1487,13 @@ match m5:
     case _:
         reveal_type(m5)  # N: Revealed type is "Tuple[Literal[2], Union[Literal['a'], Literal['b']]]"
 
-match m5:
+m6: Tuple[Literal[1, 2], Literal["a", "b"]]
+
+match m6:
     case (1, "a"):
-        reveal_type(m5)  # N: Revealed type is "Tuple[Literal[1], Literal['a']]"
+        reveal_type(m6)  # N: Revealed type is "Tuple[Literal[1], Literal['a']]"
     case _:
-        reveal_type(m5)  # N: Revealed type is "Tuple[Union[Literal[1], Literal[2]], Union[Literal['a'], Literal['b']]]"
+        reveal_type(m6)  # N: Revealed type is "Tuple[Union[Literal[1], Literal[2]], Union[Literal['a'], Literal['b']]]"
 
 [builtins fixtures/tuple.pyi]
 
diff --git a/test-data/unit/check-redefine.test b/test-data/unit/check-redefine.test
index b7642d30efc8..e162bb73a206 100644
--- a/test-data/unit/check-redefine.test
+++ b/test-data/unit/check-redefine.test
@@ -321,7 +321,7 @@ def f() -> None:
     x = 1
     if int():
         x = ''
-    reveal_type(x) # N: Revealed type is "builtins.object"
+    reveal_type(x) # N: Revealed type is "Union[builtins.str, builtins.int]"
     x = ''
     reveal_type(x) # N: Revealed type is "builtins.str"
     if int():

From 6e99af4cc5e677e24387af997138348c48e264e6 Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Sun, 26 Jan 2025 13:35:28 +0000
Subject: [PATCH 02/10] Fix self-check

---
 mypy/binder.py                      | 47 +++++++++++++++++------------
 test-data/unit/check-typeguard.test | 17 +++++++++++
 2 files changed, 45 insertions(+), 19 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 82044bfb5f00..d06c52b0c5c4 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -237,25 +237,34 @@ def update_from_options(self, frames: list[Frame]) -> bool:
                 ):
                     type = AnyType(TypeOfAny.from_another_any, source_any=declaration_type)
             else:
-                type = make_simplified_union([t.type for t in resulting_values])
-                # Try simplifying resulting type for unions involving variadic tuples.
-                # Technically, everything is still valid without this step, but if we do
-                # not do this, this may create long unions after exiting an if check like:
-                #     x: tuple[int, ...]
-                #     if len(x) < 10:
-                #         ...
-                # We want the type of x to be tuple[int, ...] after this block (if it is
-                # still equivalent to such type).
-                if isinstance(type, UnionType):
-                    type = collapse_variadic_union(type)
-                if isinstance(type, ProperType) and isinstance(type, UnionType):
-                    # Simplify away any extra Any's that were added to the declared
-                    # type when popping a frame.
-                    simplified = UnionType.make_union(
-                        [t for t in type.items if not isinstance(get_proper_type(t), AnyType)]
-                    )
-                    if simplified == self.declarations[key]:
-                        type = simplified
+                possible_types = []
+                for t in resulting_values:
+                    assert t is not None
+                    possible_types.append(t.type)
+                if len(possible_types) == 1:
+                    # This is to avoid calling get_proper_type() unless needed, as this may
+                    # interfere with our (hacky) TypeGuard support.
+                    type = possible_types[0]
+                else:
+                    type = make_simplified_union(possible_types)
+                    # Try simplifying resulting type for unions involving variadic tuples.
+                    # Technically, everything is still valid without this step, but if we do
+                    # not do this, this may create long unions after exiting an if check like:
+                    #     x: tuple[int, ...]
+                    #     if len(x) < 10:
+                    #         ...
+                    # We want the type of x to be tuple[int, ...] after this block (if it is
+                    # still equivalent to such type).
+                    if isinstance(type, UnionType):
+                        type = collapse_variadic_union(type)
+                    if isinstance(type, ProperType) and isinstance(type, UnionType):
+                        # Simplify away any extra Any's that were added to the declared
+                        # type when popping a frame.
+                        simplified = UnionType.make_union(
+                            [t for t in type.items if not isinstance(get_proper_type(t), AnyType)]
+                        )
+                        if simplified == self.declarations[key]:
+                            type = simplified
             if current_value is None or not is_same_type(type, current_value[0]):
                 self._put(key, type, from_assignment=True)
                 changed = True
diff --git a/test-data/unit/check-typeguard.test b/test-data/unit/check-typeguard.test
index c69e16c5cc9e..71c4473fbfaa 100644
--- a/test-data/unit/check-typeguard.test
+++ b/test-data/unit/check-typeguard.test
@@ -786,3 +786,20 @@ def func2(val: Union[int, str]):
     else:
         reveal_type(val)  # N: Revealed type is "Union[builtins.int, builtins.str]"
 [builtins fixtures/tuple.pyi]
+
+[case testTypeGuardRestrictAwaySingleInvariant]
+from typing import List
+from typing_extensions import TypeGuard
+
+class B: ...
+class C(B): ...
+
+def is_c_list(x: list[B]) -> TypeGuard[list[C]]: ...
+
+def test() -> None:
+    x: List[B]
+    if not is_c_list(x):
+        reveal_type(x)  # N: Revealed type is "builtins.list[__main__.B]"
+        return
+    reveal_type(x)  # N: Revealed type is "builtins.list[__main__.C]"
+[builtins fixtures/tuple.pyi]

From a95bb8eaa8ce80c455491b8f59a11f9df16b8a2f Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Sun, 26 Jan 2025 14:26:13 +0000
Subject: [PATCH 03/10] Fix edge case

---
 mypy/binder.py                      |  3 +++
 test-data/unit/check-narrowing.test | 17 +++++++++++++++++
 2 files changed, 20 insertions(+)

diff --git a/mypy/binder.py b/mypy/binder.py
index d06c52b0c5c4..99725237b24c 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -247,6 +247,9 @@ def update_from_options(self, frames: list[Frame]) -> bool:
                     type = possible_types[0]
                 else:
                     type = make_simplified_union(possible_types)
+                    # Legacy guard for corner case, e.g. when the original type is TypeVarType.
+                    if declaration_type is not None and not is_subtype(type, declaration_type):
+                        type = declaration_type
                     # Try simplifying resulting type for unions involving variadic tuples.
                     # Technically, everything is still valid without this step, but if we do
                     # not do this, this may create long unions after exiting an if check like:
diff --git a/test-data/unit/check-narrowing.test b/test-data/unit/check-narrowing.test
index ec647366e743..d1345d40a426 100644
--- a/test-data/unit/check-narrowing.test
+++ b/test-data/unit/check-narrowing.test
@@ -2416,3 +2416,20 @@ while x is not None and b():
     x = f()
 
 [builtins fixtures/primitives.pyi]
+
+[case testNarrowingTypeVarMultiple]
+from typing import TypeVar
+
+class A: ...
+class B: ...
+
+T = TypeVar("T")
+def foo(x: T) -> T:
+    if isinstance(x, A):
+        pass
+    elif isinstance(x, B):
+        pass
+    else:
+        raise
+    return x
+[builtins fixtures/isinstance.pyi]

From 0c05643b8df85de58478109dc0de123e4005f61d Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Sun, 26 Jan 2025 16:03:34 +0000
Subject: [PATCH 04/10] Limit legacy guard scope

---
 mypy/binder.py                      | 7 +++++--
 test-data/unit/check-narrowing.test | 1 +
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 99725237b24c..3417e3d69533 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -21,6 +21,7 @@
     Type,
     TypeOfAny,
     TypeType,
+    TypeVarType,
     UnionType,
     UnpackType,
     find_unpack_in_list,
@@ -247,8 +248,10 @@ def update_from_options(self, frames: list[Frame]) -> bool:
                     type = possible_types[0]
                 else:
                     type = make_simplified_union(possible_types)
-                    # Legacy guard for corner case, e.g. when the original type is TypeVarType.
-                    if declaration_type is not None and not is_subtype(type, declaration_type):
+                    # Legacy guard for corner case when the original type is TypeVarType.
+                    if isinstance(declaration_type, TypeVarType) and not is_subtype(
+                        type, declaration_type
+                    ):
                         type = declaration_type
                     # Try simplifying resulting type for unions involving variadic tuples.
                     # Technically, everything is still valid without this step, but if we do
diff --git a/test-data/unit/check-narrowing.test b/test-data/unit/check-narrowing.test
index d1345d40a426..feb1c951ad72 100644
--- a/test-data/unit/check-narrowing.test
+++ b/test-data/unit/check-narrowing.test
@@ -2431,5 +2431,6 @@ def foo(x: T) -> T:
         pass
     else:
         raise
+    reveal_type(x)  # N: Revealed type is "T`-1"
     return x
 [builtins fixtures/isinstance.pyi]

From 46b682c2add7c5a9e43c7f854e1ec2837389872e Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Sun, 26 Jan 2025 20:56:14 +0000
Subject: [PATCH 05/10] Remove most of Any special-casing in binder

---
 mypy/binder.py                             | 46 +++-------------------
 mypy/checker.py                            |  7 ++--
 mypyc/test-data/irbuild-any.test           | 10 ++---
 test-data/unit/check-classes.test          |  2 +-
 test-data/unit/check-isinstance.test       |  4 +-
 test-data/unit/check-optional.test         | 20 ++++------
 test-data/unit/check-unions.test           |  3 +-
 test-data/unit/check-unreachable-code.test |  9 +++--
 8 files changed, 31 insertions(+), 70 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 3417e3d69533..8adcc7aced23 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -14,7 +14,6 @@
 from mypy.types import (
     AnyType,
     Instance,
-    NoneType,
     PartialType,
     ProperType,
     TupleType,
@@ -271,7 +270,7 @@ def update_from_options(self, frames: list[Frame]) -> bool:
                         )
                         if simplified == self.declarations[key]:
                             type = simplified
-            if current_value is None or not is_same_type(type, current_value[0]):
+            if current_value is None or not is_same_type(type, current_value.type):
                 self._put(key, type, from_assignment=True)
                 changed = True
 
@@ -313,9 +312,7 @@ def accumulate_type_assignments(self) -> Iterator[Assigns]:
         yield self.type_assignments
         self.type_assignments = old_assignments
 
-    def assign_type(
-        self, expr: Expression, type: Type, declared_type: Type | None, restrict_any: bool = False
-    ) -> None:
+    def assign_type(self, expr: Expression, type: Type, declared_type: Type | None) -> None:
         # We should erase last known value in binder, because if we are using it,
         # it means that the target is not final, and therefore can't hold a literal.
         type = remove_instance_last_known_values(type)
@@ -344,43 +341,12 @@ def assign_type(
             # times?
             return
 
-        p_declared = get_proper_type(declared_type)
-        p_type = get_proper_type(type)
         enclosing_type = get_proper_type(self.most_recent_enclosing_type(expr, type))
-        if isinstance(enclosing_type, AnyType) and not restrict_any:
-            # If x is Any and y is int, after x = y we do not infer that x is int.
-            # This could be changed.
-            # Instead, since we narrowed type from Any in a recent frame (probably an
-            # isinstance check), but now it is reassigned, we broaden back
-            # to Any (which is the most recent enclosing type)
+        if isinstance(enclosing_type, AnyType):
+            # If x is Any and y is int, after x = y we do not infer that x is int,
+            # instead we keep it Any. This behavior is unsafe, but it exists since
+            # long time, so we will keep it until someone complains.
             self.put(expr, enclosing_type)
-        # As a special case, when assigning Any to a variable with a
-        # declared Optional type that has been narrowed to None,
-        # replace all the Nones in the declared Union type with Any.
-        # This overrides the normal behavior of ignoring Any assignments to variables
-        # in order to prevent false positives.
-        # (See discussion in #3526)
-        elif (
-            isinstance(p_type, AnyType)
-            and isinstance(p_declared, UnionType)
-            and any(isinstance(get_proper_type(item), NoneType) for item in p_declared.items)
-            and isinstance(
-                get_proper_type(self.most_recent_enclosing_type(expr, NoneType())), NoneType
-            )
-        ):
-            # Replace any Nones in the union type with Any
-            new_items = [
-                type if isinstance(get_proper_type(item), NoneType) else item
-                for item in p_declared.items
-            ]
-            self.put(expr, UnionType(new_items))
-        elif isinstance(p_type, AnyType) and not (
-            isinstance(p_declared, UnionType)
-            and any(isinstance(get_proper_type(item), AnyType) for item in p_declared.items)
-        ):
-            # Assigning an Any value doesn't affect the type to avoid false negatives, unless
-            # there is an Any item in a declared union type.
-            self.put(expr, declared_type)
         else:
             self.put(expr, type)
 
diff --git a/mypy/checker.py b/mypy/checker.py
index 3734f3170790..4d6f7675452d 100644
--- a/mypy/checker.py
+++ b/mypy/checker.py
@@ -3282,7 +3282,7 @@ def check_assignment(
                 if rvalue_type and infer_lvalue_type and not isinstance(lvalue_type, PartialType):
                     # Don't use type binder for definitions of special forms, like named tuples.
                     if not (isinstance(lvalue, NameExpr) and lvalue.is_special_form):
-                        self.binder.assign_type(lvalue, rvalue_type, lvalue_type, False)
+                        self.binder.assign_type(lvalue, rvalue_type, lvalue_type)
                         if (
                             isinstance(lvalue, NameExpr)
                             and isinstance(lvalue.node, Var)
@@ -4021,7 +4021,7 @@ def check_multi_assignment_from_union(
             if isinstance(expr, StarExpr):
                 expr = expr.expr
 
-            # TODO: See todo in binder.py, ConditionalTypeBinder.assign_type
+            # TODO: See comment in binder.py, ConditionalTypeBinder.assign_type
             # It's unclear why the 'declared_type' param is sometimes 'None'
             clean_items: list[tuple[Type, Type]] = []
             for type, declared_type in items:
@@ -4033,7 +4033,6 @@ def check_multi_assignment_from_union(
                 expr,
                 make_simplified_union(list(types)),
                 make_simplified_union(list(declared_types)),
-                False,
             )
         for union, lv in zip(union_types, self.flatten_lvalues(lvalues)):
             # Properly store the inferred types.
@@ -5231,7 +5230,7 @@ def visit_del_stmt(self, s: DelStmt) -> None:
             for elt in flatten(s.expr):
                 if isinstance(elt, NameExpr):
                     self.binder.assign_type(
-                        elt, DeletedType(source=elt.name), get_declaration(elt), False
+                        elt, DeletedType(source=elt.name), get_declaration(elt)
                     )
 
     def visit_decorator(self, e: Decorator) -> None:
diff --git a/mypyc/test-data/irbuild-any.test b/mypyc/test-data/irbuild-any.test
index 3bfb1587fb3b..74096f39a8c8 100644
--- a/mypyc/test-data/irbuild-any.test
+++ b/mypyc/test-data/irbuild-any.test
@@ -49,8 +49,8 @@ def f(a, n, c):
     r3 :: bool
     r4 :: object
     r5 :: int
-    r6 :: str
-    r7 :: object
+    r6 :: object
+    r7 :: str
     r8 :: i32
     r9 :: bit
 L0:
@@ -62,9 +62,9 @@ L0:
     a = r4
     r5 = unbox(int, a)
     n = r5
-    r6 = 'a'
-    r7 = box(int, n)
-    r8 = PyObject_SetAttr(a, r6, r7)
+    r6 = box(int, n)
+    r7 = 'a'
+    r8 = PyObject_SetAttr(a, r7, r6)
     r9 = r8 >= 0 :: signed
     return 1
 
diff --git a/test-data/unit/check-classes.test b/test-data/unit/check-classes.test
index cf401bc2aece..8a5af4ba1e0f 100644
--- a/test-data/unit/check-classes.test
+++ b/test-data/unit/check-classes.test
@@ -3709,7 +3709,7 @@ def new(uc: Type[U]) -> U:
     if 1:
         u = uc(0)
         u.foo()
-        u = uc('')  # Error
+        uc('')  # Error
         u.foo(0)  # Error
         return uc()
 u = new(User)
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index 2e483bbbfc26..e0106cc9dc38 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -115,8 +115,8 @@ if int():
     x = B()
     x.z
     x = foo()
-    x.z          # E: "A" has no attribute "z"
-    x.y
+    reveal_type(x)  # N: Revealed type is "Any"
+reveal_type(x)  # N: Revealed type is "__main__.A"
 
 [case testSingleMultiAssignment]
 x = 'a'
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index c14b6ae376ae..b3fee542b1ec 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -723,12 +723,10 @@ def f():
 def g(x: Optional[int]) -> int:
     if x is None:
         reveal_type(x)  # N: Revealed type is "None"
-        # As a special case for Unions containing None, during
         x = f()
-        reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
-    reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
+        reveal_type(x)  # N: Revealed type is "Any"
+    reveal_type(x)  # N: Revealed type is "Union[Any, builtins.int]"
     return x
-
 [builtins fixtures/bool.pyi]
 
 [case testOptionalAssignAny2]
@@ -741,12 +739,10 @@ def g(x: Optional[int]) -> int:
         reveal_type(x)  # N: Revealed type is "None"
         x = 1
         reveal_type(x)  # N: Revealed type is "builtins.int"
-        # Since we've assigned to x, the special case None behavior shouldn't happen
         x = f()
-        reveal_type(x)  # N: Revealed type is "Union[builtins.int, None]"
-    reveal_type(x)  # N: Revealed type is "Union[builtins.int, None]"
-    return x  # E: Incompatible return value type (got "Optional[int]", expected "int")
-
+        reveal_type(x)  # N: Revealed type is "Any"
+    reveal_type(x)  # N: Revealed type is "Union[Any, builtins.int]"
+    return x
 [builtins fixtures/bool.pyi]
 
 [case testOptionalAssignAny3]
@@ -758,11 +754,11 @@ def g(x: Optional[int]) -> int:
     if x is not None:
         return x
     reveal_type(x)  # N: Revealed type is "None"
-    if 1:
+    if bool():
         x = f()
-        reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
+        reveal_type(x)  # N: Revealed type is "Any"
         return x
-
+    return x  # E: Incompatible return value type (got "None", expected "int")
 [builtins fixtures/bool.pyi]
 
 [case testStrictOptionalCovarianceCrossModule]
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index 329896f7a1a7..a569522adbb7 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -528,8 +528,7 @@ x: Union[int, str]
 a: Any
 if bool():
     x = a
-    # TODO: Maybe we should infer Any as the type instead.
-    reveal_type(x)  # N: Revealed type is "Union[builtins.int, builtins.str]"
+    reveal_type(x)  # N: Revealed type is "Any"
 reveal_type(x)  # N: Revealed type is "Union[builtins.int, builtins.str]"
 [builtins fixtures/bool.pyi]
 
diff --git a/test-data/unit/check-unreachable-code.test b/test-data/unit/check-unreachable-code.test
index e6818ab5c3c7..81650b350f55 100644
--- a/test-data/unit/check-unreachable-code.test
+++ b/test-data/unit/check-unreachable-code.test
@@ -631,11 +631,12 @@ class Child(Parent):
     def bar(self) -> int:
         if 1:
             self = super(Child, self).something()
-            reveal_type(self)       # N: Revealed type is "__main__.Child"
+            reveal_type(self)       # N: Revealed type is "Any"
+            # TODO: we should probably make this unreachable similar to above.
             if self is None:
-                reveal_type(self)
-                return None
-            reveal_type(self)       # N: Revealed type is "__main__.Child"
+                reveal_type(self)   # N: Revealed type is "Never"
+                return None         # E: Incompatible return value type (got "None", expected "int")
+            reveal_type(self)       # N: Revealed type is "Any"
             return 3
 [builtins fixtures/isinstance.pyi]
 

From 1b5cdebab3f1368d16e33301ab62785535ef45f8 Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Tue, 28 Jan 2025 23:55:19 +0000
Subject: [PATCH 06/10] Try some compromise variant

---
 mypy/binder.py                                | 48 +++++++++++--------
 mypy/fastparse.py                             |  4 +-
 mypyc/test-data/irbuild-any.test              |  9 ----
 test-data/unit/check-dynamic-typing.test      |  6 ++-
 test-data/unit/check-isinstance.test          |  5 +-
 test-data/unit/check-optional.test            | 18 +++----
 .../unit/check-parameter-specification.test   |  5 +-
 test-data/unit/check-redefine.test            |  3 +-
 test-data/unit/check-unions.test              |  2 +-
 test-data/unit/check-unreachable-code.test    |  9 ++--
 10 files changed, 57 insertions(+), 52 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 8adcc7aced23..4a2cec3c461e 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -14,6 +14,7 @@
 from mypy.types import (
     AnyType,
     Instance,
+    NoneType,
     PartialType,
     ProperType,
     TupleType,
@@ -341,12 +342,34 @@ def assign_type(self, expr: Expression, type: Type, declared_type: Type | None)
             # times?
             return
 
-        enclosing_type = get_proper_type(self.most_recent_enclosing_type(expr, type))
-        if isinstance(enclosing_type, AnyType):
-            # If x is Any and y is int, after x = y we do not infer that x is int,
-            # instead we keep it Any. This behavior is unsafe, but it exists since
-            # long time, so we will keep it until someone complains.
-            self.put(expr, enclosing_type)
+        p_declared = get_proper_type(declared_type)
+        p_type = get_proper_type(type)
+        if isinstance(p_type, AnyType):
+            # Any type requires some special casing, for both historical reasons,
+            # and to optimise user experience without sacrificing correctness too much.
+            if isinstance(expr, RefExpr) and isinstance(expr.node, Var) and expr.node.is_inferred:
+                # First case: a local/global variable without explicit annotation,
+                # in this case we just assign Any (essentially following the SSA logic).
+                self.put(expr, type)
+            elif isinstance(p_declared, UnionType) and any(
+                isinstance(get_proper_type(item), NoneType) for item in p_declared.items
+            ):
+                # Second case: explicit optional type, in this case we optimize for a common
+                # pattern when an untyped value used as a fallback replacing None.
+                new_items = [
+                    type if isinstance(get_proper_type(item), NoneType) else item
+                    for item in p_declared.items
+                ]
+                self.put(expr, UnionType(new_items))
+            elif isinstance(p_declared, UnionType) and any(
+                isinstance(get_proper_type(item), AnyType) for item in p_declared.items
+            ):
+                # Third case: a union already containing Any (most likely from an un-imported
+                # name), in this case we allow assigning Any as well.
+                self.put(expr, type)
+            else:
+                # In all other cases we don't narrow to Any to minimize false negatives.
+                self.put(expr, declared_type)
         else:
             self.put(expr, type)
 
@@ -368,19 +391,6 @@ def invalidate_dependencies(self, expr: BindableExpression) -> None:
         for dep in self.dependencies.get(key, set()):
             self._cleanse_key(dep)
 
-    def most_recent_enclosing_type(self, expr: BindableExpression, type: Type) -> Type | None:
-        type = get_proper_type(type)
-        if isinstance(type, AnyType):
-            return get_declaration(expr)
-        key = literal_hash(expr)
-        assert key is not None
-        enclosers = [get_declaration(expr)] + [
-            f.types[key].type
-            for f in self.frames
-            if key in f.types and is_subtype(type, f.types[key][0])
-        ]
-        return enclosers[-1]
-
     def allow_jump(self, index: int) -> None:
         # self.frames and self.options_on_return have different lengths
         # so make sure the index is positive
diff --git a/mypy/fastparse.py b/mypy/fastparse.py
index cd7aab86daa0..f09d72d2762e 100644
--- a/mypy/fastparse.py
+++ b/mypy/fastparse.py
@@ -1106,7 +1106,9 @@ def make_argument(
         if argument_elide_name(arg.arg):
             pos_only = True
 
-        argument = Argument(Var(arg.arg, arg_type), arg_type, self.visit(default), kind, pos_only)
+        var = Var(arg.arg, arg_type)
+        var.is_inferred = False
+        argument = Argument(var, arg_type, self.visit(default), kind, pos_only)
         argument.set_line(
             arg.lineno,
             arg.col_offset,
diff --git a/mypyc/test-data/irbuild-any.test b/mypyc/test-data/irbuild-any.test
index 74096f39a8c8..55783a9a9498 100644
--- a/mypyc/test-data/irbuild-any.test
+++ b/mypyc/test-data/irbuild-any.test
@@ -37,7 +37,6 @@ def f(a: Any, n: int, c: C) -> None:
     c.n = a
     a = n
     n = a
-    a.a = n
 [out]
 def f(a, n, c):
     a :: object
@@ -49,10 +48,6 @@ def f(a, n, c):
     r3 :: bool
     r4 :: object
     r5 :: int
-    r6 :: object
-    r7 :: str
-    r8 :: i32
-    r9 :: bit
 L0:
     r0 = box(int, n)
     c.a = r0; r1 = is_error
@@ -62,10 +57,6 @@ L0:
     a = r4
     r5 = unbox(int, a)
     n = r5
-    r6 = box(int, n)
-    r7 = 'a'
-    r8 = PyObject_SetAttr(a, r7, r6)
-    r9 = r8 >= 0 :: signed
     return 1
 
 [case testCoerceAnyInOps]
diff --git a/test-data/unit/check-dynamic-typing.test b/test-data/unit/check-dynamic-typing.test
index 21fd52169ff5..59d0516eae27 100644
--- a/test-data/unit/check-dynamic-typing.test
+++ b/test-data/unit/check-dynamic-typing.test
@@ -320,8 +320,10 @@ d = None # All ok
 d = t
 d = g
 d = A
-t = d
-f = d
+
+d1: Any
+t = d1
+f = d1
 [builtins fixtures/tuple.pyi]
 
 
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index e0106cc9dc38..a1610582901f 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -1919,13 +1919,12 @@ if isinstance(x, str, 1): # E: Too many arguments for "isinstance"
 from typing import Any
 
 def narrow_any_to_str_then_reassign_to_int() -> None:
-    v = 1 # type: Any
+    v: Any = 1
 
     if isinstance(v, str):
         reveal_type(v)  # N: Revealed type is "builtins.str"
         v = 2
-        reveal_type(v)  # N: Revealed type is "Any"
-
+        reveal_type(v)  # N: Revealed type is "builtins.int"
 [builtins fixtures/isinstance.pyi]
 
 [case testNarrowTypeAfterInList]
diff --git a/test-data/unit/check-optional.test b/test-data/unit/check-optional.test
index b3fee542b1ec..a4337ecd73c9 100644
--- a/test-data/unit/check-optional.test
+++ b/test-data/unit/check-optional.test
@@ -723,9 +723,10 @@ def f():
 def g(x: Optional[int]) -> int:
     if x is None:
         reveal_type(x)  # N: Revealed type is "None"
+        # As a special case for Unions containing None, during
         x = f()
-        reveal_type(x)  # N: Revealed type is "Any"
-    reveal_type(x)  # N: Revealed type is "Union[Any, builtins.int]"
+        reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
+    reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
     return x
 [builtins fixtures/bool.pyi]
 
@@ -739,9 +740,10 @@ def g(x: Optional[int]) -> int:
         reveal_type(x)  # N: Revealed type is "None"
         x = 1
         reveal_type(x)  # N: Revealed type is "builtins.int"
+        # Same as above, even after we've assigned to x
         x = f()
-        reveal_type(x)  # N: Revealed type is "Any"
-    reveal_type(x)  # N: Revealed type is "Union[Any, builtins.int]"
+        reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
+    reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
     return x
 [builtins fixtures/bool.pyi]
 
@@ -754,11 +756,9 @@ def g(x: Optional[int]) -> int:
     if x is not None:
         return x
     reveal_type(x)  # N: Revealed type is "None"
-    if bool():
-        x = f()
-        reveal_type(x)  # N: Revealed type is "Any"
-        return x
-    return x  # E: Incompatible return value type (got "None", expected "int")
+    x = f()
+    reveal_type(x)  # N: Revealed type is "Union[builtins.int, Any]"
+    return x
 [builtins fixtures/bool.pyi]
 
 [case testStrictOptionalCovarianceCrossModule]
diff --git a/test-data/unit/check-parameter-specification.test b/test-data/unit/check-parameter-specification.test
index fa3d98036ec3..e6e943573bda 100644
--- a/test-data/unit/check-parameter-specification.test
+++ b/test-data/unit/check-parameter-specification.test
@@ -343,8 +343,9 @@ class C(Generic[P]):
         a = kwargs
         args = kwargs  # E: Incompatible types in assignment (expression has type "P.kwargs", variable has type "P.args")
         kwargs = args  # E: Incompatible types in assignment (expression has type "P.args", variable has type "P.kwargs")
-        args = a
-        kwargs = a
+        a1: Any
+        args = a1
+        kwargs = a1
 [builtins fixtures/dict.pyi]
 
 [case testParamSpecSubtypeChecking2]
diff --git a/test-data/unit/check-redefine.test b/test-data/unit/check-redefine.test
index e162bb73a206..9a0b9de14c2e 100644
--- a/test-data/unit/check-redefine.test
+++ b/test-data/unit/check-redefine.test
@@ -193,7 +193,8 @@ def f() -> None:
     _, _ = 1, ''
     if 1:
         _, _ = '', 1
-        reveal_type(_) # N: Revealed type is "Any"
+        # This is unintentional but probably fine. No one is going to read _ value.
+        reveal_type(_) # N: Revealed type is "builtins.int"
 
 [case testRedefineWithBreakAndContinue]
 # flags: --allow-redefinition
diff --git a/test-data/unit/check-unions.test b/test-data/unit/check-unions.test
index a569522adbb7..29866796c095 100644
--- a/test-data/unit/check-unions.test
+++ b/test-data/unit/check-unions.test
@@ -528,7 +528,7 @@ x: Union[int, str]
 a: Any
 if bool():
     x = a
-    reveal_type(x)  # N: Revealed type is "Any"
+    reveal_type(x)  # N: Revealed type is "Union[builtins.int, builtins.str]"
 reveal_type(x)  # N: Revealed type is "Union[builtins.int, builtins.str]"
 [builtins fixtures/bool.pyi]
 
diff --git a/test-data/unit/check-unreachable-code.test b/test-data/unit/check-unreachable-code.test
index 81650b350f55..e6818ab5c3c7 100644
--- a/test-data/unit/check-unreachable-code.test
+++ b/test-data/unit/check-unreachable-code.test
@@ -631,12 +631,11 @@ class Child(Parent):
     def bar(self) -> int:
         if 1:
             self = super(Child, self).something()
-            reveal_type(self)       # N: Revealed type is "Any"
-            # TODO: we should probably make this unreachable similar to above.
+            reveal_type(self)       # N: Revealed type is "__main__.Child"
             if self is None:
-                reveal_type(self)   # N: Revealed type is "Never"
-                return None         # E: Incompatible return value type (got "None", expected "int")
-            reveal_type(self)       # N: Revealed type is "Any"
+                reveal_type(self)
+                return None
+            reveal_type(self)       # N: Revealed type is "__main__.Child"
             return 3
 [builtins fixtures/isinstance.pyi]
 

From efaaa90e8cc8e1b3506f161a57ab71c5a2e740c4 Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Wed, 29 Jan 2025 00:29:56 +0000
Subject: [PATCH 07/10] Update test

---
 test-data/unit/typexport-basic.test | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-data/unit/typexport-basic.test b/test-data/unit/typexport-basic.test
index d78cf0f179f2..4e7df25515f0 100644
--- a/test-data/unit/typexport-basic.test
+++ b/test-data/unit/typexport-basic.test
@@ -238,7 +238,7 @@ NameExpr(4) : Any
 NameExpr(5) : A
 NameExpr(5) : Any
 NameExpr(6) : A
-NameExpr(6) : Any
+NameExpr(6) : A
 
 [case testMemberAssignment]
 from typing import Any

From be952b94dbd80deeadac88bbb7b99267e568dbfe Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Fri, 31 Jan 2025 20:34:54 +0000
Subject: [PATCH 08/10] Try respecting explicit Any annotation

---
 mypy/binder.py                           |  7 +++++++
 test-data/unit/check-dynamic-typing.test |  2 +-
 test-data/unit/check-isinstance.test     | 14 +++++++++++++-
 3 files changed, 21 insertions(+), 2 deletions(-)

diff --git a/mypy/binder.py b/mypy/binder.py
index 4a2cec3c461e..4a9b5208336f 100644
--- a/mypy/binder.py
+++ b/mypy/binder.py
@@ -370,6 +370,13 @@ def assign_type(self, expr: Expression, type: Type, declared_type: Type | None)
             else:
                 # In all other cases we don't narrow to Any to minimize false negatives.
                 self.put(expr, declared_type)
+        elif isinstance(p_declared, AnyType):
+            # Mirroring the first case above, we don't narrow to a precise type if the variable
+            # has an explicit `Any` type annotation.
+            if isinstance(expr, RefExpr) and isinstance(expr.node, Var) and expr.node.is_inferred:
+                self.put(expr, type)
+            else:
+                self.put(expr, declared_type)
         else:
             self.put(expr, type)
 
diff --git a/test-data/unit/check-dynamic-typing.test b/test-data/unit/check-dynamic-typing.test
index 59d0516eae27..ffab5afeda3e 100644
--- a/test-data/unit/check-dynamic-typing.test
+++ b/test-data/unit/check-dynamic-typing.test
@@ -252,7 +252,7 @@ if int():
 if int():
     a = d.foo(a, a)
 d.x = a
-d.x.y.z  # E: "A" has no attribute "y"
+d.x.y.z
 
 class A: pass
 [out]
diff --git a/test-data/unit/check-isinstance.test b/test-data/unit/check-isinstance.test
index a1610582901f..331ac8bc95ad 100644
--- a/test-data/unit/check-isinstance.test
+++ b/test-data/unit/check-isinstance.test
@@ -1915,12 +1915,24 @@ if isinstance(x, str, 1): # E: Too many arguments for "isinstance"
     reveal_type(x) # N: Revealed type is "builtins.int"
 [builtins fixtures/isinstancelist.pyi]
 
-[case testIsinstanceNarrowAny]
+[case testIsinstanceNarrowAnyExplicit]
 from typing import Any
 
 def narrow_any_to_str_then_reassign_to_int() -> None:
     v: Any = 1
 
+    if isinstance(v, str):
+        reveal_type(v)  # N: Revealed type is "builtins.str"
+        v = 2
+        reveal_type(v)  # N: Revealed type is "Any"
+[builtins fixtures/isinstance.pyi]
+
+[case testIsinstanceNarrowAnyImplicit]
+def foo(): ...
+
+def narrow_any_to_str_then_reassign_to_int() -> None:
+    v = foo()
+
     if isinstance(v, str):
         reveal_type(v)  # N: Revealed type is "builtins.str"
         v = 2

From cde9dc132ec8d7ba519a014b47cb482ff0e1bf1c Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Fri, 31 Jan 2025 20:46:55 +0000
Subject: [PATCH 09/10] Update assignment

---
 test-data/unit/typexport-basic.test | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-data/unit/typexport-basic.test b/test-data/unit/typexport-basic.test
index 4e7df25515f0..e3fed4606749 100644
--- a/test-data/unit/typexport-basic.test
+++ b/test-data/unit/typexport-basic.test
@@ -255,7 +255,7 @@ NameExpr(6) : A
 NameExpr(6) : A
 MemberExpr(7) : A
 MemberExpr(7) : A
-MemberExpr(7) : A
+MemberExpr(7) : Any
 NameExpr(7) : A
 NameExpr(7) : A
 

From 57d065d04ecac88b421e5156141753767804ad3c Mon Sep 17 00:00:00 2001
From: Ivan Levkivskyi <levkivskyi@gmail.com>
Date: Fri, 31 Jan 2025 23:12:14 +0000
Subject: [PATCH 10/10] Update another test

---
 test-data/unit/typexport-basic.test | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/test-data/unit/typexport-basic.test b/test-data/unit/typexport-basic.test
index e3fed4606749..512b572801d2 100644
--- a/test-data/unit/typexport-basic.test
+++ b/test-data/unit/typexport-basic.test
@@ -238,7 +238,7 @@ NameExpr(4) : Any
 NameExpr(5) : A
 NameExpr(5) : Any
 NameExpr(6) : A
-NameExpr(6) : A
+NameExpr(6) : Any
 
 [case testMemberAssignment]
 from typing import Any