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 |