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 |