Match Exhaustiveness Testing Ignores Guard Statements

[scabug]

It seems that guarded match expressions are not tested for completeness at compile time. Or, more accurately, it seems that guarded case statements are optimistically considered complete. For example, the following code will compile without "warning: match is not exhaustive!", even though calling it with a value of 1 will result in a MatchError.

def foo(x: Option[Int]): Int = x match {
  case Some(n) if n % 2 == 0 => n
  case None => 0
}

The equivalent code in Ocaml does print a non-exhaustive match warning at compile time.

let foo(x) = 
  match x with
  | Some n when n mod 2 = 0 -> n
  | None -> 0;;


Warning 8: this pattern-matching is not exhaustive.
Here is an example of a value that is not matched:
Some _
(However, some guarded clause may match this value.)
val foo : int option -> int = <fun>

Obviously the compiler can't decide whether or not arbitrary combinations of guards are complete, but I was surprised didn't treat guards pessimistically like Ocaml does. This actually bit us in production code, when a method like this:

def foo(x: Option[Int]): Int = x match {
  case Some(n) if n % 2 == 0 => n
  case _ => 0
}

was refactored to look like this:

def foo(x: Option[Int]): Int = x match {
  case Some(n) if n % 2 == 0 => n
  case None => 0
}

which resulted in runtime MatchErrors.

I understand that adding a warning that treats guarded match statements pessimistically could be annoying in cases when the combined guards actually are safe, but in these instances the warning could easily be dismissed with an annotation or a noop unguarded match. Why don't we give Scala users the option for added safety?

[scabug]

Imported From: https://issues.scala-lang.org/browse/SI-5365?orig=1
Reporter: Jon Shea (jonshea)
Affected Versions: 2.9.1
See #9232

[scabug]

@adriaanm said:
it's a tricky balance of how often we should cry wolf
when guards are statically known to fail/succeed, we take it into account
as soon as statistics are involved, I think we should back off
matches with guards are known to fail, no need to remind the user

[scabug]

Richard Bradley (richard.bradley) said (edited on Apr 24, 2015 10:10:16 AM UTC):
I came here to raise the same bug, but I'm disappointed to see this as WONTFIX.

Are you saying that "if" clauses / case guards defeat the exhaustiveness checks by design?
Is that documented somewhere? I find it rather surprising.

(See also scapegoat-scala/scapegoat#45 )

[scabug]

@adriaanm said:
Hi Richard,

I understand it's disappointing, and it's not very intuitive why we bail out when there are guards, but our key design goal is not to have spurious warnings, as that would undermine their utility while annoying a lot of users.

In general, we can't statically decide whether a guard is true or false (in the extreme it could be a method call that calls into some REST API), so we have to punt. You're right that there are simple cases where we could, and I believe we do (or could) track the same level of information as our constant folder does, but guards that depend on the value of patterns are quite tricky to reason about in general. I would be happy to include a contribution that meets our design goals and refines the handling of guards, but I suspect it would be a significant effort.

cheers
adriaan

[scabug]

Richard Bradley (richard.bradley) said (edited on Apr 24, 2015 4:55:49 PM UTC):

In general, we can't statically decide whether a guard is true or false ... you're right that there are simple cases where we could,

I agree that scalac can't determine the result of all "if" guards at compile time, but I don't think the right fix is to try to do that in simple cases.

I think that scalac should treat all "if" guards as possibly-false at compile time, and adjust the exhaustiveness checks accordingly.

So code like:

x match {
  case Some(n) if n % 2 == 0 => "even"
  case None => "nothing"
}

would give an exhaustiveness warning, and users would know that they need to do either:

x match {
  case Some(n) if n % 2 == 0 => "even"
  case Some(n) => "odd"
  case None => "nothing"
}

or

x match {
  case Some(n) if n % 2 == 0 => "even"
  case _ => "not even"
}

to fix the warning.

our key design goal is not to have spurious warnings

Are you saying that treating "if" guards as possibly-false would lead to spurious warnings? I don't think that the warning in the example above would be suprious, I think it would be correct and very helpful.

[scabug]

@adriaanm said:
Agreed in your example, but if we approximate the guard by false, then we produce spurious warnings for complimentary cases like {case p if g1 => ... case p if g2 => ... } where g1 || g2 is constant true. This also sounds like a common case to me, where you want to further refine handling. True, you could move these ifs into the case body, but it would still be noise.

[scabug]

Richard Bradley (richard.bradley) said:
I don't think that example stands up to scrutiny. If g1 || g2 really is constant true, then rewrite your proposed:

x match {
  case p if g1 => ...
  case p if g2 => ...
}

to just:

x match {
  case p if g1 => ...
  case p => ...
}

This will a) allow the compiler to verify exhaustiveness and b) will help the reader to understand the code.

[scabug]

@adriaanm said:
Fair enough, how about g1 || g2 || g3? People write the darnedest code!

[scabug]

Richard Bradley (richard.bradley) said (edited on Apr 27, 2015 4:00:28 PM UTC):

Fair enough, how about g1 || g2 || g3? People write the darnedest code!

Are you asking about the case with code like

x match {
  case p if g1 => ...
  case p if g2 => ...
  case p if g3 => ...
}

... and where the compiler cannot establish that g1 || g2 || g3 === true?

Exactly the same principle applies. The compiler ought to complain that the match may not be exhaustive, and give an error like:

  warning: match may not be exhaustive.
  It would fail on the following input: p 
  (Note that 'if' guard clauses assumed to be false for the purposes of exhaustiveness checks.)

Then the user will realise that it is unhelpful to both the compiler and to the readers of their code to expect them to infer that g1 || g2 || g3 === true, and they should rewrite the code as follows:

x match {
  case p if g1 => ...
  case p if g2 => ...
  case p => ...
}

This is much easier to read; it is much easier for the compiler to verify, and (assuming that the identity is in fact true, and that the tests have no side-effects), it is completely equivalent.

Therefore I think that:

1. the compiler should not give up on exhaustivity checks when encountering guard checks, as it will omit useful warnings (as can be seen in the initial bug report at the top)
2. the compiler should assume that all guards are "false" when performing exhaustivity checks, as it is simple, predictable and correct (in general)

[scabug]

Richard Bradley (richard.bradley) said:
(This has parallels with "definite assignment analysis".
In the g1 || g2 || g3 === true case, we wouldn't expect the compiler to be happy with Java code like:

int i;
if (g1) {
 i = 1
} else if (g2) {
 i = 2
} else if (g3) {
 i = 3
}
println(i)

It is not considered a burden on developers that they need to "help" the compiler (and readers of their code) by changing the last block to an "else", like:

int i;
if (g1) {
 i = 1
} else if (g2) {
 i = 2
} else {
 i = 3
}
println(i)

I think this is how people expect the compiler to behave in this case.)

[scabug]

Mark Feeney (overthink) said:
Scala used to issue exhaustiveness warnings in the face of guards. It seems to have disappeared as of 2.10.x: https://gist.github.com/overthink/e56f35159f6bc5751d34 I had stupidly been relying on these warnings... and just got burned.

I would value a compiler flag that will cause a warning when exhaustiveness checks are disabled.

[scabug]

@SethTisue said:
fwiw, I find Richard's arguments persuasive.

[scabug]

@non said:
If Seth is interested in revisiting this, I agree that Richard's arguments seem reasonable. When N cases are guaranteed to be complete, you can always remove the guard (or use case _) from the last one to get completeness.

What would be the process for reopening this?

[scabug]

@lrytz said:
I agree as well.

There are cases today when you get a spurious warning: if you know more than the compiler about the possible values that can reach the match. That's why we already have the @unchecked annotation.

I don't see an example (yet?) where the change proposed here would lead to new spurious warnings.

• As discussed, if ||(conditions) is always true, it is good practice to leave the last out.
• If there's a single pattern with a guard then you know more than the compiler. But then why even put the condition in the first place? Just leave it away.
• If there are multiple conditions, but their || might be false, again you know more than the compiler. Same thing: just leave away the last condition.

One argument might be that an incomplete match is like an assertion (in the shape of a MatchError). But firstly, this is bad style (better make it explicit, so others can see it), and secondly, doing the same thing with just patterns (no guards) does give an exhaustiveness warning. So it would be fine to also issue it in the case of guards.

[scabug]

@adriaanm said:
I'll reopen to keep the discussion going, but I am still catching up with email after one of those european-style vacations.

[scabug]

@adriaanm said:
Ok, it seems there's consensus, so I'm happy to be proven wrong/overly pessimistic. Please submit a PR! Let's make sure it doesn't add any noise to the community build, though. A great bonus would be if it could uncover existing exhaustivity problems!

It would be nice if we could do a corpus analysis to see whether there are any matches out there that violate the (valid) style guidelines above (maybe under a -Y flag included in the PR?)

[scabug]

@retronym said:
scala/scala#4929

[scabug]

@SethTisue said:
the PR was abandoned but could be revived by an interested contributor

[LogicalTime]

Having this is one of my biggest Scala desires, it has been for years. I really hope we can convince someone to implement it.

[lrytz]

scala/scala#4929 could certainly be revived

[swachter]

Just now fixed a bug that would have been caught by the compiler if it would default to assuming that guards always fail. IMHO that would improve the current situation.

[yawaramin]

FWIW I just tried it in Dotty and saw the same MatchError: https://scastie.scala-lang.org/5DVh9YP3RqG1VOGNioI4vQ

[martijnhoekstra]

@smarter did this regress in dotty? Should the label be removed?

[smarter]

It's possible I got it wrong at the time. I've opened lampepfl/dotty#8708

[smarter]

Actually fixed in dotty now: lampepfl/dotty#8698 :)