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
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@gmail.com