Composition of functions for all types

Question

Let's say we have a code that looks like this:

{-# 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" 

Note that _pp x = _pa $ _pfa x too verbose, and we are trying to replace it with _pp = _pa . _pfa _pp = _pa . _pfa . Suddenly the code is no longer checked by typecheck, otherwise 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 assume this is due to m in the definition of aliases of type forall - indeed, replacing m with some exact type fixes the problem. But the question is: why does forall break things in this case?

Bonus points for trying to figure out why replacing the dummy recursive definitions of _pfa and _pa with the usual _pfa = undefined results in the GHC complaining about unification variables and non-discriminatory 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 

Answer 1

Just to be clear when you write:

 _pa :: PA a -> A a 

The compiler expands type synonyms, and then moves the quantifiers and constraints up, for example:

 _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 polymorphic type of rank-2, because it has an arrow built into the left side of the function. The same goes for _pfa . They consider polymorphic functions to be arguments.

To answer the real question, I will first show you something strange. Both typecheck types:

 _pp :: PPFA a -> A a _pp x = _pa $ _pfa x _pp :: PPFA a -> A a _pp x = _pa (_pfa x) 

This, however, does not mean:

 apply :: (a -> b) -> a -> b apply fx = fx _pp :: PPFA a -> A a _pp x = apply _pa (_pfa x) 

Unintuitive, right? This is because the application operator ($) has a special wrapper in the compiler to allow you to instantiate your type variables with polymorphic types, to support runST $ do { … } rather than runST (do { … }) .

The composition (.) , However, does not have a special cover. Therefore, when you call (.) On _pa and _pfa , it first creates its types. So you are trying to pass a non-polymorphic result _pfa type (Foo a0 -> m0 ()) -> Foo a -> m () mentioned in your error message to the _pa function, but it expects a polymorphic argument of type _pa , so you get a join error.

undefined :: a does not typecheck because it is trying to create an instance of a with a polymorphic type, an example of unproductive polymorphism. This is a hint of what you should do - the standard way to hide consistency - with the 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 errors:

 _pp :: PPFA a -> A a _pp = _pa . _pfa 

With a cost that you need to explicitly wrap and deploy to tell the GHC when to abstract and instantiate:

 _pa :: PA a -> A a _pa x = A (unPA x) 

Answer 2

The initiation of polymorphic type variables with polymorphic types is called impressive polymorphism. - GHC User Guide

As the error message indicates, the GHC only allows you to create a type variable with a monomorphic type of rank 0. My assumption is that type checking with nonspecific polymorphism is more difficult to implement than it might seem.