I'm not sure anyone has developed a language with a great type level language and a worthless value level one. But that said, theorem provers (like Coq) essenti

I'm not sure anyone has developed a language with a great type level language and a worthless value level one. But that said, theorem provers (like Coq) essentially consider value-level computation as vestigial: nobody cares about running Coq programs, just checking them. To encode what you're looking for requires type-level natural numbers and a reasonable notion of type-level equality. These are fairly non-trivial. You can encode this in Haskell, but type leve" equality is a bit hard to work with so you may suffer some pains (I know, I've done it several times!). Agfa and Idris would be where I would look to see this sort of thing materialize.