> I just found out that it *is* possible to implement the inside function,
> namely as follows:
>
> > inside :: forall t. ((forall a. Wrapper (t a))-> Wrapper (forall a. (t
> > a)))
> > inside x = Wrapper f
> > where f :: forall a. (t a)
> > f = unwrap x
> > unwrap (Wrapper z) = z
>
> I guess this solves my problem. Sorry for bothering you with this question.
> I still find it a bit weird to write all these obfuscated identity functions
> to make the type checker happy, though.

As I said, the types are not isomorphic -- it you think of type
parameters as arguments you will see why.

I found these examples interesting, mostly because I don't understand it very well. So, I simplified Klaus' code a bit and derived the following:

-----
{-# LANGUAGE Rank2Types #-}

-- Wrapper
newtype W a = W { unW :: a }

inside :: ((forall a. W (t a))-> W (forall a. (t a)))
--inside (W x) = W x -- (a) FAILS
--inside = W . unW -- (b) FAILS
inside x = W (unW x) -- (c) WORKS
-----

Can someone comment on the differences between the following in terms of type-checking or inference? Considering the errors I got, I'm guess the issue is the same for the pattern-matching (a) and the point-free (b) versions. Are there any pointers for developing a better understanding or intuition of this?

Thanks,
Sean