Your dichotomy between type systems that are too restrictive and type systems that are too complex only appears because you implicitly require soundness. In Py

Your dichotomy between type systems that are too restrictive and type systems that are too complex only appears because you implicitly require soundness. In Python, all your examples can be typed as "Any" https://docs.python.org/3/library/typing.html#the-any-type https://docs.python.org/3/library/typing.html#the-any-type It's an extremely simple type that never leads to hard-to-understand type errors, because it never produces type errors. And you can use it for any real-world program, including malformed ones. Of course that means the type system is unsound and accepts programs that will fail at runtime. But that is perfectly fine as long as the type checker can spot some issues and gets out of your way otherwise.