Noob question: don't dependent typing requires the language to be dynamic? How do you check dependencies in types otherwise (eg. the size of an array)?
If I understand your question, generally the compiler would use a theorem prover / SAT solver to prove that the constraints of the dynamic types were always upheld. If it can't, in some languages this is a compiler error. In others it will introduce runtime checks (but this still doesn't require a fully dynamic language, as such, but it is in a sense partially dynamic).