Re: WARNING pragmas in `Prelude.undefined` and `Prelude.error`

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...

On 23 Dec 2019, at 17:44, Richard Eisenberg wrote:

GADT restrictions say that the match is actually total - incomplete uni-pattern matches - unless GADT restrictions say that the match is actually total - partial record selectors - non-strictly-positive datatypes - Typeable allows you to simulate non-strictly-positive datatypes (see Sec. 7 of https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs https://repository.brynmawr.edu/cgi/viewcontent.cgi?article=1002&context=compsci_pubs) - Girard's paradox (because we have Type :: Type), though it is not known whether this is encodable in Haskell. See https://link.springer.com/chapter/10.1007/BFb0014058 https://link.springer.com/chapter/10.1007/BFb0014058 - -fdefer-type-errors