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 uph

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).