Louis-Julien Guillemette wrote:

Say we are using a GADT to represent a simple language of boolean constants and conditionals,

data Term a where B :: Bool -> Term Bool Cnd :: Term Bool -> Term t -> Term t -> Term t

and we would like to perform a type-safe CPS conversion over this language. We encode the relationship between the types in the source language and those in the CPS-converted language using a class and a fundep:

Here's the code that seems to do what you wished. Liberty is taken to extend the language so we can CPS convert more interesting terms. Here are the tests

term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False) test1 = shw (cps term1 id) ""

*CPS> test1 "Cnd (B True)(Cnd (B False)(B True)(B False))(Cnd (B False)(B True)(B False))"

term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3)) (B True) (Cmp (B True) (B False)) test2 = shw (cps term2 id) ""

*CPS> test2 "Cnd (B True)(Cnd (Cmp (I 1)(I 3))(B True)(Cmp (B True)(B False))) (Cnd (Cmp (I 2)(I 3))(B True)(Cmp (B True)(B False)))" The code: {-# OPTIONS -fglasgow-exts #-} {-# OPTIONS -fallow-undecidable-instances #-} module CPS where data Term a where B :: Bool -> Term Bool Cnd :: Term Bool -> Term t -> Term t -> Term t I :: Int -> Term Int Cmp :: Term t -> Term t -> Term Bool -- Note the polymorphic answertype class CpsForm t cps_t | t -> cps_t where cps :: Term t -> (Term cps_t -> Term w) -> Term w instance CpsForm t t where cps (B b) c = c (B b) cps (I b) c = c (I b) cps (Cnd p q r) c = cps p (\p' -> Cnd p' (cps q c) (cps r c)) cps (Cmp p q) c = cps p (\p' -> cps q (\q' -> c (Cmp p' q'))) shw:: Term t -> String -> String shw (B t) = ("B "++) . shows t shw (I t) = ("I "++) . shows t shw (Cnd p q r) = ("Cnd "++) . (showParen True (shw p)) . (showParen True (shw q)) . (showParen True (shw r)) shw (Cmp p q) = ("Cmp "++) . (showParen True (shw p)) . (showParen True (shw q)) term1 = Cnd (Cnd (B True) (B False) (B False)) (B True) (B False) test1 = shw (cps term1 id) "" term2 = Cnd (Cmp (Cnd (B True) (I 1) (I 2)) (I 3)) (B True) (Cmp (B True) (B False)) test2 = shw (cps term2 id) ""