Programmers sometimes are quite upset in front of “non-exhaustive match” warnings. An example of a “non-matching value” helps a lot not only in convincing them that they indeed wrote a non-exhaustive match, but also in correcting their code.
Such an example (or counter-example) is best expressed as a pattern representing a set of non-matching instances. Then, programmers can add this “counter-example” at the end of their matching, hoping this will make it exhaustive. Consider an easy example.
let nilp = function  -> true Warning: this pattern-matching is not exhaustive. Here is an example of a non-matching value: _::_
The given pattern matching is not exhaustive and
all instances of the pattern
_::_ (a list cell) are non-matching.
Here, one achieves exhaustive match by adding a clause with
Examples of non-matching 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 non-matching values. Or, if no such vector exists (i.e. if P is exhaustive), I returns the distinguished constant ⊥.
|, 0) = ⊥ I(∅, 0) = ().|
If all those computations return ⊥, then I(P,n) also is ⊥. Otherwise, if one of the calls I(S(ck,P), ak + n − 1) returns pattern vector (r1⋯ rak p2⋯ pn), we can define I(P,n) = (ck(r1, … , rak) p2⋯pn). Of course, in practice, we stop performing recursive calls as soon as one such call is discovered. As there can be others ck′ such that I(S(ck′,P),ak′+n−1) returns a pattern vector, algorithm I is non-deterministic.
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 non-matching 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 non-matching 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 non-matching values, since the signature of integers is
Furthermore, we claim that supplying one of the non-matching patterns
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
(Nil|Cons (_,_)) 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 non-matching
patterns such as
Hence, the whole information is available to programmers, if they