Using same-name stubs is counterproductive

[ghost]

• Are you reporting a bug, or opening a feature request?
  A bug / documentation / feature request, pending on what is expected.

• Please insert below the code you are checking with mypy,
  Repo: https://github.com/vylmen/mypy-stubs-issue

• What is the actual behavior/output?
  https://github.com/vylmen/mypy-stubs-issue/blob/master/results.txt

• What is the behavior/output you expect?
  I expect the same errors to show up for coords.py as they do with nostub.py.

• What are the versions of mypy and Python you are using?
  mypy 0.782, python 3.7.7. Did not check master, but will do if authors believe this behavior changed.

• What are the mypy flags you are using? (For example --strict-optional)
  mypy.ini is in repo

So in short, coords.py is not typechecked (reveal_type is not printed for the file) using the definitions of coords.pyi. I don't see this mentioned in the docs and therefore I'm hoping it's a bug, but if this is unimplemented but desired behavior and unlikely to change - then a note in the docs needed.

[JukkaL]

If there is a stub, mypy won't check the file. There is an existing issue about this: #5028. Closing as duplicate.