Track narrowed expressions in type-checker e.g. to support `if a.b is not None`

[plajjan]

We should track a set of narrowed expressions in the type checker to allow for more natural use of e.g. if a.b is not None or isinstance(a.b, int)

This is from #1401 but reshaped here to be more focused (other solutions / partial workarounds are mentioned in #1401).

class Apa(object):
    def __init__(self, b: ?int):
        self.b = b

actor main(env):
    a = Foo(1)
    if a.b is not None:
        sum = 1337 + a.b
        call_some_func(a) # call_some_func() will still see a with an optional b attribute
        print(sum)
    env.exit(0)

This means that in this scope, a.b will have a narrower type. However, when a is passed around, it will still have the optional b. It is only a.b when accessed exactly as a.b that has the narrower type.

[plajjan]

@nordlander can we track a dict key as a narrowed expression?

if isinstance(foo["hello"]):
    blargh = foo["hello"]

[nordlander]

I suppose the question is really whether we can dynamically check if expression foo is an instance of dict[str,...]. If so the answer is no, not in the desired amount of detail.

What we can do is to check if foo is an instance of class dict, by writing isinstance(foo, dict). So the second parameter to built-in construct isinstance must always be a class name, it can't be a full-blown type expression including type parameters. While we do carry around the actual class of every object at run-time (it's just an aspect of the object's method table), we don't (and can't) keep track of their possible type arguments for the simple reason that these aren't necessarily accessible as object attributes. For a generic function object, the argument and return types are only intermittently determined while the function is being invoked. And for a dict object, the key and value types could only be dynamically traced provided the dict is not empty. Etc, etc.

Instead we rely on type inference to validate an expression like foo["hello"], which is only correct if foo can be statically inferred to support the protocol Indexed[str,T] for some T. This doesn't automatically force foo to be a dict, though, so the question isinstance(foo, dict) might actually be valid in some contexts.

That said, we also have a loop-hole in the current type-checker when it comes to isinstance, in the sense that if the static type of foo is object --- a type that doesn't mention the type parameters of its potential subtype dict[K,V] --- we actually have no right to assume any concrete type for K and V after we've concluded that isinstance(foo, dict) is true. All we are really entitled to do in this case is to treat the foo dict in a fully generic way (like computing its length), which works equally well whatever K and V happens to be. But for this to be statically verifiable we need to introduce the concept of existential types to the type system, which I think is better to defer until we're ready to implement fully-fledged pattern matching.

[plajjan]

Sorry, I don't know what happened there, I just seem to have left out parts of the example. Here's a fixed and more complete one:

foo = {
    "hello": "world",
    "answer": 42
}

def function_that_takes_a_str(s: str):
    print(s)

def function_that_takes_an_int(s: int):
    print(s)

actor main(env):
    if isinstance(foo["hello"], str):
        function_that_takes_a_str(foo["hello"])

    if isinstance(foo["foo"], int):
        function_that_takes_an_int(foo["foo"])
    env.exit(0)

so what I mean by tracking the dict key is that we isinstance check the value that the key maps to, not the key itself.

[plajjan]

@nordlander and I spoke about this separately and yes, dict key accesses like that should act the same way, we can narrow it. I suppose it's general, so we can narrow any expression?