I'm not sure if this answers your questions, but I think this particular problem has a cleaner solution with GADTs:

    {-# LANGUAGE GADTs #-}

    

    data Cmd s t where

      Push :: a             -> Cmd s         (a,s)

      F1   :: (a -> b)      -> Cmd (a,s)     (b,s)

      F2   :: (a -> b -> c) -> Cmd (a,(b,s)) (c,s)

    

    data Prog s t where

      (:.) :: Cmd s t -> Prog t u -> Prog s u

      End  :: Prog s s

    

    infixr 5 :.

    

    cmd :: Cmd s t -> s -> t

    cmd (Push a) s         = (a, s)

    cmd (F1 f)   (a,s)     = (f a, s)

    cmd (F2 f)   (a,(b,s)) = (f a b, s)

    

    prog :: Prog s t -> s -> t

    prog (c :. p) s = prog p (cmd c s)

    prog End      s = s

    

    run :: Prog () t -> t

    run p = prog p ()

Then from GHCi:

    

    > run (Push 3 :. Push 4 :. F2 (+) :. F1 show :. End)

    ("7",())

Maybe you really want GADTs? :)

-Eric