"switch must be exhaustive" -- but it is

Using Swift
1

I have the following code:

func switchTest(_ n: UInt) -> String {
    switch n % 4 {
    case 0:
        return "0"
    case 1:
        return "1"
    case 2:
        return "2"
    case 3:
        return "3"
    }
}

If I attempt to compile this, the compiler will complain with error: switch must be exhaustive.

Now obviously I can shut this up by adding a default case and put something like preconditionFailure() there, but imho this makes the compiler check less useful since now I am doing a check at runtime that I rather would do at compile time. IIRC clang-tidy can check these cases for C/C++.

Should this be considered a bug? Or would this be a feature request? If so, how would I do this?

2 Likes
2

Swift understands switch exhaustiveness at the type level, but it doesn't understand math, so it sees the result of n % 4 as an arbitrary UInt value. We could teach the compiler to understand certain code patterns, but it's not possible to check arbitrary math expressions in full generality.

13 Likes
3

could we add a heuristic that can understand unbounded ranges?

switch x
{
case ...0:
    break

case 1:
    break

case 2...:
    break
}

this would solve many of my most common use cases.

2 Likes
4

It's definitely in the realm of possibility, especially if we get constant evaluation into the language. I agree it'd be nice to handle a certain set of obvious idioms, like ranges, </==/> comparisons against the same constant fenceposts, or % and & modular operations as in the example here. It'd take some thought to figure out the balance of what's practical to check statically vs. human intuition, since it's very easy for simple-looking sets of conditions to end up exploding into exponentially-complex sat problems.

8 Likes
5

Building on what Joe said, you can address this by adding a default: fatalError() case that the optimizer will strip out later, because it can prove that it's not needed: Compiler Explorer

For the rare case where performance is absolutely critical and there's some invariant that you know about but cannot convince the optimizer to adhere to, you can also do the following: Compiler Explorer. But I really do not recommend this, because unlike the first example, you are introducing undefined behavior if the "invariant" turns out not to be.

19 Likes
6

I understand this isn't trivial -- whatever the compiler is able to handle should probably be obvious so that a human isn't confused if some things work while others don't.

I wonder what exactly others, like clang-tidy are doing here?

1 Like
7

C family language implementations have a lot more leeway because switch exhaustiveness isn't really part of the core language; switch in C isn't required to be exhaustive, and any analysis that does attempt to check for exhaustiveness is a nicety provided by the compiler implementation rather than a requirement of the language design. And since they're generally just warnings, you can ignore the warning or turn it off if it's wrong.

5 Likes
8

oh that's nice! Just out of curiosity: how do fatalError and preconditionFailure compare in general? To me preconditionFailure seems a bit more descriptive and the compiler seems to optimize it away as well.

9

Good point. What about haskell? When I define a function in haskell I can also do pattern matching and the compiler seems to be able to proof whether the patterns are exhaustive. This check is a language requirement.

Specifically this works in Haskell:

example x | x `mod` 3 == 0 = "0"
          | x `mod` 3 == 1 = "1"
          | x `mod` 3 == 2 = "2"

Edit: please ignore this one, I was wrong. I just tried this locally and it seems that this produces a runtime error and not a compiler error if I make it non-exhaustive

10

Vanilla Haskell doesn't require match exclusivity, and it's a fatal error if you match against a value that doesn't have an arm in the match. GHC may support exhaustivity checking in some situations as an extension, though with its full array of type system extensions, even type-level exhaustivity checking is undecidable in the general case with GADTs. I'm not familiar with the limitations of when and how GHC does do exhaustivity checking, but that might be a good line of research to look into prior art when designing similar functionality for Swift.

6 Likes
11

preconditionFailure() may be assumed to be unreachable when built with -Ounchecked, resulting in undefined behavior if the invariant isn't. fatalError() will always trap, even in unchecked builds: Compiler Explorer. No one should really be building with -Ounchecked, but that's a story for another day.

You can find all this in the standard library reference documentation, by the way:

preconditionFailure:

  • In playgrounds and -Onone builds (the default for Xcode’s Debug configuration), stops program execution in a debuggable state after printing message.
  • In -O builds (the default for Xcode’s Release configuration), stops program execution.
  • In -Ounchecked builds, the optimizer may assume that this function is never called. Failure to satisfy that assumption is a serious programming error.

fatalError:

Unconditionally prints a given message and stops execution.

5 Likes