Ah, I see! That makes a lot of sense, thank you for explaining.

If I understand correctly, that means type-checking python as you described was an open problem before, and this paper effectively proves it will never happen (ideally). They do this by establishing Turing completeness of type-hints, which are the main mechanisms for type-checking.