#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
