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

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

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

sZ :: SNat Z
sZ = case singInstance SZ of
       SingInstance -> SZ

sS :: SNat n -> SNat (S n)
sS n = case singInstance n of
         SingInstance -> SS n

--

class Sing n where
  sing :: SNat n

instance Sing Z where
  sing = SZ

instance Sing n => Sing (S n) where
  sing = SS sing

data SingInstance a where
  SingInstance :: Sing a => SingInstance a

singInstance :: SNat n -> SingInstance n
singInstance SZ = SingInstance
singInstance (SS n) =
    case singInstance n of
      SingInstance -> SingInstance

--

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)

type SumType (a :: [*]) = (n @ SNat,a !! n)