My first reaction is that this is a type checker bug: the type checker infers a different type for the expression 0 == x than its actual runtime type.
Unfortunately, it’s a difficult bug for type checkers to resolve, since the actual semantics of __eq__ are complex and can’t be fully encoded in the method signature using the current type system. So a fully correct solution likely requires changes to the type system. There’s been a few other recent threads (Encoding mypy's "overlapping types" in the type system, `__hash__`, `__eq__`, and LSP) dealing with similar issues. I don’t have a solution but I think someone needs to look at all the related issues and try to come up with a solid solution.
I don’t think adding a typing-only __req__ method is a good solution; that would create a second complicated way of representing __eq__ semantics that’s different from the runtime semantics. It’s better for the type system to accurately reflect how things work at runtime. Also, the mention of C extensions in the header here seems like a red herring; the same thing can come up with objects implemented in Python.