Wrong location reported for inaccessible code with GADTs

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

Trac metadata

Trac field	Value
Version	7.6.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture