Just noticed Joost Visser's message but since I had (essentially a very similar) response I thought I might send it off as well ... It includes the conditional cases. Regards, -d {-# OPTIONS_GHC -fglasgow-exts #-} module Main where data Term a where Lit :: Int -> Term Int Inc :: Term Int -> Term Int IsZ :: Term Int -> Term Bool If :: Term Bool -> Term a -> Term a -> Term a Pair :: Term a -> Term b -> Term (a,b) Fst :: Term (a,b) -> Term a Snd :: Term (a,b) -> Term b data Expr = ELit Int | EInc Expr | EIsZ Expr | EPair Expr Expr | EIf Expr Expr Expr | EFst Expr | ESnd Expr deriving (Read,Show) -- Give a GADT for representation types data R a where Rint :: R Int Rbool :: R Bool Rpair :: R a -> R b -> R (a,b) -- Give an existential type with a type representation data TermEx where MkTerm :: R a -> Term a -> TermEx -- we use Weirich's higher-order type-safe cast to avoid deep traversals -- one can replace the type_cast with a more simple traversal-based -- version. data CL c a d = CL (c (d,a)) data CR c a d = CR (c (a,d)) type_cast :: forall a b c. R a -> R b -> c a -> c b type_cast Rint Rint x = x type_cast Rbool Rbool x = x type_cast (Rpair (ra::(R a0)) (rb::(R b0))) (Rpair (ra'::(R a0')) (rb'::(R b0'))) x = let g = (type_cast ra ra' :: ( (CL c b0) a0 -> (CL c b0) a0' )) h = (type_cast rb rb' :: ( (CR c a0') b0 -> (CR c a0') b0')) in case (g (CL x)) of CL x' -> case (h (CR x')) of CR y' -> y' type_cast _ _ _ = error "cannot cast!" -- give only the cases for Eif and Elit, the others are similar my_read :: Expr -> TermEx my_read (ELit i) = MkTerm Rint (Lit i); my_read (EIf p t e) = case (my_read p) of MkTerm rb b -> case rb of Rbool -> case (my_read t) of MkTerm r1 t1 -> case (my_read e) of MkTerm r2 t2 -> MkTerm r2 (If b (type_cast r1 r2 t1) t2) _ -> error "conditional not boolean!"