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

Start by reproducing examples 1–3 with the reported mypy version and compare lambda inference with and without the Callable annotation. Trace the type-checking path for narrowed variables captured by lambdas; done means late-bound captures do not retain invalid narrowing, while the annotated case behaves consistently without duplicate or contradictory errors.