[red-knot] How should we handle unreachable code?

[dcreager]

We can statically determine that code is unreachable, due to terminal statements or statically known branches:

def f():
    x = 1
    return
    reveal_type(x)  # ???

def g():
    x = 1
    if True:
        return
    reveal_type(x)  # ???

We should consider how we want to handle this. I think the uncontroversial part is that we should produce a (possibly optional?) diagnostic about the code being unreachable. But after that, there are several options:

• We could mark all bindings as not visible once we reach a terminal statement. That would produce an unresolved-reference errors. This seems least helpful, since it seems likely that the user either (a) didn't intend for the code to become unreachable or (b) is inserting e.g. early returns as part of a debugging process. In both cases the user expects the supposedly unreachable code to be well-typed, and would want diagnostics about ways that it's not.

• We could consider the bindings visible, but update their inferred type to be Never to signify that those symbols wouldn't have any values in the unreachable code. This is arguably the most accurate interpretation, but doesn't provide much value over the "this code is unreachable" diagnostic.

• We could type-check the unreachable code as if it were reachable. Note that this would only apply to truly unreachable code, but not in something like:

  def h(cond: bool):
      x = 1
      if cond:
          return
      reveal_type(x)  # revealed: Literal[1]

  Here, the return statement isn't always executed, and so the reveal_type is not unreachable, and the obviously correct result is Literal[1].

We should also look into what mypy and pyright do here, to see if there's an obvious community consensus we should follow.

[dcreager]

Per @AlexWaygood: #15676 (comment)

Mypy has terrible UX if it sees a reveal_type in a block of code it considers unreachable: it just doesn't emit any diagnostic for the reveal_type call at all. This has been the source of many bug reports at mypy over the years, because the rule that tells you off for having unreachable code in the first place is disabled by default, even if you opt into mypy's --strict flag. We shouldn't do what mypy does!

[sharkdp]

since it seems likely that the user either (a) didn't intend for the code to become unreachable or (b) is inserting e.g. early returns as part of a debugging process. In both cases the user expects the supposedly unreachable code to be well-typed, and would want diagnostics about ways that it's not.

I think there is also a valid use case (c) where the user intends the code to be unreachable, but only in certain scenarios. This would be the case for sys.version_info/sys.platform checks that would lead to unreachable code if checked on a version/platform that does not meet the criterion:

if sys.version_info >= (3, 11):
    # [code that makes use of symbols only available in 3.11+]

• We could type-check the unreachable code as if it were reachable.

I think this could lead to many false-positives for the scenario (c) above, because we would emit unresolved-reference diagnostics for all 3.11+ symbols, if we check that code with a target version <3.11.

As @AlexWaygood pointed out recently: we shouldn't even treat that use case (c) in the same way that we treat (a) and (b). Of course we would/could still gray-out the code inside that conditional if the target version is <3.11, but emitting a unreachable-code diagnostic for this code section would be rather annoying, I believe.

We can statically determine that code is unreachable, due to terminal statements or statically known branches:

There is also a distinct third option, where we call a function that does not return (has return type Never/NoReturn). Like a function that always raises, goes into an infinite loop or that aborts the process.

See also: this section in the Pyright documentation.

[mitsuhiko]

Personal feedback: my expectation as a user is that the type inference is unchanged because of the presence of a known return. The reason is that for debugging purposes it's very common to introduce a temporary early return that is unconditional.

Now there are subtleties but I think that the right thing to do is to type check it as if it was reachable.

[eltoder]

I think in general, if some code is provably unreachable, this warrants a warning, but should not by itself change types of anything. If the code is unreachable because, for example, you eliminated all alternatives in a union, that should be a warning, plus the union type should decay to Never.

[sharkdp]

Example where this leads to false positive diagnostics:

def f(arg):
    if True:
        return arg
    return arg  # Name `arg` used when not defined

[sharkdp]

Another instance of this that I found highly irritating until I minified it and found that there was an infinite while loop much further down in the function that causes the public symbol to be invisible:

def outer():
    x = 1

    def inner():
        return x  # Name `x` used when not defined

    # imagine many lines of code here

    while True:
        pass

[dcreager]

Another instance of this that I found highly irritating until I minified it and found that there was an infinite while loop much further down in the function that causes the public symbol to be invisible

That example would also be addressed by astral-sh/ty#210, if we choose to consider the public type of x to include all of the definitions in its scope, not just the ones that are still visible at end-of-scope.

[carljm]

my expectation as a user is that the type inference is unchanged because of the presence of a known return

I understand why this could be desirable for simple cases, but I think it's a very hard answer to generalize to all dead code in any consistent way.

Consider this example:

def f(flag: bool):
    x = 1
    if flag:
        x = 2
        return
        reveal_type(x)  # we currently consider `x` to be undefined here
    reveal_type(x)  # Literal[1]

The behavior of the two different reveal_type here are very closely connected in our control-flow model. It's important here that we understand in the final reveal_type that x cannot be Literal[2]. But it's difficult to split this understanding from our (correct!) understanding that, after the "known return" in the branch, x has no visible definitions at the point of the first reveal_type (because this point is not reachable at all.) It is not clear to me yet how to implement "type check unreachable code 'as normal'", even as a special case.

I think in the short term at least, the minimal right answer here is that, if we find a symbol has no visible definitions, we should check if we are in unreachable code, and if so we should not emit an undefined reference diagnostic, we should just silently infer the type as Never instead.