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?

Accepted Answer

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.

GADT's failed exhaustiveness checking

Solution

Problem