[ty] loop control flow analysis using loop header definitions

crates/ty_python_semantic/resources/mdtest/loops/for.md

@@ -1051,3 +1051,276 @@ def _(value: list[Not[str]]):
     for x in value:
         reveal_type(x)  # revealed: ~str
 ```
+
+## Walrus definitions in the iterator expression are always evaluated
+
+```py
+for _ in (x := range(0)):
+    pass
+reveal_type(x)  # revealed: range
+```
+
+## Cyclic control flow
+
+### Basic
+
+```py
+i = 0
+reveal_type(i)  # revealed: Literal[0]
+for _ in range(1_000_000):
+    i += 1
+    reveal_type(i)  # revealed: int
+reveal_type(i)  # revealed: int
+```
+
+### A binding that didn't exist before the loop started
+
+```py
+i = 0
+for _ in range(1_000_000):
+    if i > 0:
+        loop_only += 1  # error: [possibly-unresolved-reference]
+    if i == 0:
+        loop_only = 0
+    i += 1
+# error: [possibly-unresolved-reference]
+reveal_type(loop_only)  # revealed: int
+```
+
+### Nested loops with `break` and `continue`
+
+```py
+def random() -> bool:
+    return False
+
+x = "A"
+for _ in range(1_000_000):
+    reveal_type(x)  # revealed: Literal["A", "D"]
+    for _ in range(1_000_000):
+        # The "C" binding isn't visible here. It breaks this inner loop, and it always gets
+        # overwritten before the end of the outer loop.
+        reveal_type(x)  # revealed: Literal["A", "D", "B"]
+        if random():
+            x = "B"
+            continue
+        else:
+            x = "C"
+            break
+        reveal_type(x)  # revealed: Never
+    # We don't know whether a `for` loop will execute its body at all, so "A" is still visible here.
+    # Similarly, we don't know when the loop will terminate, so "B" is also visible here despite the
+    # `continue` above.
+    reveal_type(x)  # revealed: Literal["A", "D", "B", "C"]
+    if random():
+        x = "D"
+        continue
+    else:
+        x = "E"
+        break
+    reveal_type(x)  # revealed: Never
+reveal_type(x)  # revealed: Literal["A", "D", "E"]
+```
+
+### Walrus operator assignments are visible via loopback
+
+```py
+for _ in range(1_000_000):
+    # error: [possibly-unresolved-reference]
+    reveal_type(y)  # revealed: Literal[1]
+    x = (y := 1)
+```
+
+### Loopback bindings are not visible to the walrus operator in iterable expression
+
+The iterable is only evaluated once, before the loop body runs.
+
+```py
+x = "hello"
+for _ in (y := x):
+    # This assignment is not visible when the iterable `x` is used above.
+    x = None
+reveal_type(y)  # revealed: Literal["hello"]
+```
+
+### "Member" (as opposed to "symbol") places are also given loopback bindings
+
+```py
+my_dict = {}
+my_dict["x"] = 0
+reveal_type(my_dict["x"])  # revealed: Literal[0]
+for _ in range(1_000_000):
+    my_dict["x"] += 1
+reveal_type(my_dict["x"])  # revealed: int
+```
+
+### `del` prevents bindings from reaching the loopback
+
+This `x` cannot reach the use at the top of the loop:
+
+```py
+for _ in range(1_000_000):
+    x  # error: [unresolved-reference]
+    x = 42
+    del x
+```
+
+On the other hand, if `x` is defined before the loop, the `del` makes it a
+`[possibly-unresolved-reference]`:
+
+```py
+x = 0
+for _ in range(1_000_000):
+    x  # error: [possibly-unresolved-reference]
+    x = 42
+    del x
+```
+
+### `del` in a loop makes a variable possibly-unbound after the loop
+
+```py
+x = 0
+for _ in range(1_000_000):
+    # error: [possibly-unresolved-reference]
+    del x
+# error: [possibly-unresolved-reference]
+x
+```
+
+### Bindings in a loop are possibly-unbound after the loop
+
+```py
+for _ in range(1_000_000):
+    x = 42
+# error: [possibly-unresolved-reference]
+x
+```
+
+### Swap bindings converge normally under fixpoint iteration
+
+```py
+x = 1
+y = 2
+for _ in range(1_000_000):
+    x, y = y, x
+    # Note that we get correct types in the "avoid oscillations" test case below, but not here. I
+    # believe the difference is that in this case the Salsa "cycle head" is the tuple on the RHS of
+    # the assignment, which triggers our recursive type handling, whereas below it's `x`.
+    # TODO: should be Literal[2, 1]
+    reveal_type(x)  # revealed: Divergent
+    # TODO: should be Literal[1, 2]
+    reveal_type(y)  # revealed: Divergent
+```
+
+### Tuple assignments are inferred correctly
+
+```py
+x = 0
+for _ in range(1_000_000):
+    x, y = x + 1, None
+    # TODO: should be int
+    reveal_type(x)  # revealed: Divergent
+```
+
+### Avoid oscillations
+
+We need to avoid oscillating cycles in cases like the following, where the type of one of these loop
+variables also influences the static reachability of its bindings. This case was minimized from a
+real crash that came up during development checking these lines of `sympy`:
+<https://github.com/sympy/sympy/blob/c2bfd65accf956576b58f0ae57bf5821a0c4ff49/sympy/core/numbers.py#L158-L166>
+
+```py
+x = 1
+y = 2
+for _ in range(1_000_000):
+    if x:
+        x, y = y, x
+    reveal_type(x)  # revealed: Literal[2, 1]
+    reveal_type(y)  # revealed: Literal[1, 2]
+```
+
+### Bindings in statically unreachable branches are excluded from loopback
+
+```py
+VAL = 1
+
+x = 1
+for _ in range(1_000_000):
+    reveal_type(x)  # revealed: Literal[1]
+    if VAL - 1:
+        x = 2
+```
+
+### `Divergent` in narrowing conditions doesn't run afoul of "monotonic widening" in cycle recovery
+
+This test looks for a complicated inference failure case that came up during implementation. See the
+`while` variant of this case in `while_loop.md` for a detailed description.
+
+```py
+class Node:
+    def __init__(self, next: "Node | None" = None):
+        self.next: "Node | None" = next
+
+node = Node(Node(Node()))
+for _ in range(1_000_000):
+    if node.next is None:
+        break
+    node = node.next
+reveal_type(node)  # revealed: Node
+reveal_type(node.next)  # revealed: Node | None
+```
+
+### `global` and `nonlocal` keywords in a loop
+
+We need to make sure that the loop header definition doesn't count as a "use" prior to the
+`global`/`nonlocal` declaration, or else we'll emit a false-positive semantic syntax error.
+
+```py
+x = 0
+
+def _():
+    y = 0
+    def _():
+        for _ in range(1_000_000):
+            global x
+            nonlocal y
+            x = 42
+            y = 99
+```
+
+On the other hand, we don't want to shadow true positives:
+
+```py
+x = 0
+
+def _():
+    y = 0
+    def _():
+        x = 1
+        y = 1
+        for _ in range(1_000_000):
+            global x  # error: [invalid-syntax] "name `x` is used prior to global declaration"
+            nonlocal y  # error: [invalid-syntax] "name `y` is used prior to nonlocal declaration"
+```
+
+### Loop header definitions don't shadow member bindings
+
+```py
+class C:
+    x = None
+
+c = C()
+c.x = 0
+
+for _ in range(1):
+    reveal_type(c.x)  # revealed: Literal[0]
+    c = C()
+    break
+
+d = [0]
+d[0] = 1
+
+for _ in range(1):
+    reveal_type(d[0])  # revealed: Literal[1]
+    d = []
+    break
+```