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?

Wantage

The best part is how adding fun (Inl Foo) = ... is a type error. Man, you just can't catch a break! (but using _ works, of course) – Forensics

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.

Susurrus

A shame. In the actual code, a variant of the :+: operator is nested to sum together dozens of datatypes totaling hundreds of constructors. I guess I'll have to suck it up and forgo type safety in my casing, and hope some future version of GHC offers a solution. – Wantage

@JamesKoppel It's tricky to see what it could do. GHC is correctly able to rule out incorrectly typed constructors when pattern matching on GADTs, as shown in your second example. It's matching on the type containing a GADT value that's the issue, and there GHC really has no generic way of knowing that Inl shouldn't occur. What if Foo l was defined as an abstract type in another module, which didn't export the constructors? Then GHC would have no way of guessing for what types l Foo l is valid, it's just checking that all the cases of :+: are handled. – Susurrus

Foo is not an abstract type, so it's quite trivial to show Inl cannot occur without ⊥. Though I don't need that -- I'd be happy if I can provide some annotation so that GHC warns if I do not explicitly (i.e.: not using wildcards) handle each constructor. – Wantage

"and you can't write a pattern for bottom.": using EmptyCase you actually basically can. – Collaborative

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. :[

Forensics

I'd be happy to provide cases for undefined things, as long as I still get warnings when I actually define new productions of type Sig B. Can you think of any way to do that? – Wantage

@JamesKoppel quite a few years late but you could use EmptyCase to add a fun (Inl x) = case x of case, this will warn if at some point in the future ghc thinks there is a non-_|_ x that fits (such as adding new constructors to Foo). – Collaborative

@Collaborative Thanks! – Wantage

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.

Collaborative