But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "

But "type checking" that's Turing complete is not type checking at all, it's just a phase distinction. It's no different than choosing whether to run code at "compile" vs. "run" time, except that in practice, we don't even want to have fully Turing-complete compile workflows that might, e.g. not terminate. Dependently typed languages implement this phase distinction via program extraction: you "extract" the code to be fed into the "runtime" phase of execution.