Switch expression is not exhaustive on integers

[Pante]

• Dart 3.0.0

The analyzer claims that the following code snippet isn't exhaustive when it is. It emits the following message: The type 'int' is not exhaustively matched by the switch cases since it doesn't match 'int()'.

void main() {
  final foo = switch ('a'.compareTo('b')) {
    > 0 => 'more',
    == 0 => 'equal',
    < 0 => 'less',
  };
}

[ltOgt]

Relatedly, this also does not work for the following case:

bool bothTheSame(bool? a, bool? b) => switch ((a, b)) {
    (bool? b1, bool? b2) when b1 == b2 => true,
    (bool? b1, bool? b2) when b1 != b2 => false,
    // The type '(bool?, bool?)' is not exhaustively matched by the switch cases since it doesn't match '(_, _)'.
};

If exhaustiveness cant be guaranteed for non sealed / enum types, maybe the error message should be clearer

[lrhn]

The first switch is not exhaustive because there is no specified way to exhaust integers.
Exhausting integers by range exhaustion, like this example tries, is something that could be possible (probably), with some possible caveats about the difference between web numbers and native integers.
But it's not part of the current exhaustiveness definition.
See #2474 (comment)
(Don't know if we have an open issue for it.)

The second example doesn't work because a case with a with clause never counts towards exhaustiveness. The compiler cannot be expected to evaluate arbitrary expressions for all possible values while compiling, so if a case has a when, the compiler goes "damn if I know what that means", and excludes the entire case from exhaustion checking.
Which means that. as far as the compiler knows, the example switch can reach the point after the two first cases with any combination of values still possible. That's what the error message says: It (possibly) doesn't match anything.
That's working as intended, and is unlikely to change.

It's not because (bool?, bool?) is not sealed/enum, it's treated just as if bool was an enum, and so the entire record is a "must exhaust" type, and it can be exhausted by, e.g.,

bool bothTheSame(bool? a, bool? b) => switch ((a, b)) {
    (true, true) => true,
    (true, false) => false,
    (true, null) => false,
    (false, false) => true,
    (false, true) => false,
    (false, null) => false,
    (null, null) => true,
    (null, true) => false,
    (null, false) => false,
 };

(But that's just doing bool bothTheSame(bool? a, bool? b) => a == b; the long way 😉.)

[leafpetersen]

Or more succinctly (though not as succinct as a == b):

bool bothTheSame(bool? a, bool? b) => switch ((a, b)) {
    (true, true) => true,
    (false, false) => true,
    (null, null) => true,
    (_, _) => false
 };

[munificent]

We definitely could do exhaustiveness checking over integer ranges with relational patterns. It's something some other languages do and is something I'd like to do for Dart. We just didn't have time to get it in to 3.0.

[adriank]

@munificent could that also be possible for double?

[lrhn]

No, you cannot exhaust doubles using <, == and > patterns, or any non-match-all pattern, because you cannot match NaN using any of the match types which work towards exhaustiveness.
(Getting more and more convinced that a constant pattern of double.nan should match any NaN value, rather than use == and give false. Because then it's actually useful instead of completely useless. Won't be able to distinguish different NaN values that way, but who cares.)

So, here's a proposal:

Number exhaustion

Allow the type int to be exhausted by range exhaustion introduced by relational operators:

• A pattern of == c or c/const c exhausts a single value.
• A pattern of < c, > c, <= c, or >= c exhausts the entire range from c (inclusive or exclusive, so from c or from c±1 to min/max-value (on web, the max values are infinities, but NaN is not an int).
• Combining patterns with || exhausts the union of the ranges (which is just a set of ranges).
• Combining patterns with && exhausts the intersections of the ranges (which can be a finite range, like >= 0 && < 10. And can be empty, in which case it's discarded. Combining sets of ranges with && includes all the pair-wise intersections.
• The "spaces" for int is a set of ranges, starting out at {(minValue..maxValue)}, and each pattern can exhaust some sub-ranges of this, which leaves the remaining ranges. (Exhausting 0 from the above leaves {(minValue..-1), (1..maxValue)}, exhausting > 0 (subtracting the intersections with (1..maxValue)) from that leaves {(*minValue*..-1)}, and then exhausting < 0 will leave the unmatched space as empty, which means exhausted.

I have no idea if the algorithm's use of spaces allows for such a dynamically defined "space set". It might have to be special-cased.

Allow exhausting double as follows:

• Make the double.nan constant pattern be special cased to work like .isNan. (Can still use == double.nan to have a pattern that never matches.)
• Make double be exhausted in the same way as int, plus giving NaN a space of its own.
• Except probably introduce open and closed ranges, so <= 5 is the inclusive range [-infinity .. 5], and < 5 is the end-exclusive range [-Infinity .. 5). ... Because nobody wants to look at an inclusive range of (infinity .. 4.99999999999999911182158029987476766109466552734375).
• Can still define intersection of sets of ranges in such a way that the non-NaN doubles are exhausted if the set {[-infinity .. infinity]} is covered by the switch cases.
• That is, double is treated as the union of NaN values and a range of non-NaN values that can be exhausted by ranges.

Same caveats about exhaustiveness algorithm and how it implements spaces applies.

The next question is whether this algorithm should be implemented by inference/reachability analysis.
So far reachability analysis only tries to predict exhaustieness for simple cases of enums/sealed types/union types
and must-exhaust types (which it doesn't check, it just assumes).
If it starts doing exhaustiveness analysis on integers, then inference will notice that:

    switch (someInt) {
      case <0: sign = -1;
      case ==0: sign = 0;
      case >0: sign = 1;
      default: throw "unreachable";
    }

now cannot reach the default case. Or if the default case wasn't there, it now cannot fall through without going through one of the branches, which may change the definite-assignment state of the sign variable, making a later assignment (probably unreachable, since it was actually always assigned here) into a compile-time error.
Most likely that won't cause any real errors, because the code already runs correctly today. It'll just make code that never runs be recognized as dead. That's only a warning.

Doing range exhaustion in the reacahbility analysis does mean doing it twice, if it's also done in the exhaustiveness checking. It's not necessary if the switch is already must-exhaust (because it's an expression, or because it switches over a sealed type, which could look something like:

switch (Scale) { // A sealed type with two subtypes
  case Linear(magnitude: < 0): timyScale(...);
  case Linear(magnitude: >= 0 && < 10): smallScale(...);
  case Linear(magnitude: > 10): bigScale(...);
  case Logarithmic(): logScale();
}

Here the switch must be exhaustive, which means the inference doesn't need to check, it can leave that to the exhaustiveness algorithm.
It's only for a non-always-exhaustive switch where recognizing that int-ranges cover all integers can make some case/fallthrough unreachable (and if the check is exact, then it doesn't need to run the exhaustiveness algorithm afterwards).

I'd go with no letting inference do int-range checking, and only check for exhaustiveness in switches that must be exhaustive. (We really should introduce a switch! (...) which must be exhaustive.)

The other side of that coin is whether int/double should themselves become "must exhaust" types.
Probably too breaking to add it today. Also, it's very common for an int to be known to only contain, say, non-negative numbers, so forcing switch (foo.length) { case 0: ..., case 1: ..., case >1: ... } to also account for negative nubmers is just annoying.
I'd say no, which means this change probably won't affect any existing switches.

All in all: Only a change to the exhaustiveness algorithm, not anything else. Only affects switches that must be exhaustive for other reasons (like switch expressions).
If possible.

[MelbourneDeveloper]

Generally not a huge deal, but when this bites you, it bites you hard because it's very confusing to figure out why this is happening. If you don't know that the exhaustiveness checker doesn't handle integers like this, you'll be scratching your head.