Fwd: Unification for rank-N types

[Vladimir Reshetnikov]

Forwarding to GH list.

---------- Forwarded message ----------
From: Vladimir Reshetnikov <v.reshetnikov at gmail.com>
Date: Tue, 9 Jun 2009 16:51:59 +0500
Subject: Re: Unification for rank-N types
To: haskell-cafe <haskell-cafe at haskell.org>

One more example:

This does not type-check:
-------------------------------------------------------
{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

f :: [forall a. t a -> t a] -> t b -> t b
f = foldr (.) id
-------------------------------------------------------

    Couldn't match expected type `forall a. f a -> f a'
           against inferred type `b -> c'
    In the first argument of `foldr', namely `(.)'

But this, very similar, does type-check:
-------------------------------------------------------
{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

f :: [forall a. t a -> t a] -> t b -> t b
f = foldr (\g -> (.) g) id
-------------------------------------------------------

What is the reason for this?

Thanks,
Vladimir


On 6/9/09, Vladimir Reshetnikov <v.reshetnikov at gmail.com> wrote:
> Hi,
>
> I have the following code:
> -------------------------------------------------------
> {-# LANGUAGE RankNTypes #-}
>
> f :: ((forall a. a -> a) -> b) -> b
> f x = x id
>
> g :: (forall c. Eq c => [c] -> [c]) -> ([Bool],[Int])
> g y = (y [True], y [1])
>
> h :: ([Bool],[Int])
> h = f g
> -------------------------------------------------------
>
> GHC rejects it:
>     Couldn't match expected type `forall a. a -> a'
>            against inferred type `forall c. (Eq c) => [c] -> [c]'
>       Expected type: forall a. a -> a
>       Inferred type: forall c. (Eq c) => [c] -> [c]
>     In the first argument of `f', namely `g'
>     In the expression: f g
>
> But, intuitively, this code is type-safe, and actually I can convince
> the typechecker in it with the following workaround:
> -------------------------------------------------------
> h :: ([Bool],[Int])
> h = let g' = (\(x :: forall a. a -> a) -> g x) in f g'
> -------------------------------------------------------
>
> So, is the current behavior of GHC correct ot it is a bug?
> How unification for rank-N types should proceed?
>
> Thanks,
> Vladimir
>