1{-# LANGUAGE DataKinds      #-}
2{-# LANGUAGE GADTs          #-}
3{-# LANGUAGE KindSignatures #-}
4{-# LANGUAGE TypeOperators  #-}
5
6import Data.Kind
7
8data Nat = Z | S Nat
9
10data HList (ls :: [Type]) where
11  HNil :: HList '[]
12  HCons :: t -> HList ts -> HList (t ': ts)
13
14data ElemAt (n :: Nat) t (ts :: [Type]) where
15  AtZ :: ElemAt 'Z t (t ': ts)
16  AtS :: ElemAt k t ts -> ElemAt ('S k) t (u ': ts)
17
18lookMeUp :: ElemAt i ty tys -> HList tys -> ty
19lookMeUp = _
20
21