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 foos 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.
