I believe dependent typing is what you're after. Have you looked at Idris?

http://www.idris-lang.org/example/