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
Just to be clear, when you write:
_pa :: PA a -> A a
The compiler expands the type synonyms and then moves the quantifiers and constraints upward, like so:
_pa
:: forall a.
(forall m1. Monad m1 => Foo a -> m1 ())
-> (forall m2. Monad m2 => Foo a -> m2 ())
_pa
:: forall m2 a. (Monad m2)
=> (forall m1. Monad m1 => Foo a -> m1 ())
-> Foo a -> m2 ()
So _pa has a rank-2 polymorphic type, because it has a forall nested to the left of a function arrow. Same goes for _pfa. They expect polymorphic functions as arguments.
To answer the actual question, I’ll first show you something strange. These both typecheck:
_pp :: PPFA a -> A a
_pp x = _pa $ _pfa x
_pp :: PPFA a -> A a
_pp x = _pa (_pfa x)
This, however, does not:
apply :: (a -> b) -> a -> b
apply f x = f x
_pp :: PPFA a -> A a
_pp x = apply _pa (_pfa x)
Unintuitive, right? This is because the application operator ($) is special-cased in the compiler to allow instantiating its type variables with polymorphic types, in order to support runST $ do { … } rather than runST (do { … }).
Composition (.), however, is not special-cased. So when you call (.) on _pa and _pfa, it instantiates their types first. Thus you end up trying to pass the non-polymorphic result of _pfa, of the type (Foo a0 -> m0 ()) -> Foo a -> m () mentioned in your error message, to the function _pa, but it expects a polymorphic argument of type P a, so you get a unification error.
undefined :: a doesn’t typecheck because it tries to instantiate a with a polymorphic type, an instance of impredicative polymorphism. That’s a hint as to what you should do—the standard way of hiding impredicativity is with a newtype wrapper:
newtype A a = A { unA :: forall m. Monad m => Foo a -> m () }
newtype PA a = PA { unPA :: forall m. Monad m => Foo a -> m () }
newtype PPFA a = PPFA { unPPFA :: forall m. Monad m => Foo a -> m () }
Now this definition compiles without error:
_pp :: PPFA a -> A a
_pp = _pa . _pfa
With the cost that you need to explicitly wrap and unwrap to tell GHC when to abstract and instantiate:
_pa :: PA a -> A a
_pa x = A (unPA x)