What is Haskell missing for totality checking?

Question

A total (functional) language is one in which everything can be shown to terminate. Obviously, there are lots of places where I don't want this - throwing exceptions is sometimes handy, a web-server isn't supposed to terminate, etc. But sometimes, I would like a local totality check to enable certain optimizations. For example, if I have a provably-total function

commutativity :: forall (n :: Nat) (m :: Nat). n + m :~: m + n
commutativity = ...

then, since :~: has exactly one inhabitant (Refl), GHC could optimize

gcastWith (commutativity @n @m) someExpression
  ==>
someExpression

And my proof of commutativity goes from having an O(n) runtime cost to being free. So, now for my question:

What are some of the subtle difficulties in making a totality checker for Haskell?

Obviously, such a checker is conservative so whenever GHC isn't sure something is total (or is to lazy to check) it could assume it isn't... Seems to me it might not be too difficult to cobble together a not-so-smart checker that would still be very useful (at least it should be straightforward to eliminate all my arithmetic proofs). Yet, I can't seem to find any efforts to build such a thing into GHC, so obviously I'm missing some pretty big constraints. Go ahead SO, crush my dreams. :)

---

Relevant but not recent: Unfailing Haskell by Neil Mitchell, 2005.

Answer 1

Liquid Haskell has totality checking: https://github.com/ucsd-progsys/liquidhaskell#termination-check

By default a termination check is performed on all recursive functions.

Use the no-termination option to disable the check

liquid --no-termination test.hs

In recursive functions the first algebraic or integer argument should be decreasing.

The default decreasing measure for lists is length and Integers its value.

(I included screenshot and quote for posterity.)

Similar to in Agda or other languages with totality checking, the arguments to the function must become structurally smaller over time to reach the base case. Combined with a totality checker, this makes for a reliable check for a number of functions. LH also supports helping the checker along by indicating how things decrease, which you could do with an abstract data type that's opaque or from an FFI. It's really quite practical.