[GHC] #6124: Spurious non-exhaustive warning with GADT and newtypes

[GHC]

#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