Rescoping of type variables into return types: agreeing on a specification

Some type checkers such as mypy and pyright implement special rules for rescoping type variables into the return type of a function. This allows such an example to typecheck:

from collections.abc import Callable

def make_identity[T]() -> Callable[[T], T]:
    return lambda x: x

f = make_identity()

reveal_type(f)
# mypy 1.11.1 shows:
#    Revealed type is "def [T] (T`2) -> T`2"
# pyright 1.1.375 shows:
#    Type of "f" is "(T@make_identity) -> T@make_identity"

print(f(0), f("abc"))  # f is polymorphic!

Here, type variable T is rescoped to the callable returned by make_identity, allowing make_identity to return a polymorphic function. This behaviour is not currently formalised in the typing spec. Here is how pyright currently documents it:

When a TypeVar or ParamSpec appears within parameter or return type annotations for a function and it is not already bound to an outer scope, it is normally bound to the function. As an exception to this rule, if the TypeVar or ParamSpec appears only within the return type annotation of the function and only within a single Callable in the return type, it is bound to that Callable rather than the function. This allows a function to return a generic Callable.

As mentioned by @erictraut in another thread, this rule is only a best-effort attempt at matching some undocumented behaviour from mypy. The typing spec should decide what the exact rule must be here. My hope is that this post can start a discussion on this topic.


However, such a discussion cannot be limited to simply making a decision about whether or not the rule above should be made official. Indeed, this rule strikes me as oddly specific and more importantly, it does not capture the more general and sometimes inconsistent behaviours that are currently implemented by type checkers. I’ll give two examples below.

First, mypy also implements rescoping for custom callable protocols, but only if they are pure in the sense that no method other than __call__ is specified (see issue). Pyright used not to implement such a generalisation (see issue), although it may have changed in recent versions. More generally, this raises the question: why should this rescoping rule be restricted to pure callables in the first place?

Second, both mypy and pyright seem to be implementing rescoping in cases that go clearly beyond the rule above. For example, both would accept the following example:

from collections.abc import Callable

def apply_twice[T](f: Callable[[T], T]) -> Callable[[T], T]:
    return lambda x: f(f(x))

def identity[T](x: T) -> T:
    return x

f = apply_twice(identity)

reveal_type(f)  # mypy: Revealed type is "def [T] (T`1) -> T`1"

print(f(0), f("abc"))

Here, variable T does not only appear in the return type of apply_twice, but it is rescoped nonetheless. It is unclear how general the implemented rescoping behaviour is though, in both mypy and pyright. For example, updating pyright from version 1.1.369 to 1.1.375 caused a regression in the codebase of a library I am currently developing, due to an apparent restriction of the (undocumented) rescoping behaviour. Here is a minimal replicating example:

from collections.abc import Callable

def compose[P, T](
    p1: Callable[[P, T], str],
    p2: Callable[[P, T], str]
)    -> Callable[[P, T], str]:
    return lambda p, x: p1(p, x) + p2(p, x)

def foo1(p: object, x: object) -> str:
    return str(x)

def foo2[P](p: P, x: Callable[[P], str]) -> str:
    return x(p)

foo = compose(foo1, foo2)
reveal_type(foo)
# pyright 1.1.369 infers:
#    "(P, (P) -> str) -> str",
#    where P is a type variable bound to the callable.
# pyright 1.1.375 and mypy 1.11.1 infer the less general type:
#    "(object, (object) -> str) -> str",
#    causing them to raise a spurious error below:

p = 0
x: Callable[[int], str] = lambda p: str(p)
foo(p, x)  # pyright 1.1.375 and mypy 1.11.1 report a spurious error

Although I would personally advocate for accepting the code above and assigning foo a polymorphic type, I can imagine counterarguments about keeping the solving algorithm simpler and more efficient at the price of artificial restrictions. I would be curious to hear about what other people think the correct behaviour should be here.


Type variable scoping is currently a major gray area of the typing spec. Anecdotally, it’s also been one of my main source of frustration as a mypy and pyright user. I believe there is an opportunity here to make the behavior of type-checkers more general, more consistent and simpler to explain at the same time. I am looking forward to hearing your thoughts on this.

5 Likes