No, I think the idea is that you'd get a runtime exception if the value was outside the range. No need for dependent types. It is no different conceptually from casting, say, a 64-bit integer to a 32-bit integer. If the value is outside the range for a 32-bit integer, then (depending on the language semantics) you either raise a runtime error, or the result is some kind of nonsense value. You do not need to introduce dependent types into your language to enable such casts (as long as you're willing to enforce the relevant checks only at runtime, or forego such checks altogether).