#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 _______________________________________________ Glasgow-haskell-bugs mailing list Glasgow-haskell-bugs@haskell.org http://www.haskell.org/mailman/listinfo/glasgow-haskell-bugs