I have found total checks in languages like idris helpful, but really only for catching small mistakes that I've made (for example, recursing on the original argument)
If your language has equality proofs, for example `a = Int` then, if your language is non-total I can prove anything by divergence. So I can prove `Int = String`. This is still type-safe as long as you don't erase the proof, because you can never use the invalid proof because your program will diverge.
So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.
So if you want to be type-safe but you still want to be able to erase proofs, your proofs have to be total.