False unbound-name after a nested exhaustive match whose arms all raise/return #5069

Describe the Bug

I'd like to work on this. #claim

An exhaustive match whose every arm returns or raises is not treated as terminating the enclosing branch. When control flow merges afterwards, a variable bound in the sibling branch is reported as may be uninitialized [unbound-name].

The flat case (the match is the last statement of the function) is handled correctly, so this seems to be specific to the definite-assignment analysis at a flow merge.

Repro

class A: ...

def f(flag: bool, x: A) -> int:
    if flag:
        y = 1
    else:
        match x:
            case A():
                raise ValueError("x")
    return y   # ERROR `y` may be uninitialized [unbound-name]

The same happens when the outer construct is a match arm instead of if/else. This is how we hit it in practice, with a Result-style union:

from dataclasses import dataclass
from typing import final

@final
@dataclass
class Ok[T]:
    value: T

@final
@dataclass
class Err[E]:
    error: E

class NotFoundError(Exception): ...

def get() -> Ok[int] | Err[NotFoundError]: ...

def g() -> int:
    match get():
        case Ok(value):
            pass
        case Err(err):
            match err:
                case NotFoundError():
                    raise ValueError("should not happen")
    return value   # ERROR `value` may be uninitialized [unbound-name]

Sandbox: repro 1 · repro 2

Actual Behavior

ERROR `y` may be uninitialized [unbound-name]
ERROR `value` may be uninitialized [unbound-name]

Reproduces on pyrefly 1.3.2 and 1.4.0-dev.2.

Expected Behavior

No error. In both examples the else branch / Err arm cannot fall through, so y / value is always bound at the return.

What works (for comparison)

Related symptom: no unreachable warning after an exhaustive match

The same construct is also invisible to the unreachable check. With unreachable enabled (--min-severity=warn), only the statement after a plain raise is reported; statements after an exhaustive match whose arms all raise are not, even in the flat case:

def flat(r: Ok[int] | Err[NotFoundError]) -> None:
    match r:
        case Ok():
            raise ValueError()
        case Err():
            raise ValueError()
    print("not reported")          # expected: This code is unreachable [unreachable]

def nested() -> None:
    match get():
        case Ok(value):
            pass
        case Err(err):
            match err:
                case NotFoundError():
                    raise ValueError()
            print("not reported")  # expected: This code is unreachable [unreachable]

def plain() -> None:
    raise ValueError()
    print("reported")              # WARN This code is unreachable [unreachable]

Sandbox: repro 3 (only the last print gets the warning)

So the unreachable check appears to consider only syntactic terminators, not match exhaustiveness. Mentioning it here since it is likely the same underlying gap; happy to split it out if you'd rather track it separately.

Possibly related

#5011 reports that narrowing is not preserved after a nested exhaustive match — likely the same underlying cause (the nested match is not recognised as terminating), but with a different symptom (narrowing vs. definite assignment) and only if as the outer construct with literal patterns. Filing separately in case the code paths differ.

Possibly relevant: unbound-name detection happens during binding (per #4887), whereas match exhaustiveness is only known at solve time, which would explain why the last-statement case works but the merge case doesn't.

Sandbox Link

https://pyrefly.org/sandbox/?project=v2.pZQxD4IwEIX_ykUGGJTGlY3BWcPgIiYUqECC1AgY6q_3tahAVBY7NU3v2rz33fsVmf2o-B65rvsG0zmVHDjHmNsldR75xl-IPjBobgyIKHx6_RWeM2-SHE2GE72QbYJ8Z4zhlLa9ptHg5oSLLlzA6RGrCluLNkGwDShSER5RFAuC5hCn4GVxFykd2iqWbZWuNG7HTxst2vUH9FQEAQb_sxYxCV8hh4WEFJQ3zaX2GHuVy2vGRMVSmdRsUsFIE8tvvDDhO21H0mBXo-0__Ng9PvYcPbaGBzdmgXgA

(Only applicable for extension issues) IDE Information

No response