{-# Language
 DataKinds,
 TypeOperators,
 PolyKinds,
 TypeFamilies,
 UndecidableInstances
#-}

data N = Z | S N

type family Head (xs :: [a]) :: a where
 Head (x ': xs) = x

type family Drop (n :: N) (xs :: [a]) :: [a] where
 Drop (S n) (x ': xs) = Drop n xs
 Drop Z xs = xs

type family (!!) (xs :: [a]) (n :: N) :: a where
 (!!) xs n = Head (Drop n xs)

type StateN (a :: [*]) s = s -> (a !! n,s)
-- obviously wrong, how does it use n?
-- it seems like its trying to emulate a Sum datatype using a type level list,
-- the Nat then is like the constructor for the corresponding position in the Sum type..

eg :: StateN '[Bool,Int,Bool] Int
eg = undefined