Am Montag, den 07.11.2011, 14:49 +0200 schrieb Wolfgang Jeltsch:
Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagnerdm@seas.upenn.edu:
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)
[…]
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.
That’s the problem. I could have written the second type in the type signature, which would directly express my intension, but I didn’t, since GHC silently transforms it into the first type anyway.
The only way I know of to prevent this is to make a newtype "barrier".
This is what I already thought of worth trying.
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.)
I shouldn’t need impredicativity in the result, so I’ll try this route.
Yes, this works. Thank you. Best wishes, Wolfgang