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.reshetni...@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 > _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe