The problem with a typed preserving translation in the presence of functional dependencies is illustrated by Martin Sulzmann's ''critical example'':
{{{
class C a b | a -> b
instance C Int Bool

class D a where
  foo :: C a b => a -> b
instance D Int where
  foo _ = False
}}}
The straight forward translation is as follows:
{{{
data C a b = MkC
dC_Int_Bool = MkC

data D a = MkD {foo :: forall b. C a b -> a -> b}
dD_Int = MkD {foo = \_ -> False}
}}}
The translated program is not type correct (as `b` is universally quantified in `foo`s signature).  In the source, however, the functional dependency instantiates `b` to `Bool` in the `D Int` instance.

GHC currently circumvents the problem by rejecting the source program.