継続操作を持つ言語をHaskell上で実装したい(1)

(そもそもEDSLって言うのかなぁ)
(DomainにSpecificじゃないですし、なんというか、簡単な言語をHaskell上で表現する、encode、まぁ埋め込むでも良いんですがなんと言えばしっくりくるのか)

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ScopedTypeVariables #-}

data Exp t where
    EInt :: Int -> Exp Int
    ELam :: (Exp a -> Exp b) -> Exp (a -> b)
    EApp :: Exp (a -> b) -> Exp a -> Exp b
    Cop :: Exp ((a -> b) -> b) -> Exp a -- Felleisen's C Operator

e1 :: Exp Int
e1 = EInt 1

e2 :: Exp (Int -> Int)
e2 = ELam (\(EInt x) -> EInt (x + 1))

e3 :: Exp Int
e3 = EApp e2 e1

e4 :: Exp Int
e4 = EApp e2 (Cop (ELam (\k -> EApp k (EInt 2))))

exit :: Exp (a -> b)
exit = ELam exit'
    where
      exit' :: Exp a -> Exp b
      exit' v = error "exit"

{-

eval e1 exit
eval e2 exit
eval e3 exit
eval e4 exit

としたい。

-}

eval :: Exp t -> Exp (t -> r) -> Exp r
eval (EApp (f :: Exp (a -> t)) (arg :: Exp a) :: Exp t) (ELam k :: Exp (t -> r)) = v
    where
      k' :: Exp t -> Exp r
      k' = k

      k1_body :: Exp (a -> t) -> Exp r
      k1_body = (\(f' :: Exp (a -> t)) -> case f' of
                                            ELam f'' -> k2_body f''
                )

      k2_body :: (Exp a -> Exp t) -> Exp r
      k2_body f'' = eval arg (ELam (\(arg' :: Exp a) -> k' (f'' arg')))

      k1 :: Exp ((a -> t) -> r)
      k1 = ELam k1_body

      v :: Exp r
      v = eval f k1

eval (Cop (ELam catcher :: Exp ((t -> h) -> h)) :: Exp t) (ELam k :: Exp (t -> r)) = undefined
    where
      catcher' :: Exp (t -> h) -> Exp h
      catcher' = catcher

      -- No!!
      app = catcher' (ELam k)

とりあえず、継続操作で型が二重否定除去なソレを載せてみるも、こいつの型変数bが隠れちゃうので大変ですよっていうので、さてどうする?とかで考えててうまい具合にどうすれば良いのか分からないので困ってます。

頭良い人やってください...

最もシンプルぽい形のものを載せておこう・・・。