Typed lambda calculus interpreter

interp.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}

data VarKind t = Bound | Free t

data RecArg (f :: k -> *) (v :: VarKind k) where
  BoundArg :: RecArg f 'Bound
  FreeArg :: f t -> RecArg f ('Free t) 

data RecRes b (g :: k -> *) (v :: VarKind k) where
  BoundRes :: b -> RecRes b g 'Bound
  FreeRes :: g t -> RecRes b g ('Free t)

unfree :: RecRes b g ('Free t) -> g t
unfree (FreeRes x) = x

unbound :: RecRes b g 'Bound -> b
unbound (BoundRes b) = b

data Expr :: * -> (k -> *) -> (k -> *) -> * where
  Literal :: a -> Expr a f g
  Var     :: f t -> Expr (g t) f g
  Cast    :: (b -> a) -> Expr b f g -> Expr a f g
  Lambda  :: Expr a (RecArg f) (RecRes b g) -> Expr (b -> a) f g
  App     :: Expr (b -> a) f g -> Expr b f g -> Expr a f g

bound :: Expr b (RecArg f) (RecRes b g)
bound = Cast unbound $ Var BoundArg

raise :: Expr a f g -> Expr a (RecArg f) (RecRes b g)
raise (Literal a) = Literal a
raise (Var t) = Cast unfree (Var (FreeArg t))
raise (Cast f e) = Cast f (raise e)
raise (App f x) = App (raise f) (raise x)
raise (Lambda e) = _
  where e' = raise e

evaluate :: forall a f g. (forall t. f t -> g t) -> Expr a f g -> a
evaluate _ (Literal a) = a
evaluate f (Var x) = f x
evaluate f (Cast g e) = g (evaluate f e)
evaluate f (App e1 e2) = evaluate f e1 (evaluate f e2)
evaluate f (Lambda t) = \b -> evaluate (raiseF b) t
  where raiseF :: forall b t. b -> RecArg f t -> RecRes b g t
        raiseF b BoundArg = BoundRes b
        raiseF _ (FreeArg t) = FreeRes (f t)

This is a learning exercise for me, but I can't figure out how to implement raise.