Re: problems with impredicativity

Quoting wagnerdm@seas.upenn.edu:

Quoting Wolfgang Jeltsch :

...

this code is accepted by GHC 7.0.4: <snip> However, this one isn?t:

...

{-# LANGUAGE ImpredicativeTypes #-}

polyId :: (forall a. Maybe a) -> Maybe a polyId x = x

polyIdMap :: [forall a. Maybe a] -> [forall a. Maybe a] polyIdMap xs = fmap polyId xs

Is there a way to make it accepted?

Yep, fix the type signature. There is no type you can substitute for "a" in "Maybe a" that results in "forall a. Maybe a". But GHC accepts the same code with the following type signature, which should make clear what I mean:

polyIdMap :: [forall a. Maybe a] -> [Maybe (forall a. a)]

It occurred to me that you may have been attempting to do something else, so perhaps I fired off my first reply too quickly. Another interpretation is that the type of polyIdMap is correct, but the type of polyId isn't. The first thing to observe is that, ideally, the following two types would mean slightly different things: polyId :: forall b. (forall a. Maybe a) -> Maybe b polyId :: (forall a. Maybe a) -> (forall b. Maybe b) The first means: first, choose a monomorphic type, then specialize the first argument to that monomorphic type. The second means: take a polymorphic value, then return it, delaying the choice of a monomorphic type until later. (And, again ideally, any unbound variables would implicitly put their "forall" at the top level, as in the first signature above.) If this distinction existed, then your polyIdMap would be fully compatible with a polyId having the second type signature. Unfortunately, in GHC, these two types do not mean different things: "forall"s on the result side of an arrow are silently floated to the top level, even if you explicitly choose to put them later in your type annotation. The only way I know of to prevent this is to make a newtype "barrier". For example, the following works: newtype PolyMaybe = PolyMaybe (forall a. Maybe a) polyId :: PolyMaybe -> PolyMaybe polyId x = x polyIdMap :: [PolyMaybe] -> [PolyMaybe] polyIdMap xs = fmap polyId xs Then, later, you can unwrap the PolyMaybe -- but only when you're ready to turn it into a monomorphic Maybe! (Note that none of these things is using ImpredicativeTypes, which is what made me jump to my first, probably mistaken impression of what you were trying to do. Rank2Types is enough for the above to compile.) ~d