Related to this, Idris has a totality checker. It does not require totality, however.

http://docs.idris-lang.org/en/latest/tutorial/theorems.html#...