Comment by vbrandl

Idris is an other example for a programming language that always terminates. For that matter any total functional programming language does and is therefore turing incomplete.