Incorrect specialisation of inferred lambda types based on early binding assumption (sometimes)

If a lambda is defined in a partially specialised context, its type implicitly captures the specialisation of the context, even though the specialisation may no longer hold at the point it gets executed. This changes unexpectedly if a type hint is given.

For example

def example_1(p1: Optional[int]):
    if p1 is not None:
        late_p1 = (lambda: p1)
        reveal_type(late_p1)

Revealed type is 'def () -> builtins.int'

However, if we give it a type annotation on the assignment line, it complains.

def example_2(p1: Optional[int]):
    if p1 is not None:
        late_p1: Callable[[], int] = (lambda: p1)
        reveal_type(late_p1)

This time it abandons the local context that p1 has been checked against None, and considers that the broadest type of p1 is Optional. And even though that signature is exactly what it otherwise infers, it now raises two errors on the same assignment line:

error: Incompatible types in assignment (expression has type "Callable[[], Optional[int]]", variable has type "Callable[[], int]")
error: Incompatible return value type (got "Optional[int]", expected "int")

The behaviour in example_1 is buggy: because of late binding it is possible for the former behaviour to leak wider types.

def example_3(p1: Optional[int]):
    if p1 is not None:
        late_p1 = (lambda: p1)
    p1 = None
    inc = late_p1() + 1 # This will crash, but MyPy is perfectly confident that `late_p1()` is an integer.

Example_2 considered in isolation exhibits expected behaviour.
It is a bit odd that type a type hint that matches the original inferred type changes and indeed is suddenly incompatible with the inferred type.

Seen on this StackOverflow question: https://stackoverflow.com/q/64203221/1688786

• Mypy version used: mypy 0.790
• Python version used: 3.8.2
• Operating system and version: Windows 10

Iniziate riproducendo gli esempi 1–3 con la versione di mypy indicata e confrontate l’inferenza di lambda con e senza l’annotazione Callable. Tracciate il percorso del controllo dei tipi per le variabili ristrette catturate dalle lambda; il lavoro è completato quando le catture late-bound non mantengono un restringimento non valido e il caso annotato si comporta in modo coerente, senza errori duplicati o contraddittori.