[feature request] Possible type constraints within if-blocks

[a-recknagel]

Given the following code

from typing import Dict, List, Union

mapping: Dict[str, str] = {'a': 'a', 'b': 'b', 'c': 'c'}
vals: List[Union[str, int]] = ['a', 1, 'b', 2]
for val in vals:
    if val in mapping:
        print(mapping[val])

I get error: Invalid index type "Union[str, int]" for "Dict[str, str]"; expected type "str" for the print statement (mypy 0.761, python 3.8.0), even though it seems safe to assert within the scope of the if-block that the type of val can only be the intersection of val's type and mapping's keys type.

Is this possible to implement? Are there pitfalls to this pattern that I'm not seeing?

[JelleZijlstra]

This is #3229.

[a-recknagel]

thanks!