Thomas Jäger
I believe there may be some nasty interactions with generalized newtype-deriving, since we can construct two Leibniz-equal types which are mapped to different types using fundeps:
class Foo a where foo :: forall f. f Int -> f a
instance Foo Int where foo = id
newtype Bar = Bar Int deriving Foo
I think this is where your example falls apart. The compiler cannot sensibly derive the instance of Foo for Bar. Why? Because, if written explicitly, its implementation would need to be something like instance Foo Bar where foo = fmap Bar but that is invalid, because the signature is different: foo :: forall f . Functor f => f Int -> f Bar As it happens, the compiler probably does derive some different code for 'foo', namely an unsafe coercion, but it is code that could not be written explicitly by the user. That is why you are able to reveal the coercion via some other route. Regards, Malcolm