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.