Looks like mypy has discovered interfaces. Lovely.
Having had this experience now it’s much easier to appreciate the practical benefits of systems like Rust and Haskell, where the type checker is doing real work.
A Protocol is just the same structural subtyping (duck typing) Python has always preferred.
I use static Python types a lot at the application layer, where things have no need to be particularly extensible and having strict definitions for how things are put together brings clarity. But at lower levels of the system, Python's duck typing really shines because I can solve ten slight variations on the same problem with the same code.
The same could be said of Typescript, or Clojure+spec, or really any other language where dynamic types are given to you for free (unlike, say, reflection in Java) but types can be added wherever you find them useful.