del followed by an assignment of an "incompatible" type shouldn't probably raise an error #2806

I'm posting this to here because PEP 482--484 didn't seem to mention either "scope" or del and this is probably an implementation detail.

Consider this example:

x = 1
del x
x = "a"

Mypy 0.470 raises an error for the above code, saying "Incompatible types in assignment (expression has type "str", variable has type "int")". But, shouldn't it be allowed because the xs before and after del are essentially different variables?

Compare it with

x = 1
x = None
x = "a"

which clearly is a type error (and mypy judges as such.)

Allowing the 1st pattern will open up the way to conveniently rewrite legacy codes like

# path: # type str
path = path.split(os.pathsep)
# path: # type List[str]

(taken from shutil.py)

I mean, we will be able to write

path_ = path.split(os.pathsep)
del path
path = path_