[Haskell] Functional dependencies and type inference (2)

[Louis-Julien Guillemette]

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