The question can be reduced to the following one: can we write a function that moves foralls in the following way?
suicidal :: f (forall n. n) -> forall n. f n
After all, if we can do that, then the rest is easy with a few impredicative types:
hard' :: Maybe (f (forall n. n)) -> Maybe (forall n. f n)
hard' Nothing = Nothing
hard' (Just x) = Just (suicidal x)
hard :: (forall n. Maybe (f n)) -> Maybe (forall n. f n)
hard x = hard' x -- instantiate 'n' at type 'forall n. n', thank goodness for impredicativity!
(If you want to try this in GHC, be sure to define a newtype like
newtype Forall f = Forall { unForall :: forall n. f n }
since otherwise GHC likes to float forall
s to the front of arrows and screw you over.)
But the answer to whether we can write suicidal
is clear: No, we can't! At least, not in a way that's parametric over f
. The solution would have to look something like this:
suicidal x = /\ n. {- ... -}
...and then we'd have to walk over the "structure" of f
, finding "places" where there were type functions, and applying them to the n
we now have available. The answer for the original question about hard
turns out to be the same: we can write hard
for any particular f
, but not parametrically over all f
.
By the way, I'm not convinced that what you said about parametricity is quite right:
By parametricity, for any fixed f :: *->*
the only total inhabitants of (forall n . Maybe (f n))
will take one of two forms: Nothing
or Just z
where z :: forall n . f n
.
Actually, I think what you get is that the inhabitants are (observationally equivalent to) one of two forms:
/\ n. Nothing
/\ n. Just z
...where the z
above is not polymorphic: it has the particular type f n
. (Note: no hidden forall
s there.) That is, the possible terms of the latter form depend on f
! This is why we can't write the function parametrically with respect to f
.
edit: By the way, if we allow ourselves a Functor
instance for f
, then things are of course easier.
notSuicidal :: (forall a b. (a -> b) -> (f a -> f b)) -> f (forall n. n) -> forall n. f n
notSuicidal fmap structure = /\ n. fmap (\v -> v [n]) structure
...but that's cheating, not least because I have no idea how to translate that to Haskell. ;-)