{-# LANGUAGE GADTs, TypeOperators, KindSignatures, DataKinds #-}
data (a :: *) :== b where Refl :: a :== a

data List a where {
Nil :: List a ;
(:::) :: a -> List a -> List a
}

infixr 5 :::

data Exists b c where {
Here :: a :== b -> Exists a (b ::: c);
There :: Exists a c -> Exists a (b ::: c)
}

sample :: Exists Int (String ::: Int ::: Char ::: Nil)
sample = There (Here Refl)

ghcの型システムの上でそれっぽいものは作れるようだけど