
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

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
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
participants (1)
-
Vladimir Reshetnikov