Erroneous "non-exhaustive pattern match" using nested GADT with strictness annotation

In the following code, fun contains an exhaustive pattern match, but, when compiling with -Wall, ghc erroneously reports a non-exhaustive pattern match.

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

This report came from https://stackoverflow.com/questions/16225281/gadts-failed-exhaustiveness-checking . Without strictness annotations, this is indeed a failed exhaustive check, due to bottom. I spoke to Richard Eisenberg at PLDI a few days ago, and he informed me that, if this warning did not disappear with strictness annotations, it was a bug. I added strictness annotations, and it did not disappear. I've tried all combinations of using strictness annotations and/or running with {-# LANGUAGE Strict #-}.

Trac metadata

Trac field	Value
Version	8.4.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture