I have it for Common Lisp in emacs for example(it requires running a live repl and having the editor connect to it).
Pre compilation errors are harder, and I personally don't feel safe refactoring in any language unless there are good automated tests. Static typing makes it better, but nowhere near full proof.
With polymorphism and inheritance in the mainstream languages, the method signature still doesn't exactly tell you what you are going to get, so you have all of the pain of micromanaging type annotations and you still don't really get an invariant.
Also, Python has function annotations if your purpose is to document the signature without using docstrings. I'm unsure why you don't mention these because they are exactly analogous to what you say is straightforward.
Interfaces will without a doubt tell you what you can do with a given object. With polymorphism you most assuredly know what types the arguments are inside each signature you write.
Function annotations look like shit[0] and are not guaranteed to mean the same thing across projects.
Don't get me wrong, I love Python and its idioms and have been using it for a rather long time. It pays the bills and I am productive in it. I just think that I've outgrown its implicit typing when I step into an explicitly typed language using modern tools and enjoy myself.
This is exactly what is addressed by the Liskov substitution principle [0] -- the "L" in SOLID [1]. If your subtype does not have the same semantics as the type it extends, then it fails this criteria. It is violating the (implicit) contract of the type it is extending.
[0] https://en.wikipedia.org/wiki/Liskov_substitution_principle
[1] https://en.wikipedia.org/wiki/SOLID_%28object-oriented_desig...