Embrace -XTypeInType, add -XStarIsType
[ghc.git] / testsuite / tests / indexed-types / should_fail / T7967.hs
1 {-# LANGUAGE TypeFamilies, DataKinds, TypeOperators, GADTs #-}
2 module T7967 where
3
4 import Data.Kind (Type)
5
6 data Nat = Zero | Succ Nat
7
8 data SNat :: Nat -> Type where
9 SZero :: SNat Zero
10 SSucc :: SNat n -> SNat (Succ n)
11
12 data HList :: [Type] -> Type where
13 HNil :: HList '[]
14 HCons :: h -> HList t -> HList (h ': t)
15
16 data Index :: Nat -> [Type] -> Type where
17 IZero :: Index Zero (h ': t)
18 ISucc :: Index n l -> Index (Succ n) (h ': l)
19
20 type family Lookup (n :: Nat) (l :: [Type]) :: Type
21 type instance Lookup Zero (h ': t) = h
22 type instance Lookup (Succ n) (h ': t) = Lookup n t
23
24 hLookup :: Index n l -> HList l -> Lookup n l
25 hLookup IZero (HCons h _) = h
26 hLookup (ISucc n) (HCons _ t) = hLookup n t
27 hLookup _ _ = undefined
28
29 -- So far, so good. But, I wanted a way to convert `SNat`s to `Index`es. When
30 -- I add the (wrong) code below, and got a bogus error above
31
32 sNatToIndex :: SNat n -> HList l -> Index n l
33 sNatToIndex SZero HNil = IZero