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