Redefinition using the same type should not be an error

Possibly related to #10563.

Bug Report

Consider the following:

# a.py

x: int = 5

# b.py

from a import *

x: int = 7 # error: Name "x" already defined (possibly by an import)  [no-redef]

I would not call it an error. Sure, it's already defined, but it was an int originally.

If you do this:

# c.py

from a import *

x: float = 7.5 # error: Name "x" already defined (possibly by an import)  [no-redef]

You get the same error, but in this case, I'd say that's correct, because maybe I didn't realize it was an int.

And this:

# d.py

from a import *

x = 'boo' # error: Incompatible types in assignment (expression has type "str", variable has type "int")  [assignment]

This I also agree with.

Expected Behavior
I would argue that I should not get an error in b.py, whereas the errors in c.py and d.py are correct.

Typehints to me are as much a documentation tool as they are indispensable to finding bugs. Not being able to reiterate that something is an int means that I cannot document it in the code. I believe this is particularly important with star-imports because by just reading the current file, you have no idea what's being imported.

Here's something else to consider:

# a.py

x: float = 3.14

# b.py

from a import *

x = 5 # no error, because 5 is a float.

Do we know that the author new that x is a float and thus 5 is OK, or did they really mean to write x: int = 5? If I were allowed to write x: float = 5, we would have a definitive answer.

• Mypy version used: 1.3.0
• Mypy configuration options from mypy.ini (and other config files): ignore_missing_imports = True
• Python version used: 3.8.10

Start by reproducing the examples in a.py, b.py, c.py, and d.py with the reported mypy configuration and Python version. Compare diagnostics for same-type redefinition, differing annotations, and incompatible assignment. Done means the expected cases are distinguished consistently, with regression coverage for the reported behavior.