[Haskell-cafe] Re: Forall and type synonyms in GHC 7.0

[Bas van Dijk]

On Mon, Nov 1, 2010 at 4:30 AM, Mario Blažević <mblazevic at stilo.com> wrote:
>     Before uploading a new version of my project on Hackage, I decided to
> future-proof it against GHC 7.0. I ran into several compile errors caused by
> the changes in let generalization, but these were easy to fix by adding
> extra type annotations. But then I ran into another problem that I can't fix
> so easily. Here is its trimmed-down reproduction:
>
>> {-# LANGUAGE RankNTypes #-}
>>
>> module Test where
>>
>> data Component c = Component {with :: c}
>>
>> pair1 :: (Bool -> c1 -> c2 -> c3) -> Component c1 -> Component c2 ->
>> Component c3
>> pair1 combinator (Component c1) (Component c2) = Component (combinator
>> True c1 c2)
>>
>> type PairBinder m = forall x y r. (x -> y -> m r) -> m x -> m y -> m r
>>
>> pair2 :: Monad m => (PairBinder m -> c1 -> c2 -> c3) -> Component c1 ->
>> Component c2 -> Component c3
>> pair2 combinator = pair1 (combinator . chooseBinder)
>>
>> chooseBinder :: Monad m => Bool -> PairBinder m
>> chooseBinder right = if right then rightBinder else leftBinder
>>
>> leftBinder :: Monad m => PairBinder m
>> leftBinder f mx my = do {x <- mx; y <- my; f x y}
>>
>> rightBinder :: Monad m => PairBinder m
>> rightBinder f mx my = do {y <- my; x <- mx; f x y}
>
>    The general idea here, if you're intrigued, is that pair1 belongs to a
> generic module that packages things it knows nothing about into Components.
> The remaining definitions belong to a client of the generic module, and
> pair2 is a specialization of pair1 to components that have something to do
> with monads.
>
>    Now this little test compiles fine with GHC 6.12.1, but GHC
> 7.0.0.20101029 reports the following error in the pair2 definition:
>
> TestForall.lhs:13:42:
>     Couldn't match expected type `forall x y r.
>                                   (x -> y -> m r) -> m x -> m y -> m r'
>                 with actual type `(x -> y -> m1 r) -> m1 x -> m1 y -> m1 r'
>     Expected type: Bool -> PairBinder m
>       Actual type: Bool -> (x -> y -> m1 r) -> m1 x -> m1 y -> m1 r
>     In the second argument of `(.)', namely `chooseBinder'
>     In the first argument of `pair1', namely
>       `(combinator . chooseBinder)'
>
>     I've tried adding extra type annotations without making any progress. At
> this point I'm beginning to suspect I ran into a bug in GHC 7.0, but I can't
> find it in GHC Trac; the only ticket that looks similar is #4347, but that
> one works for me. Is this a bug? If not, how do I make my code compile?
>
>
> _______________________________________________
> Glasgow-haskell-users mailing list
> Glasgow-haskell-users at haskell.org
> http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
>
>

I had the exact same problem in my regional-pointers package in the
withArray function:

withArray ∷ (Storable α, MonadCatchIO pr)
          ⇒ [α]
          → (∀ s. RegionalPtr α (RegionT s pr) → RegionT s pr β)
          → pr β

 I had to replace the original:

withArray vals = withArrayLen vals ∘ const

with:

withArray vals f = withArrayLen vals $ \_ → f

where:

withArrayLen ∷ (Storable α, MonadCatchIO pr)
            ⇒ [α]
            → (∀ s. Int → RegionalPtr α (RegionT s pr) → RegionT s pr β)
            → pr β

So unfortunately you gave to inline the function composition:

pair2 combinator = pair1 $ \b -> combinator (chooseBinder b)

Note that in the other thread I'm describing a similar problem in my
usb-safe package. Where in essence the problem is that the following
won't type check:

foo :: (forall s. ST s a) -> a
foo st = ($) runST st

but the following will:

foo :: (forall s. ST s a) -> a
foo st = runST st

and surprisingly the following will also type check:

foo :: (forall s. ST s a) -> a
foo st = runST $ st

Regards,

Bas