problems with impredicativity

[Wolfgang Jeltsch]

Am Freitag, den 04.11.2011, 20:16 -0400 schrieb wagnerdm at seas.upenn.edu:
> Quoting wagnerdm at seas.upenn.edu:
> 
> > Quoting Wolfgang Jeltsch <g9ks157k at acme.softbase.org>:
> >
> >> 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?
>
> […]
> 
> 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.

> ~d

Best wishes,
Wolfgang