Test.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE GADTs #-}
module Test where

data D :: * -> * -> * where
  Refl :: D a a

data T :: * -> * where
  Nil :: T a
  Cons :: (D a e) -> (e -> a) -> T a

newtype CpsT a = CpsT
  { runCpsT :: forall r .
      r ->                                   -- Nil
      (forall e . D a e -> (e -> a) -> r) -> -- Cons
        r }

uncps :: CpsT a -> T a
uncps p = runCpsT p Nil Cons

main = pure () :: IO ()

test.ml

type (_, _) d =
  Refl : ('a, 'a) d

type 'a t =
  | Nil
  | Cons : ('a, 'e) d * ('e -> 'a) -> 'a t

type 'a cps_t =
  < get : 'r .
    'r ->                                            (* Nil *)
    < get : 'e . ('a, 'e) d -> ('e -> 'a) -> 'r > -> (* Cons *)
      'r >

(* Error: The universal variable 'e would escape its scope *)
let uncps : type a . a cps_t -> a t =
  fun p -> p # get Nil (object method get d f = Cons (d, f) end)