Is there a way to push foralls past constructors when sound?

Question

Suppose I have

data Foo p =
    NoFoo
  | YesFoo (forall a. p a)

I can write

fromFoo :: Foo p -> Maybe (p a)
fromFoo NoFoo = Nothing
fromFoo (YesFoo p) = Just p

It's also possible to go the other way:

toFoo :: forall p.
         (forall a. Maybe (p a))
      -> Foo p
toFoo m =
  case m :: Maybe (p ()) of
    Nothing -> NoFoo
    Just _ -> YesFoo (fromJust m)

The fromJust is disgusting! toFoo is actually total, because parametricity ensures that m @a behaves exactly the same as m @(), but this is gross. Is there any cleaner way?

Edit: rampion pointed out that this can be written more concisely, still with fromJust. I just realized it can be done a bit humorously, making fun of the newbies:

toFoo m
  | isNothing m = NoFoo
  | otherwise = YesFoo (fromJust m)

The only way I see to avoid creating a thunk to apply fromJust is by getting super-evil:

toFoo Nothing = NoFoo
toFoo (Just x) = YesFoo (unsafeCoerce# x)

Answer 1

The best I can come up with so far still uses fromJust, but it's simpler:

toFoo :: forall p.
         (forall a. Maybe (p a))
      -> Foo p
toFoo Nothing = NoFoo
toFoo m = YesFoo $ fromJust m