problems with impredicativity

[Wolfgang Jeltsch]

Am Montag, den 07.11.2011, 14:49 +0200 schrieb Wolfgang Jeltsch:
> Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagnerdm at 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