Pull recent Hadrian changes from upstream
[ghc.git] / testsuite / tests / indexed-types / should_compile / T2219.hs
1 {-# LANGUAGE TypeFamilies, GADTs, EmptyDataDecls, TypeOperators #-}
2
3 module Test where
4
5 data Zero
6 data Succ a
7
8 data FZ
9 data FS fn
10
11 data Fin n fn where
12 FZ :: Fin (Succ n) FZ
13 FS :: Fin n fn -> Fin (Succ n) (FS fn)
14
15 data Nil
16 data a ::: b
17
18 type family Lookup ts fn :: *
19 type instance Lookup (t ::: ts) FZ = t
20 type instance Lookup (t ::: ts) (FS fn) = Lookup ts fn
21
22 data Tuple n ts where
23 Nil :: Tuple Zero Nil
24 (:::) :: t -> Tuple n ts -> Tuple (Succ n) (t ::: ts)
25
26 proj :: Fin n fn -> Tuple n ts -> Lookup ts fn
27 proj FZ (v ::: _) = v
28 proj (FS fn) (_ ::: vs) = proj fn vs