> There are languages with dependent typing, but of them I only know Coq, and Coq sidesteps the issue by the language not being Turing Complete.

There's also Idris, which I haven't really used, but from what I understand, it's sort of like Haskell with dependent types.

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