[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.