problems with impredicativity

[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?
>
> 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