import Data.Type.Index
data Sum :: [Type] -> Type where
  L :: x -> Sum (x : xs)
  R :: Sum xs -> Sum (x : xs)


inj :: (Elem xs x) => x -> Sum xs
inj = inj' elemIndex


inj' :: Index xs x -> x -> Sum xs
inj' = \case
  IZ   -> L
  IS x -> R . inj' x

class Proj x xs where
  proj :: Proxy x -> Sum xs -> Maybe x

instance Proj x (x:xs) where
  proj _ (L x) = Just x
  proj _ _     = Nothing

instance Proj x ys => Proj x (y:ys) where
  proj p (R ys) = proj p ys

data FList f xs where
  FNil :: FList f '[]
  (:<) :: Typeable x => f x -> FList f xs -> FList f (x : xs)

newtype Rev b a = Rev (a -> b)

elim :: FList (Rev a) xs -> Sum xs -> a
elim (Rev f :< fs) (L x)  = f x
elim (_ :< fs)     (R xs) = elim fs xs

infixr 5 :<

test, test1 :: Sum [Int, Double, Maybe String]
test = inj (3 :: Int)
test1 = inj (Just "fooobar")

f = (Rev show :< Rev show :< Rev show :< FNil)
res = (elim f test1, elim f test)