I believe these terms (including "exceptional state", but no "exception") are commonly used in formal languages, combinatorics, rewriting systems, mathematical logic and so. They are also used in Haskell because this was partially based on System F, which comes from the simply typed lambda calculus. I understand your frustration and please believe me that it was not my intention to turn this thread into a pedantic show.
But now coming back to your original point and example: I don't think anyone from the Haskell and ML-family languages camp is claiming one can automatically deduce every possible decidable property from any function with their type system, or at least not yet :)
Yes, they are commonly used in formal languages, and their precise meaning is language dependent, which is why I didn't use partial or divergence but termination, which has a unique computational meaning.
I don't think anyone claims that any property can be proven. I do think that some think that if a program can be decomposed into simple parts, whose "interesting" properties are provable in isolation, then you can feasibly prove interesting properties of their composition, which is not true. A proof of that was only given in the past 10-15 years, and is referenced in my post.
But now coming back to your original point and example: I don't think anyone from the Haskell and ML-family languages camp is claiming one can automatically deduce every possible decidable property from any function with their type system, or at least not yet :)