Fix loop convergence with redefinitions (python#20865)

Currently, we reset the variable type each time we visit the initial
definition (textually first assignment). This can cause problems with
`--allow-redefinition-new`:
* Not all branches will be explored (see added test). This is a
correctness problem.
* Many loops will become runaway (will never converge to a fixed point)
while they actually can converge. Currently this is stopped by manual
cut-off. This is a performance problem.

The only non-trivial part here is handling of this pattern:
```python
for key in ("key_a", "key_b"):
    some_typed_dict[key]
```
It is special-cased in regular mode, and this special-casing used to
work accidentally with redefinition allowed. Now I simply make the same
special-casing apply (since for loops can never be runaway on index).

Author: ilevkivskyi

mypy/checker.py

@@ -4401,8 +4401,23 @@ def check_lvalue(
         index_lvalue = None
         inferred = None
 
-        if self.is_definition(lvalue) and (
-            not isinstance(lvalue, NameExpr) or isinstance(lvalue.node, Var)
+        # When revisiting the initial assignment (for example in a loop),
+        # treat is as regular if redefinitions are allowed.
+        skip_definition = (
+            self.options.allow_redefinition_new
+            and isinstance(lvalue, NameExpr)
+            and isinstance(lvalue.node, Var)
+            and lvalue.node.is_inferred
+            and lvalue.node.type is not None
+            # Indexes in for loops require special handling, we need to reset them to
+            # a literal value on each loop, but binder doesn't work well with literals.
+            and not lvalue.node.is_index_var
+        )
+
+        if (
+            self.is_definition(lvalue)
+            and (not isinstance(lvalue, NameExpr) or isinstance(lvalue.node, Var))
+            and not skip_definition
         ):
             if isinstance(lvalue, NameExpr):
                 assert isinstance(lvalue.node, Var)
@@ -4784,7 +4799,7 @@ def check_simple_assignment(
                     # This additional check is to give an error instead of inferring
                     # a useless type like None | list[Never] in case of "double-partial"
                     # types that are not supported yet, see issue #20257.
-                    or not is_proper_subtype(rvalue_type, inferred.type)
+                    or not is_subtype(rvalue_type, inferred.type)
                 )
             ):
                 self.msg.need_annotation_for_var(inferred, inferred, self.options)
@@ -4807,7 +4822,9 @@ def check_simple_assignment(
                 ):
                     lvalue_type = make_simplified_union([inferred.type, new_inferred])
                     # Widen the type to the union of original and new type.
-                    self.widened_vars.append(inferred.name)
+                    if not inferred.is_index_var:
+                        # Skip index variables as they are reset on each loop.
+                        self.widened_vars.append(inferred.name)
                     self.set_inferred_type(inferred, lvalue, lvalue_type)
                     self.binder.put(lvalue, rvalue_type)
                     # TODO: A bit hacky, maybe add a binder method that does put and

test-data/unit/check-redefine2.test

@@ -1098,6 +1098,33 @@ def func() -> None:
     reveal_type(l) # N: Revealed type is "None | builtins.list[Any]"
 [builtins fixtures/list.pyi]
 
+[case testNewRedefineLoopProgressiveWidening]
+# flags: --allow-redefinition-new --local-partial-types
+def foo() -> None:
+    while int():
+        if int():
+            x = 1
+        elif isinstance(x, list):
+            x = ""
+        elif isinstance(x, str):
+            x = None
+        else:
+            x = [1]
+    reveal_type(x)  # N: Revealed type is "builtins.int | builtins.list[builtins.int] | builtins.str | None"
+[builtins fixtures/isinstancelist.pyi]
+
+[case testNewRedefineAnyOrEmptyUnpackInLoop]
+# flags: --allow-redefinition-new --local-partial-types
+from typing import Any
+
+def foo() -> None:
+    while int():
+        data: Any
+        x, y = data or ([], [])
+        # Requiring an annotation may be better, but we want to preserve old behaviour.
+        reveal_type(x)  # N: Revealed type is "Any | builtins.list[Never]"
+[builtins fixtures/isinstancelist.pyi]
+
 [case testNewRedefineNarrowingSpecialCase]
 # flags: --allow-redefinition-new --local-partial-types --warn-unreachable
 from typing import Any, Union