programming language with type-level functions
Yes, and this is much, much more common than you may have thought. You can do meaningful (and actually 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.

Of course, the system that fits your description best 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 near 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. For a reference on dependent types, you might want to consult Chapter 2 of Advanced Topics in Types and Programming Languages (ATTAPL), or Software Foundations by Benjamin Pierce et al., and Type-Driven Development with Idris by Edwin Brady if you're more inclined to work with code.