Spurious non-exhaustive warning with GADT and newtypes

[joeyadams]

This may be related to #3927 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.

[simonpj]

Thanks. I'm afriad this is part of a collection of pattern-match-exhaustiveness-checking tickets: #595, #5728, #3927, #5724, #5762, #4139. I think it's precisely #3927 but have not checked carefully.

This whole area needs love, but it's not trivial or I'd have done it by now!

Simon