GADT's failed exhaustiveness checking

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.

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