Programmers sometimes are quite upset in front of “nonexhaustive match” warnings. An example of a “nonmatching value” helps a lot not only in convincing them that they indeed wrote a nonexhaustive match, but also in correcting their code.
Such an example (or counterexample) is best expressed as a pattern representing a set of nonmatching instances. Then, programmers can add this “counterexample” at the end of their matching, hoping this will make it exhaustive. Consider an easy example.
let nilp = function [] > true Warning: this patternmatching is not exhaustive. Here is an example of a nonmatching value: _::_
The given pattern matching is not exhaustive and
all instances of the pattern _::_
(a list cell) are nonmatching.
Here, one achieves exhaustive match by adding a clause with
pattern _::_
.
Examples of nonmatching values are easily computed by a slight extension of algorithm U. Indeed, algorithm U shows that M(P, q^{→} ) is not empty by implicitly computing a witness of that fact.
The new algorithm I takes a matrix P and an integer n as arguments, since I is used in a context where the pattern vector q^{→} of Section 3.1 is a vector of n wildcards. Algorithm I normally returns a pattern vector p^{→} of size n such that all the instances of p^{→} are nonmatching values. Or, if no such vector exists (i.e. if P is exhaustive), I returns the distinguished constant ⊥.
I(  ⎛ ⎝  ⎞ ⎠  , 0) = ⊥ I(∅, 0) = (). 
If all those computations return ⊥, then I(P,n) also is ⊥. Otherwise, if one of the calls I(S(c_{k},P), a_{k} + n − 1) returns pattern vector (r_{1}⋯ r_{ak} p_{2}⋯ p_{n}), we can define I(P,n) = (c_{k}(r_{1}, … , r_{ak}) p_{2}⋯p_{n}). Of course, in practice, we stop performing recursive calls as soon as one such call is discovered. As there can be others c_{k′} such that I(S(c_{k′},P),a_{k′}+n−1) returns a pattern vector, algorithm I is nondeterministic.
It should be clear that I(P, n) = ⊥, if and only if P is exhaustive. Otherwise, I(P, n) is some pattern vector p^{→} and all the instances of p^{→} are nonmatching values.
A simple example will demonstrate algorithm I at work. Let us check the exhaustiveness of the following matching that acts on values of type mylist (Section 2).
match … with One 1 > ⋯
We thus compute I((One 1), 1).

One may think that algorithm I should make an additional effort
to provide more nonmatching values, by systematically computing
recursive calls on specialized matrices when possible, and by
returning a list of all pattern vectors returned by recursive calls.
We can first observe that it is not possible in general to supply the users
with all nonmatching values, since the signature of integers is
(potentially) infinite.
Furthermore, we claim that supplying one of the nonmatching patterns
is enough.
Correcting the source that triggers the warning is a programmer’s job,
and we intentionally limit the task of the compiler
to supplying a precise (and not too costly) warning, justified
by a concrete example.
In our example, the answer (NilCons (_,_))
points out the
most obvious forgotten pattern. Furthermore, if the programmers
write a clause for the flagged pattern and recompile
the corrected program,
then the compiler will flag other nonmatching
patterns such as One 0
.
Hence, the whole information is available to programmers, if they
want it.