Support type-narrowing on non-zero length sequences

Feature

In the following example, mypy currently flags the final return statement because it thinks l could be empty, in which case the body of the for-loop would never execute, and therefore d could still be None. However, the preceding if-statement proves that the body of the for-loop will execute at least once, after which d must be int; it would be pretty cool if mypy could detect this and narrow d to int from that point forward.

def fun(d: int | None, l: list[int]) -> int:
    if len(l) == 0:
        return 0

    for x in l:
        d = (d or 0) + x

    # error: Incompatible return value type (got "Optional[int]", expected "int")
    # but actually we could safely narrow d to int
    return d

Reproduce the issue with the provided fun example and mypy, then trace the type-narrowing and control-flow analysis used for the non-empty list check and loop. No repository file or test is named; done means mypy safely accepts the final return and coverage verifies this narrowing without regressing related cases.