Re: [Haskell-cafe] function composition and Rank2Types

If you turn on ImpredicativeTypes it does compile. Jur

On 3 Feb 2023, at 16:55, Olaf Klinke wrote:

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

_______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.