You might be interested to learn that in languages like Coq with dependent types, the difference between type-level and value-level languages (almost) disappears! Check out the Software Foundations book [1].

[1] https://softwarefoundations.cis.upenn.edu/