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

data Nat = Z | S Nat
           deriving (Show, Eq, Ord)

data SNat (n :: Nat) where
  SZ :: SNat Z
  SS :: SNat n -> SNat (S n)

--

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

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

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

--

data StateN (xs :: [* -> * -> *]) s a where
  StateN :: xs !! n ~ x => (s -> (SNat n,x s a)) -> StateN xs s a

newtype StackS   s a = StackS  {runStackS   :: Maybe (a,s) }
newtype LinearS  s a = LinearS {runLinearS  :: (a,Maybe s) }

eg :: (Int,Int) -> StateN '[LinearS,StackS] (Int,Int) Int
eg (nT,mT) = StateN (\(i,j) -> case (i,j) of
              (0,_) -> (SS SZ,StackS Nothing)
              (n,1) -> (SZ,LinearS (n+1,Nothing))
              (n,m) -> (SZ,LinearS (n+m,Just (n,m-1)))
            )
-- this gives type errors as the different cases return different types.