[GHC] #7293: Wrong location reported for inaccessible code with GADTs

[GHC]

#7293: Wrong location reported for inaccessible code with GADTs
------------------------------+---------------------------------------------
 Reporter:  goldfire          |          Owner:                  
     Type:  bug               |         Status:  new             
 Priority:  normal            |      Component:  Compiler        
  Version:  7.6.1             |       Keywords:  GADTs           
       Os:  Unknown/Multiple  |   Architecture:  Unknown/Multiple
  Failure:  None/Unknown      |       Testcase:                  
Blockedby:                    |       Blocking:                  
  Related:                    |  
------------------------------+---------------------------------------------
 Consider this code:

 {{{
 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
              TypeOperators #-}

 data Nat = Zero | Succ Nat

 data Vec :: * -> Nat -> * where
   Nil :: Vec a Zero
   Cons :: a -> Vec a n -> Vec a (Succ n)

 type family (m :: Nat) :< (n :: Nat) :: Bool
 type instance m :< Zero = False
 type instance Zero :< Succ n = True
 type instance Succ n :< Succ m = n :< m

 data SNat :: Nat -> * where
   SZero :: SNat Zero
   SSucc :: forall (n :: Nat) => SNat n -> SNat (Succ n)

 nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
 nth (Cons x _) SZero = x
 nth (Cons _ xs) (SSucc k) = nth xs k
 nth Nil _ = undefined
 }}}

 The pattern match on the last line is invalid and should indeed cause an
 error. However, the error is reported for the line declaring the type of
 {{{nth}}}, which is confusing. It seems the error should be reported at
 the location of the pattern match.

 Here is the error:

 {{{
 /Users/rae/temp/sing.hs:20:8:
     Couldn't match type 'False with 'True
     Inaccessible code in
       the type signature for
         nth :: (k :< n) ~ 'True => Vec a n -> SNat k -> a
 }}}

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