Nested exhaustive pattern matching in Purescript

Question

Consider my two attempts at writing the same function:

data Foo = Bar Int | Quux Int | Baz Int

f :: Foo -> Int
f (Bar n) = n
f other =
  case other of
    Quux n -> 2 * n
    Baz n -> 3 * n

g :: Foo -> Int
g foo =
  case foo of
    Bar n -> n
    other ->
      case other of
        Quux n -> 2 * n
        Baz n -> 3 * n

Neither f nor g compiles, because the case statement on other is non-exhaustive in each version.

Is there another way to write these functions such that the fact that other is statically known not to be of the Bar variant is used by the compiler to prove that the case statement is indeed exhaustive?

This can be worked around in various ways (e.g., by throwing an exception if Bar is encountered in the case statement), but I'd be interested in something that can be statically checked.

Answer 1

Probably it is also about the fact that you only want to handle these two cases (Quux and Baz) further.

Therefore, you could simply add a case that recursively uses f again. Because there is already the "base case" for (Bar n).

f :: Foo -> Int
f (Bar n) = n
f other =
  case other of
    Quux n -> 2 * n
    Baz n -> 3 * n
    _ -> f other

The use of _ means that every other case is processed with it.

But this is just a workaround to make the example compilable. You cannot create a function that only accepts Quux and Baz and not Bar.

Then you should separate these types:

data Foo = Quux Int | Baz Int

newtype Bar = Bar Int

So now you have to work with two types.