What would runtime dependent types be? As I understand, they are a tool for statically proving properties of some code. What use are they at runtime? For code

What would runtime dependent types be? As I understand, they are a tool for statically proving properties of some code. What use are they at runtime? For code that came up as a result of the working system? I believe properties of generated programs can also be proven statically. For user-provided code? Why not just run the compiler/interpreter on it?