typed trans

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.