I agree with your assessment, Richard, but my (possibly flawed) understanding is that in the Haskell community "totality" does not have the same meaning as in mathematics/PLT—Haskellers use "total" for the property "doesn't throw non-exhaustive pattern match errors" or perhaps "doesn't throw any exceptions at all" vs "terminating" for the property "doesn't loop infinitely". [citation needed]
Hence I understood Henning's proposal to refer to the notion of "exception-free". This would already be a very useful property and I suspect would be easier to solve. Yes, complete pattern matches are undecidable in the presence of GADTs, but can't we simply build on GHC's existing heuristics?
Would this really be a pragma or would it be a language /restriction/ (heh)?
Regarding nontermination, I would be grateful if Haskell at least had an option for explicit let-rec...