Ticket #6124 (new bug)
Spurious non-exhaustive warning with GADT and newtypes
|Reported by:||joeyadams||Owned by:|
|Component:||Compiler (Type checker)||Version:||7.4.1|
|Type of failure:||Incorrect warning at compile-time||Difficulty:||Unknown|
|Test Case:||Blocked By:|
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.