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

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

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 Proxy n = Proxy
type SumType (xs :: [*]) = forall x (n::Nat). xs !! n ~ x => (Proxy n,x)

type Eg = [Bool,Int,Bool]

eg :: SumType Eg
eg = (Proxy :: Proxy Z,False)

{-

    * Could not deduce: n ~ 'Z
      from the context: (Eg !! n) ~ x
        bound by the type signature for:
                   eg :: SumType Eg
      `n' is a rigid type variable bound by
        the type signature for:
          eg :: SumType Eg
      Expected type: Proxy n
        Actual type: Proxy 'Z
    * In the expression: Proxy :: Proxy Z
      In the expression: (Proxy :: Proxy Z, False)
      In an equation for `eg': eg = (Proxy :: Proxy Z, False)
    * Relevant bindings include
        eg :: (Proxy n, x)
   |
   | eg = (Proxy :: Proxy Z,False)
   |       ^^^^^^^^^^^^^^^^

    * Could not deduce: x ~ Bool
      from the context: (Eg !! n) ~ x
        bound by the type signature for:
                   eg :: SumType Eg
      `x' is a rigid type variable bound by
        the type signature for:
          eg :: SumType Eg
    * In the expression: False
      In the expression: (Proxy :: Proxy Z, False)
      In an equation for `eg': eg = (Proxy :: Proxy Z, False)
    * Relevant bindings include
        eg :: (Proxy n, x)
   |
   | eg = (Proxy :: Proxy Z,False)
   |                        ^^^^^
-}