Totality Checks

[mvcisback]

In a lot of typed languages, the compiler can be told to check if a function is total, handles all cases.

For Example:

def foo(x: Union[int, str]) -> str:
    if isinstance(x, int):
        return "bar"

Is only a partial function. If x is a str, then this function actually returns None.
Thus the output type should really be Union[str, NoneType]

I tested this snippet and mypy doesn't seem to catch this.
I'm not 100% sure, but I think if a function is partial, NoneType is a potential return type.

[mvcisback]

An informal proof might be:

Suppose an input case is not handled, then either

1. There is a type error, because the program is forcing the input down an incompatible code path.
2. The input bypasses all control flow in the function (as in the foo example).

The first case (hopefully) doesn't pass the type checker.
The second case, returns NoneType (because of pythons implicit return None)

[JukkaL]

This is related to #320. As pointed out by Guido, this is somewhat tricky to implement.

[gvanrossum]

Let's call this a duplicate of #320.