[Haskell-cafe] function composition and Rank2Types

[Hage, J. (Jurriaan)]

If you turn on ImpredicativeTypes it does compile.

Jur


> On 3 Feb 2023, at 16:55, Olaf Klinke <olf at aatal-apotheke.de> 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.