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