Also, if what you have is just a linter, ie it only reports things it can detect are errors, and doesn’t report when it can’t figure things out, it’s pretty easy to end up with programs that have plenty of annotations but don’t have enough for the linter to actually catch many errors. That’s somewhat unsubstantiated, so take it with a grain of salt, but when the linter is supposed to work when it can’t figure out all the types it necessarily admits the possibility that it will run without figuring out almost any of them. To some extent, the whole point of a type system is that it covers the whole program, as that’s really the only way you can start counting on it to catch certain types of errors (which, really, is the whole point - it eliminates them from the list of things that programmers have to worry about).
Which isn’t to say doing this is a bad idea, just that the end result is probably going to be a much worse typed language than modern ones (F#, OCaml, Haskell, Rust, Scala…), and this isn’t really a best-of-both-worlds solution. And for places where performance isn’t critical (which, if you’re using Python or Ruby, it probably isn’t), it’s not clear to me that this is going to produce all that much better results than runtime type assertions (ie, contracts).