That's essentially what dependent typed languages do. But the stuff that happens at type checking level has to be known to terminate, so it isn't Turing complet

That's essentially what dependent typed languages do. But the stuff that happens at type checking level has to be known to terminate, so it isn't Turing complete. Without this restriction, it is possible to prove false things to the compiler by writing code that never returns.