Let's say we have some code like this, which typechecks just fine:
{-# LANGUAGE RankNTypes #-}
data Foo a
type A a = forall m. Monad m => Foo a -> m ()
type PA a = forall m. Monad m => Foo a -> m ()
type PPFA a = forall m. Monad m => Foo a -> m ()
_pfa :: PPFA a -> PA a
_pfa = _pfa
_pa :: PA a -> A a
_pa = _pa
_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x
main :: IO ()
main = putStrLn "yay"
We note that _pp x = _pa $ _pfa x is too verbose, and we try to replace it with _pp = _pa . _pfa. Suddenly the code doesn't typecheck anymore, failing with error messages similar to
• Couldn't match type ‘Foo a0 -> m0 ()’ with ‘PA a’
Expected type: (Foo a0 -> m0 ()) -> Foo a -> m ()
Actual type: PA a -> A a
I guess this is due to m in the definition of type aliases being forall'd — indeed, replacing m with some exact type fixes the issue. But the question is: why does forall break things in this case?
Bonus points for trying to figure out why replacing dummy recursive definitions of _pfa and _pa with usual _pfa = undefined results in GHC complaining about unification variables and impredicative polymorphism:
• Cannot instantiate unification variable ‘a0’
with a type involving foralls: PPFA a -> Foo a -> m ()
GHC doesn't yet support impredicative polymorphism
• In the expression: undefined
In an equation for ‘_pfa’: _pfa = undefined