[Haskell-cafe] function composition and Rank2Types

[Olaf Klinke]

Dear Cafe, 

I used to believe that
   f . g $ x
is equivalent to 
   f $ g x
but apparently that is not the case when rank-2 types are involved.
Counterexample:

{-# LANGUAGE RankNTypes #-}
type Cont = forall r. (() -> r) -> r
data Foo = Foo Cont

mkCont :: () -> Cont
mkCont x = \f -> f x

foo1 :: () -> Foo
foo1 x = Foo $ mkCont x

foo2 :: () -> Foo
foo2 x = Foo . mkCont $ x

The function foo1 type-checks, the function foo2 doesn't. And that is
although ghci tells me that
mkCont :: () -> Cont
Foo    :: Cont -> Foo
so I should be able to compose? What is going on here? GHC 9.0.2 errors
with  
    • Couldn't match type ‘b0’ with ‘Cont’
      Expected: b0 -> Foo
        Actual: Cont -> Foo
      Cannot instantiate unification variable ‘b0’
      with a type involving polytypes: Cont
    • In the first argument of ‘(.)’, namely ‘Foo’
      In the expression: Foo . mkCont
and GHC 8.8.4 errors with
    • Couldn't match type ‘(() -> r0) -> r0’ with ‘Cont’
      Expected type: ((() -> r0) -> r0) -> Foo
        Actual type: Cont -> Foo
    • In the first argument of ‘(.)’, namely ‘Foo’
      In the expression: Foo . mkCont

The latter suggests that r is unnecessarily specialized to some
specific-yet-unknown r0 which destroys the universal quantification. 

Olaf