[dllthomas]

Strictly speaking, "totality" is asking for more than just exhaustiveness in pattern matching (all manner of languages let you check exhaustiveness). For totality, you also have to prove termination for all inputs, which means your language (or sub-language) is not Turing complete.

Though these days I've been saying "Turing complete" is a bug, not a feature, provided you can accomplish your aims without it.