You need dependent types in order to do this, which means doing away with Turing-completeness. (Moreover, the principle 'Type is of type Type' as found in Zig comptime leads to type-unsafety. So you need to replace that with some notion of universes.)
Well, you can have dependent types but limit their expressiveness. Rust, for example, has dependent (comptime) types, but they're very extremely limited:
fn foo<const N: usize>() -> [f32; N]
I imagine having arbitrary comptime code, but more limited use of comptime values in type position.
Also, do you know the exact issue with "Type is of type Type"? I know that can lead to _non-termination_, and non-termination completely breaks proof assistants. For example, you can prove `False` with:
fn make_false() -> False { return make_false(); }
But if you're not building a proof assistant, a function like `make_false()` is fine. Does it lead to any additional problems?
You need dependent types in order to do this, which means doing away with Turing-completeness. (Moreover, the principle 'Type is of type Type' as found in Zig comptime leads to type-unsafety. So you need to replace that with some notion of universes.)