GADT's failed exhaustiveness checking

Question

Consider the following code:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1

Even though fun is an exhaustive match, when compiling with -Wall, GHC complains about a missing case. However, if I add another constructor:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl Baz) = 2

Then GHC correctly detects that fun is total.

I am using code similar to this in my work, and would like GHC to raise warnings if I have missed cases, and not raise warnings if I don't. Why is GHC complaining on the first program, and how can I get the first sample to compile without warnings without adding spurious constructors or cases?

Answer 1

The problem actually reported is:

Warning: Pattern match(es) are non-exhaustive
         In an equation for `fun': Patterns not matched: Inl _

Which is true. You provide a case for the Inr constructor, but not the Inl constructor.

What you're hoping is that since there's no way to provide a value of type Sig B that uses the Inl constructor (it would need an argument of type Foo B, but the only constructor for Foo is of type Foo A), that ghc will notice that you don't need to handle the Inl constructor.

The trouble is that due to bottom every type is inhabited. There are values of type Sig B that use the Inl constructor; there are even non-bottom values. They must contain bottom, but they are not themselves bottom. So it is possible for the program to be evaluating a call to fun that fails to match; that's what ghc is warning about.

So to fix that you need to change fun to something like this:

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = error "whoops"

But now of course if you later add Baz :: Foo B this function is a time bomb waiting to happen. It's be nice for ghc to warn about that, but the only way to make that happen is to pattern match foo against a currently-exhaustive set of patterns. Unfortunately there are no valid patterns you can put there! foo is known to be of type Foo B, which is only inhabited by bottom, and you can't write a pattern for bottom.

But you could pass it to a function that accepts an argument of polymorphic type Foo a. That function could then match against all the currently-existing Foo constructors, so that you'll get a warning if you later add one. Something like this:

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl foo) = errorFoo foo
    where 
        errorFoo :: Foo a -> b
        errorFoo Foo = error "whoops"

Now You've properly handled all the constructors of :+: in fun, the "impossible" case simply errors out if it ever actually occurs and if you ever add Baz :: Foo B you get a warning about a non-exhaustive pattern in errorFoo, which is at least directing you to look at fun because it's defined in an attached where.

On the downside, when you add unrelated constructors to Foo (say more of type Foo A) you'll have to add more cases to errorFoo, and that could be unfun (though easy and mechanical) if you've got lots of functions applying this pattern.

Answer 2

I'm sorry to tell you this, but your first example is not quite as exhaustive as you think it is:

∀x. x ⊢ fun (Inl (undefined :: Foo B))
*** Exception: Test.hs:48:1-17: Non-exhaustive patterns in function fun

Annoying, yes, but them's the breaks. ⊥ is why we can't have nice things. :[

Answer 3

As already mentioned. The case you are not handling is Inl _|_, which is not itself _|_, and thus must be handled.

Luckily there is a perfectly nice way to handle this:

data (:+:) f g a = Inl (f a) | Inr (g a)

data A
data B

data Foo l where
  Foo :: Foo A
  Baz :: Foo B

data Bar l where
  Bar :: Bar B

type Sig = Foo :+: Bar

fun :: Sig B -> Int
fun (Inr Bar) = 1
fun (Inl x) = case x of {}

Now if you do add in the Baz :: Foo B constructor, you will appropriately get:

    Pattern match(es) are non-exhaustive
    In a case alternative: Patterns not matched: Baz
   |
21 | fun (Inl x) = case x of {}
   |               ^^^^

Thus you can appropriately change the code to something like your second example to properly handle the new case you have created.