[GHC] #14098: Incorrect pattern match warning on nested GADTs

7 Aug 2017

      #14098: Incorrect pattern match warning on nested GADTs
-------------------------------------+-------------------------------------
           Reporter:  jmgrosen       |             Owner:  (none)
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:                 |  Operating System:  Unknown/Multiple
  PatternMatchWarnings               |
       Architecture:                 |   Type of failure:  Incorrect
  Unknown/Multiple                   |  error/warning at compile-time
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 {{{#!hs
 {-# Language GADTs #-}

 data App f a where
   App :: f a -> App f (Maybe a)

 data Ty a where
   TBool :: Ty Bool
   TInt  :: Ty Int

 data T f a where
   C :: T Ty (Maybe Bool)

 -- Warning
 f :: T f a -> App f a -> ()
 f C (App TBool) = ()

 -- No warning
 g :: T f a -> App f a -> ()
 g C (App x) = case x of
                 TBool -> ()
 }}}

 When compiling, with `-Wincomplete-patterns`:
 {{{
 Foo.hs:15:1: warning: [-Wincomplete-patterns]
     Pattern match(es) are non-exhaustive
     In an equation for ‘f’: Patterns not matched: C (App TInt)
    |
 15 | f C (App TBool) = ()
    | ^^^^^^^^^^^^^^^^^^^^
 }}}

 I'm sorry for such a complicated example, but I wasn't able to reduce it
 any further than this.

 The gist of the problem is that this code gives a pattern matching non-
 exhaustiveness warning when matching a nested pattern, when pulling out a
 value then matching on it produces no warning (correctly). It also seems
 to have to do with using a type constructor (`Maybe`) within the
 constructor definition of `App`, as changing it to
 {{{#!hs
 data App f a where
   App :: f a -> App f a

 ...

 data T f a where
   C :: T Ty Bool
 }}}
 does not give a warning, even when `App` is modified further to force it
 to be a proper GADT.

 This might be a known limitation of the checker, but given that it works
 fine when the nesting is removed, I would think it would be more of a bug.

 Thanks to Iavor for helping me minimize the test case.

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14098
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler