I mentioned this later

> You can separate terms that can be used in proofs (those must be total) from terms that can only be used in computations (those can be Turing complete), like in Lean

What I meant is that the part of Idris that lets people prove theorems is the non-total part

But, I think you are right. Haskell could go there by adding a keyword to mark total functions, rather than marking nontotal functions like Idris does. It's otherwise very similar languages