Hi,
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