> as an exercise, you can try to figure out the implementation

.. time is up :-P

Here is an answer for slightly more generic Proxy and f:

data Proxy a = Proxy a

exProxy::Functor f =>

f (Proxy a) -> f a

exProxy = (un1 <$>)

where un1 (Proxy a1) = a1