so, you are right in that the following code is “safe”, in the sense that it will never fail with a
However, you are wrong in thinking it should not warn.
The way the “match is not exhaustive” compiler warning work changed somewhere in the
2.13.x releases cycle.
Before, it warned if it knew the match was not exhaustive, but now it warns if it can’t prove it is exhaustive.
That may sound the same, but they are very different. Formally speaking, being unable to prove that something doesn’t satisfy a property is not the same as providing that such an object does not satisfy the property.
With match expressions, the compiler is able to reach one of three conclusions.
a. It knows it is exhaustive.
b. It knows it is not exhaustive. (I am not familiar with the compiler internals, but I guess this is actually the same as above)
c. It doesn’t know whether it is exhaustive or not.
And that third case is the important bit.
Previously, it would not warn, now it warns; which makes sense to many folks (like me) since better safe than sorry.
Now, your next question will be:
Why the compiler can’t know that the current match is not exhaustive?
Well, because for it to know that it must be able to solve the halting problem, and if the compiler would be able to do that Martin would be extremely rich.
Now, joke answer aside, the compiler only has two ways to know if a match is exhaustive.
- You are matching a sealed type; i.e. an ADT. This makes sense, the compiler knows exactly all the possible values it may take.
- You use
case _, also known as cheating
And, despite what it may look like, your code is not doing
1 and absolutely not
+: are custom extractors, not an ADT.
At this point (if you are not tired of my bad humor) you would be asking.
How to fix it then?
What Luis would do:
List instead of a
Seq and pattern match using
:: instead of
What folks that like to use
Seq would do:
case Seq() with
case _ and put it as the last one.
PS: @SethTisue do you think this is worth it as a FAQ?
(of course, removing all the unnecessary failed attempt at comedy)