[Haskell-cafe] function composition and Rank2Types

[Brandon Allbery]

What you're trying to do requires impredicative types. ($) is
special-cased to support them; (.) isn't.

On Fri, Feb 3, 2023 at 11:55 AM 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.



-- 
brandon s allbery kf8nh
allbery.b at gmail.com