Yes, and this is much, much more common than you may think. You can do (Turing-complete!) type-level computation in C++ (see this post by Matt Might for example). Haskell allows type-level partial functions by way of type families, etc., etc.
Of course, the system that fits your description most is probably dependent typing, which unify types and terms, i.e. there is no differentiation between type-level and value-level computation in a dependently-typed language. There are a myriad dependent type systems (Calculus of Constructions, Martin-Lof type theory, Zhaohui Luo's UTT, etc.), and also plenty of dependently-typed programming languages (Coq, Agda, Idris, you name it).
So, I doubt this question is anywhere close to research-level. But the answer to your question is, yes, there are such languages, and a lot, and the theory of such languages is already fairly well-researched.