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?