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: class CpsForm a b | a -> b instance CpsForm Bool Bool A natural formulation of the type of the CPS transformation would be cps :: CpsForm t cps_t => Term t -> (Term cps_t -> Term ()) -> Term () cps (B b) c = c (B b) -- doesn't type-check! cps (Cnd p q r) c = cps p (\p' -> Cnd p' (cps q c) (cps r c)) -- type-checks OK but the first clause of the function doesn't type-check: Couldn't match the rigid variable `cps_t' against `Bool' `cps_t' is bound by the type signature for `cps' Expected type: Term cps_t Inferred type: Term Bool In the application `B b' In the first argument of `c', namely `(B b)' On the contrary, if we push the (otherwise implicit) quantifier inside the parentheses: cps' :: Term t -> (forall cps_t . CpsForm t cps_t => Term cps_t -> Term ()) -> Term () cps' (B b) c = c (B b) -- type-checks OK cps' (Cnd p q r) c = cps' p (\p' -> Cnd p' (cps' q c) (cps' r c)) -- doesn't type-check! then the second clause fails to type-check: Couldn't match the rigid variable `cps_t' against `Bool' `cps_t' is bound by the polymorphic type `forall cps_t. (CpsForm t cps_t) => Term cps_t -> Term ()' Expected type: Term Bool Inferred type: Term cps_t In the first argument of `Cnd', namely `p'' In a lambda abstraction: \ p' -> Cnd p' (cps' q c) (cps' r c) This case seems to be an instance of a problem discussed earlier. (http://www.haskell.org/pipermail/haskell-cafe/2005-August/011053.html) Any suggestion on a way to get around this problem in current Haskell? And, any hope to get this fixed in a future release of GHC? Thanks Louis-Julien