Type inference problem in generic function

[JukkaL]

Mypy complains about the following code:

from typing import TypeVar, List
T = TypeVar('T')
def f(a: T) -> None:
    l = []  # type: List[T]   # Error, even though this should be fine

The reason for the error seems to be that the type variable type T in List[T] is erased so that it won't conflict with the type variables used for inferring the type of the list expression. Both type variables should be able to coexist during type inference.

[rwbarton]

I took a quick look at this bug first because it seems pretty fundamental to some of the inference problems involving type variables. Indeed as Jukka says the problem is that function type variables get "erased" from the type of the context when checking a call to a generic callable, making them not valid solutions for the type arguments of that call.

The reason is that in a nested call like

def mklist(x: T) -> List[T]: ...
def mkset(x: List[T]) -> Set[T]: ...
b = False
s = mkset(mklist(b))

we first try to figure out what type mkset is being called at, by determining the type of its arguments; calling that type to be determined T1, we next need to determine what type mklist is being called at. Based on the fact that the return type of mklist needs to be List[T1], we would conclude that mklist is called at type T1. But its argument has type bool, and we don't know that that is the same as T1, causing an error.

By erasing the type variable T1 from the context when type checking mklist(b), we prevent solving for the type variable of mklist based on the return type, so instead it gets solved based on the argument type bool. Then when finishing the type checking of mkset(...), we know the argument has type List[Bool] so T1 must be Bool. This approach seems like a bit of a hack, but I guess it works well for now. (The alternative is for type checking of mklist(b): List[T1] to be able to return a result like "yes, provided T1 = Bool" and then take this into account when inferring the type variables of mkset.)

Turning to the program in this ticket, the problem is that we also erase the type T from the context of [], because we currently have no way to distinguish type variables bound by a surrounding function definition from type variables that we are solving for in a surrounding function call. In general we might even be typechecking inside a function call that is a call to a surrounding function definition, for example in a generic function f that calls itself recursively. So at a minimum, we need to do some kind of relabeling of the type variables of the call to f to distinguish them from the type variables bound by the definition of f. This would still be true even if we implemented #1261, or replaced the context type variable erasure with an approach based on returning constraints from type checking.

This ought to be enough for now since when relabeling type variables of a generic call, we can mark them as "erasable", and erase only those type variables in context type variable erasure. But since this isn't trivial to do, I'm going to investigate some related bugs before deciding whether to go down that path.