[Dylan16807]

> SFINAE, accidentally turing-complete templates

Template meta-programming is awful but that particular type of turing completeness isn't a problem at all. Mere arithmetic and some kind of ability to loop gives you that kind of turing completeness. The typical compiler limits looping depth to a couple hundred, and the problem is solved. Such a construct isn't a notably slow use of templates either. It's more trouble to avoid it than to have it. Compare some macros that can't loop and need a bunch of extremely repetitive lines for different sizes.

[ernst_klim]

>Mere arithmetic and some kind of ability to loop gives you that kind of turing completeness

I need my typechecker be total. And you don't need turing completeness for arithmetic and recursion.

[Dylan16807]

> I need my typechecker be total.

Recursion limits make it total, very easily.

> And you don't need turing completeness for arithmetic and recursion.

Yes you do. If you allow basic arithmetic to recurse n times, it can simulate n iterations of a turing machine.

[ernst_klim]

You don't need infinite loops, all you need are simple inductive types and reduction rules, it has not to be a turing complete language. You can have simple typelevel functions in haskell, whilst its typechecker is not turing-complete.