No, you can have downcasting that is checked for validity at runtime, a la Java (or C++ with RTTI). This is not a failure of type safety, since only valid casts will be performed. It's not vacuous, either - it's not just one big type.

What happens when a cast is invalid?

You have type-safe casts in Haskell, for instance, where the failure is reflected at runtime.

    cast :: (Typeable a, Typeable b) => a -> Maybe b

Those are alright.

In Java, IIRC, the cast fails with a ClassCastException. That seems to me to be "failure is reflected at runtime".

In C++ with RTTI, IIRC it returns null. That's also "failure at runtime" (of a sort), but you have to check it.

RTTI returns nullptr when casting a pointer, but it does throw an exception when casting references. Both of these behaviors are well-defined, although the first is kind of questionable.