What is the meaning of GHC.Err.patternFailure?

[christinaburge]

Is this effectively an error message or something else? I can't find it it in the docs!

[lastland]

Hi, GHC.Err.patternFailure is something we defined manually in Coq for denoting non-exhaustive matches. It is defined here:

hs-to-coq/examples/base-src/manual/GHC/Err.v

Lines 39 to 40 in c1ecb08

	Definition patternFailure {a} `{Default a} : a.
	Proof. exact default. Qed.

The background is that Haskell allows a pattern match to be non-exhaustive, while Coq requires all pattern matches to be exhaustive. The way we deal with that is by adding a catch-all case that returns a GHC.Err.patternFailure.

More information regarding how we handle Haskell partial functions in general can be found in Section 5.4 in our paper.

[christinaburge]

Thanks again for your help! I'm slightly unclear on one thing though: can coq routines be proven if they contain non-exhaustive matches?

[lastland]

Suppose you have a Haskell function f that contains an absent case, and a function g that calls f. If the use case of f in g ensures that the absent case would never happen, you should be able to prove whatever correct specifications you have of f, even though f is not exhaustive. However, if f's call site cannot guarantee that, you will not be able to prove anything specific about f's result---and that is still what you want because you will not be able to prove anything wrong.

Hope that answers your question!