Nested pattern matching not exhaustive warning

Question

Consider the following code example:

function
  | [] -> "bla"
  | ds -> let x::l = List.rev ds in "woot";;

When compiling / interpreting the above piece of code the following warning occur:

line 3, characters 14-18:
Warning 8: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
[]

I wonder why this warning appear. It is clear that [] is not a valid option due to the top level pattern-matching. I expect the compiler / interpreter of OCaml to be able to easily deduce the exhaustiveness of the above code by passing information from the top-level matching to the nested matching. Why isn't that the case? Am I missing something?

Amadan Amadan · Accepted Answer · 2018-11-07T10:21:54

OCaml is complaining about

let x::l = List.rev ds in "woot"

which will fail if List.rev ds produces [].

Of course, we know that it can't, because if List.rev ds would be empty, then ds would have to be empty, which is impossible because of the other guard; but OCaml doesn't know that.

See docs:

OCaml's pattern matching can check whether a set of patterns is exhaustive or not, based on the type only.

and goes on to present an example that is remarkably similar to yours.

Regarding your "easily deduce the exhaustiveness of the above code"... I don't think it's as easy as you make it sound. Imagine if you demanded instead of ds not being empty that it must be "foo", and the inner guard making sure that Digest.to_hex(Digest.string ds) is "acbd18db4cc2f85cedef654fccc4a4d8" (which must be so, as that is the MD5 digest of "foo"). Not as simple any more, even for us humans. But is there a difference between List.rev ds and Digest.to_hex(Digest.string ds), from a computer's point of view? Types are easy. Values are hard.

Nested pattern matching not exhaustive warning

1 Answers