[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.0.1       
   Component:  Compiler          |      Version:  6.12.1      
    Keywords:                    |     Testcase:              
   Blockedby:                    |   Difficulty:              
          Os:  Unknown/Multiple  |     Blocking:              
Architecture:  Unknown/Multiple  |      Failure:  None/Unknown
---------------------------------+------------------------------------------

Comment(by pumpkin):

 I understand that you can provide bottoms for Fin Nz, but the issue is
 that in the code I submitted, the pattern match itself is badly typed. The
 warning alludes to it, but the fact remains that for my index function,
 Nil and Fz or Fs cannot "coexist" within a pattern and have consistent
 types. I see that the warning spots that, but I'd expect it to be an error
 instead of a warning, a bit like the test function above, since the
 constructors in the pattern are impossible to type correctly.

 Just to clarify, I'm advocating that

 {{{
 index :: Vec n a -> Fin n -> a
 index Nil Fz = error "GHC shouldn't even let me write this combination of
 patterns, but the coverage checker tells me my pattern is non-exhaustive
 if I don't write it"
 index Nil (Fs _) = error "Ditto"
 index (Cons x _) Fz = x
 index (Cons _ xs) (Fs n) = index xs n
 }}}

 be rejected, and

 {{{
 index :: Vec n a -> Fin n -> a
 index Nil _ = error "damn!"
 index (Cons x _) Fz = x
 index (Cons _ xs) (Fs n) = index xs n
 }}}

 be accepted (that is, for a Nil in the Vec position, the only valid
 pattern for the Fin should be _ or a variable).

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