> If you want that, just enable strict mode for mypy.

But I can't do that if I want to do gradual typing. If I type a function, but the type system cannot figure out what's going to call it, that's when I want it to perform a check: at the boundary.

> I certainly don't want runtime checks for what the type system has already checked for me.

The type system can remove the checks if it can prove that they always pass. My point is that if it cannot prove that they will pass, I want them at runtime.