That is true in general, yes. This is also true of Python, but a program which is just `print("hi!")` can be statically proven to halt. I suspect this is true

That is true in general, yes. This is also true of Python, but a program which is just `print("hi!")` can be statically proven to halt. I suspect this is true of a very great majority of type hints in Python which actually exist.