Modify a couple of error messages slightly
[ghc.git] / testsuite / tests / gadt / T7294.hs
1 {-# OPTIONS_GHC -fdefer-type-errors #-}
2 {-# LANGUAGE GADTs, DataKinds, KindSignatures, TypeFamilies,
3 TypeOperators, RankNTypes #-}
4
5 module T7294 where
6
7 data Nat = Zero | Succ Nat
8
9 data Vec :: * -> Nat -> * where
10 Nil :: Vec a Zero
11 Cons :: a -> Vec a n -> Vec a (Succ n)
12
13 type family (m :: Nat) :< (n :: Nat) :: Bool
14 type instance m :< Zero = False
15 type instance Zero :< Succ n = True
16 type instance Succ n :< Succ m = n :< m
17
18 data SNat :: Nat -> * where
19 SZero :: SNat Zero
20 SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
21
22 nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
23 nth (Cons x _) SZero = x
24 nth (Cons _ xs) (SSucc k) = nth xs k
25 nth Nil _ = undefined