On Mon, Jun 09, 2008 at 06:55:20AM -0700, Klaus Ostermann wrote:
But here we have an argument that can return a Wrapper (t a) for any 'a'; that does *not* mean it can return a wrapper of a polymorphic type. If you think about 'a' as an actual argument, then you could pass 'Int' to get a Wrapper (t Int), Bool to get a wrapper (t Bool), or even (forall a. a -> a) to get a Wrapper (t (forall a. a -> a)), but no argument at all could make a Wrapper (forall a. t a).
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. Edsko