Is it possible to write an injective function of type

hard :: (forall n . Maybe (f n)) -> Maybe (forall n . (f n))

as a total functional program -- that is, without using error, undefined, unsafeXXX, bottom, inexhaustive patterns, or any functions which don't terminate?

By parametricity, for any fixed f :: *->* the only total inhabitants of

(forall n . Maybe (f n))

will take one of two forms:

Nothing

Just z
  where
    z :: forall n . f n

Unfortunately any attempt to case on the Maybe will require choosing n first, so the types of the pattern variables inside the case branches will no longer be polymorphic in n. It seems like the language is missing some sort of construct for performing case-discrimination on a polymorphic type without instantiating the type.

By the way, writing a function in the opposite direction is easy:

easy :: Maybe (forall n . (f n)) -> (forall n . Maybe (f n))
easy Nothing  = Nothing
easy (Just x) = Just x
haskell types polymorphism
Edit
Report