Forall and type synonyms in GHC 7.0
Bas van Dijk
v.dijk.bas at gmail.com
Mon Nov 1 02:20:01 EDT 2010
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
More information about the Glasgow-haskell-users
mailing list