It appears, as far as I can tell, that GHC can't move a forall past an -> with coerce. I was playing around with the MonadTrans instance for Codensity, wanting (essentially) to write lift = coerce (>>=) This is legal: instance MonadTrans Codensity where lift = frob frob :: forall m a . Monad m => m a -> Codensity m a frob = coerce (blah (Mag (>>=)) :: m a -> Mag2 m a) newtype Mag m a = Mag (forall b . m a -> (a -> m b) -> m b) newtype Mag2 m a = Mag2 (forall b . (a -> m b) -> m b) blah :: Mag m a -> m a -> Mag2 m a blah (Mag p) q = Mag2 (p q) The problem is that there doesn't *seem* to be a way to implement blah as a coercion. GHC doesn't recognize that Mag m a has the same representation as m a -> Mag2 m a The essential difference, as far as I can see, is that the `forall b` is shifted across `m a ->`. It seems that this really shouldn't be an issue, because 1. b is not free in `m a` 2. Type lambdas all compile away Would it be worth trying to extend the Coercible mechanism to deal with these kinds of situations? Or is there already some way to do it that I've missed? David