[GHC] #3927: Incomplete/overlapped pattern warnings + GADTs = inadequate

[GHC]

#3927: Incomplete/overlapped pattern warnings + GADTs = inadequate
---------------------------------+------------------------------------------
    Reporter:  simonpj           |        Owner:  simonpj     
        Type:  bug               |       Status:  new         
    Priority:  high              |    Milestone:  7.2.1       
   Component:  Compiler          |      Version:  6.12.1      
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------
Changes (by conal):

 * cc: conal@… (added)


Comment:

 Here is another example of this problem, which arose in the blog post
 [http://conal.net/blog/posts/fixing-lists/ Fixing lists]. This example
 doesn't appear to be handled correctly in ghc 7.0.1 either. Moreover, I
 don't think SPJ's "quite correct" remark above (to pumpkin) applies in
 this case.

 {{{
 {-# LANGUAGE GADTs, KindSignatures, EmptyDataDecls #-}
 {-# OPTIONS_GHC -Wall #-}

 module Test where

 data Z
 data S n

 infixr 5 :<
 data Vec :: * -> * -> * where
   ZVec :: Vec Z a
   (:<) :: a -> Vec n a -> Vec (S n) a

 applyV :: Vec n (a -> b) -> Vec n a -> Vec n b
 ZVec      `applyV` ZVec      = ZVec
 (f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)

 -- GHC 6.12.3 gives me a warning (with -Wall)

 --     Warning: Pattern match(es) are non-exhaustive
 --              In the definition of `<*>':
 --                  Patterns not matched:
 --                      ZVec (_ :< _)
 --                      (_ :< _) ZVec

 -- Adding the following cases silences the compiler.

 -- ZVec `applyV` (_ :< _) = undefined
 -- (_ :< _) `applyV` ZVec = undefined

 -- However, benmachine found that GHC 7.0.1 balks at these definitions as
 ill-typed,
 -- but also warns of non-exhaustive patterns when the lines are removed.

 }}}

-- 
Ticket URL: <http://hackage.haskell.org/trac/ghc/ticket/3927#comment:14>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler