Totality matters not because it guarantees typechecking terminates, but because it means you don't have to evaluate certain things at all. In a total language, if you have a proof that two types are equal then you can transport values between them, preserving type safety, without any runtime cost. Without totality, you have to evaluate your proofs before you can trust them.