[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):

 Oh! I see the difference now!

 Matching on a GADT constructor introduces a type equality context on the
 matched variables, but doesn't refine them explicitly, as far as I can
 tell.

 To test this, in addition to the

 {{{
 test :: Fin Nz -> a
 test _ = undefined
 -- test Fz = undefined -- Rightfully rejected by GHC
 -- test (Fs n) = undefined -- Rightfully rejected by GHC
 }}}

 example above, I wrote the following:

 {{{
 test' :: (n ~ Nz) => Fin n -> a
 test' Fz = undefined
 test' (Fs n) = undefined
 }}}

 It seems like roughly the same thing as test, but GHC happily accepts the
 Fz and Fs constructors. I see now that that is what matching on Nil does
 in my original index function, so that is why the seemingly incompatible
 Fin constructors are accepted!

 Anyway, I promise I'll shut up about this now! It had just misunderstood
 how GADT matching actually refined the types. I'm putting this up here for
 the benefit of anyone else who might be interested and have the same
 confusion (a couple of people in the Haskell IRC channel expressed
 interest in my example). Sorry for the noise :)

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