Redefinition without reassignment doesn't check existing value

[Zeckie]

With --allow-redefinition, mypy allows a variable to be redefined, without checking that the existing value is the correct type.

a: str = "foo"
print(a)  # value needs to be used before redefinition
a: int  # but it is really still str
if a > 1:
    ...

https://mypy-play.net/?mypy=latest&python=3.10&flags=allow-redefinition&gist=79d1e9219d66da441050ba730a7c2842

Expected Behaviour

In this example, mypy should detect that a is still a str, and not allow this redefinition.

It could treat the redefinition as though it is a new variable, being assigned the value of the existing one. That would result in an error like:
error: Incompatible types in assignment (expression has type "str", variable has type "int")

Or it could be a new error, like:
error: Redefinition incompatible with existing type (existing type "str", new type "int")

Actual Behaviour

mypy:

Success: no issues found in 1 source file

python:

TypeError: '>' not supported between instances of 'str' and 'int'

[DetachHead]

pretty sure this is the same issue as #686

[KotlinIsland]

also #4019/#686

[Zeckie]

I think this is different enough from those other issues, in that it is not about whether the variable had been assigned before it is redefined.

Rather it is about mypy recognising that when the redefinition statement does not assign a value to the "new" variable (so a statement in the form variable: type rather than one in the form variable: type = expression), the variable's value (and therefore the current type) does not change.

As the redefinition does not change the value, the new type has to be one that includes the (potentially narrowed) existing type of the variable.

Rewriting the original example as though a was 2 separate variables

a_old: str = "foo"
print(a_old)
a_new: int = a_old  # this clearly isn't valid - assigning a string expression to an integer variable
del a_old
if a_new > 1:
    ...

A slightly different case may work at runtime, but I don't think it should be considered valid:

a: int = 1
b = a + 1 # mypy currently does not allow redefinition unless the variable has been used
a: str # I don't consider this to be valid, as a is still an int
a = "foo" # makes this work at runtime
print(a + "bar")

Another example that currently mypy considers to be valid, but I consider to be invalid:

a: object
print(a)
a: int

Though this would be fine:

a: object
assert isinstance(a, int)
a: int

And taking it one step further, mypy currently says this isn't valid, but I think it should be:

def something() -> bool:
    ...

a: object
assert isinstance(a, int)
a: int | str
b = a + 1  # still narrowed to int from the assert (hasn't been reassigned)
if something():
    a="foo"