In practice, I have not (yet) found many great use cases for the distinction in Koka. It is nice to have "total" functions, but "pure" (exceptions+divergence) is still a good thing (and what Haskell gives you). And like you say, in practice we can easily have functions that just take a long long time to compute.

Still, it is a good extra check and I can see more use for the `div` effect for future verification tools where total functions can be used as a predicates (but non-terminating ones cannot).

Good to know. At compile or verification time, it seems like you could get the same problem again, though? We want our compiles to finish promptly, and a slow, total predicate could hang.

Which is to say, a possibly-diverging function seems okay to use even by a verification tool, so long as it finishes quickly in practice. Having some notion of analysis-time-safe predicates seems useful but it doesn't seem to map cleanly to being able to prove termination?

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.