undefined variables do not raise a type error

[LuKuangChen]

What version of Static Python are you using?

6862bbd 2021-10-07

What program did you run?

def f() -> int:
    return a_definitly_undefined_variable

What happened?

The program passes type checks.

What should have happened?

We expected a compile-time error complaining that a_definitly_undefined_variable is undefined. (This is what mypy does.)

[carljm]

Yes, this is a known issue; in general our approach initially has been "opportunistic optimization," meaning we don't try to verify everything and we just fall back to dynamic if we don't understand something. But explicitly adding all imports to the module's symbol table and then being able to error on use of undefined identifiers (in code or in annotations) is something that's been on the roadmap for a while, just haven't done it yet. Thanks for flagging!

[shriram]

Thanks, Carl. I think from a modeling perspective, then, we're going to act like this is going to be done. Otherwise the model becomes a lot harder, and some desired and intended properties may not even be true due to this technicality, but both without offering any real insight. Rather, we'll think of this as a "side condition" that will eventually be patched in the implementation (and for now remains a caveat for the formal model).

[carljm]

I think that makes sense.