[red-knot] Rethink public types of symbols in function-like scopes

[dcreager]

#15676 currently has the following mdtest with incorrect results:

def top_level_return(cond1: bool, cond2: bool):
    x = 1

    def g():
        reveal_type(x)  # revealed: Unknown | Literal[1, 2, 3]

    if cond1:
        if cond2:
            x = 2
        else:
            x = 3
    return

def return_from_if(cond1: bool, cond2: bool):
    x = 1

    def g():
        reveal_type(x)  # revealed: Unknown | Literal[1]

    if cond1:
        if cond2:
            x = 2
        else:
            x = 3
        return

def return_from_nested_if(cond1: bool, cond2: bool):
    x = 1

    def g():
        reveal_type(x)  # revealed: Unknown | Literal[1, 3]

    if cond1:
        if cond2:
            x = 2
            return
        else:
            x = 3

We should determine how we want to handle the assignments in this scope.

One possibility (which mimics our current behavior for module-level scopes) would be to reveal Literal[1, 2, 3] for all three. (This would require changes to our terminal statement support: we currently purposefully resolve the x use in the nested function relative to the end of f's scope, but the return statements are preventing some of the bindings from being visible there.)

[carljm]

Just to be clear, the "should reveal" assertions in the example above are based on what we would currently reveal for a similarly-defined symbol in a module level scope, if we don't consider the return statements. That doesn't mean they represent what we should reveal. It's a bit tricky to say what we should reveal, because it all depends on how much analysis we attempt of where the nested scope can possibly be called from. In all three examples above, a sufficiently powerful analysis would be able to declare that g is never called, and doesn't escape from the local scope to be called elsewhere, so we may as well consider the body of g itself to be unreachable code.

Barring any attempt to analyze where the nested scope can be called from, I think the starting point has to be that all definitions are visible, regardless of control flow. (This is effectively modeling that g could be, perhaps transitively, called from anywhere, including e.g. after x = 2 and before return in the third example, meaning even Literal[2] should be considered a possible value. Of course we can see that in fact g can't be called there, but that's starting to "analyze where the nested scope can be called from".)

Also, for symbols in function-like scopes, if we don't see a nested scope with a nonlocal statement for that symbol and assignment to it, we can remove the union with Unknown, because nothing outside the scope can reassign the symbol, even if it is not declared.

All of that is to say: we have a lot of design work to do on types for closed-over variables, and "the status quo before terminal support", as documented in the tests shown above, is not a very good guide to the desired eventual behavior.

[dcreager]

All of that is to say: we have a lot of design work to do on types for closed-over variables, and "the status quo before terminal support", as documented in the tests shown above, is not a very good guide to the desired eventual behavior.

I've updated the issue description to not presume what behavior we'll want to implement.