The term "dynamically typed" is meaningless in the context of type systems. As you say yourself, a type system proves the absence of certain errors. A "dynamic" type system tells you precisely where and when such an error occurred. As such, these languages are untyped (or uni-typed which is just a more fancy way of saying that they are untyped).
I am aware that some type theorists insist on this distinction and it does have some some merits, but (afaik) type theorists didn't invent the word "type" and "runtime tags" are commonly and widely known as "dynamic types", even if they do work quite differently from static ones, so I always feel that insisting on this distinction is somewhat pedantic.
But yes, arguing about semantics never got anyone anywhere, what I wanted to highlight was that it's not just coincidence that interpreted languages are by and large dynamically typed.
