Spurious non-exhaustive warning with GADT and newtypes

This may be related to #3927 (closed) or similar, but here's another case where the compiler produces a "Pattern match(es) are non-exhaustive" warning for patterns on a GADT that are impossible to implement:

newtype A = MkA Int
newtype B = MkB Char

data T a where
    A :: T A
    B :: T B

f :: T A -> A
f A = undefined

This produces the following warning:

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

It is impossible to write a pattern for B because B :: T B does not match T A.

If I replace newtype with data for both A and B, the warning goes away. If I replace only one instance of either newtype, it will still produce the warning.

Trac metadata

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