Some types are not (and cannot) be enforced at compile time [0]. In fact what makes something a type is not something internal to the type, but its participation in a larger type system or type theory, so in that sense, almost any abstract model of computation could give rise to types, as long as it was sound.
In a dependently typed language, types may rely upon arbitrary terms that are computed at runtime, and yet you are correct that dependently typed programs are checked statically. The way this is achieved is if a property can only be checked at runtime, then the burden of proof for that property is moved from the typechecker to the program.
The program must verify the property at runtime and create a witness to the proof, which it can then pass to functions to say that it has done the necessary work.
So I guess the answer is yes and no. I would say the whole point of dependently-typed languages is that we can statically determine that somebody is maintaining correctness, be it at compile time or at run time.
