Embrace -XTypeInType, add -XStarIsType
[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 import Data.Kind (Type)
8
9 data Nat = Zero | Succ Nat
10
11 data Vec :: Type -> Nat -> Type where
12 Nil :: Vec a Zero
13 Cons :: a -> Vec a n -> Vec a (Succ n)
14
15 type family (m :: Nat) :< (n :: Nat) :: Bool
16 type instance m :< Zero = False
17 type instance Zero :< Succ n = True
18 type instance Succ n :< Succ m = n :< m
19
20 data SNat :: Nat -> Type where
21 SZero :: SNat Zero
22 SSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
23
24 nth :: ((k :< n) ~ True) => Vec a n -> SNat k -> a
25 nth (Cons x _) SZero = x
26 nth (Cons _ xs) (SSucc k) = nth xs k
27 nth Nil _ = undefined