{-# 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)

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 family Elem (x :: a) (xs :: [a]) :: Bool where
 Elem _ '[] = 'False
 Elem x (x ': _) = 'True
 Elem x (_ ': xs) = Elem x xs

data Proxy n = Proxy

data SumType (ls :: [*]) where
  SumType :: xs !! s ~ x => SNat s -> x -> Proxy xs -> SumType xs

type Eg = [Bool,Int,Bool]

eg1 :: SumType Eg
eg1 = SumType SZ False (Proxy :: Proxy Eg)

eg2 :: SumType Eg
eg2 = SumType (SS SZ) 1 (Proxy :: Proxy Eg)