#6124: Spurious non-exhaustive warning with GADT and newtypes
-----------------------------------------------+----------------------------
Reporter: joeyadams | Owner:
Type: bug | Status: new
Priority: normal | Component: Compiler
(Type checker)
Version: 7.4.1 | Keywords:
Os: Unknown/Multiple | Architecture:
Unknown/Multiple
Failure: Incorrect warning at compile-time | Testcase:
Blockedby: | Blocking:
Related: |
-----------------------------------------------+----------------------------
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.
--
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/6124>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler
_______________________________________________
Glasgow-haskell-bugs mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs
