On Mon, Jun 09, 2008 at 03:20:33PM +0200, Klaus Ostermann wrote:
At first I'd like to thank Claus, Ryan, Edsko, Luke and Derek for their quite helpful replies to my previous thread.
In the course of following their advice I encountered the problem of moving a "forall" quantifier over a wrapper type constructor.
If I have
newtype Wrapper a = Wrapper a
and I instantiate Wrapper with a polymorphic type, then it is possible to move the quantifier outside:
outside :: Wrapper (forall a. (t a)) -> (forall a. Wrapper (t a)) outside(Wrapper x) = Wrapper x
(surprisingly the code does not work with the implementation 'outside x = x'; I guess this is a ghc bug)
Not a bug; those two types are not the same. In the code you've given, ghc needs to find evidence that it can create a element of type (Wrapper (t a)) for any any; fortunately, it can do so because it has 'x', which can create a 't a' for any 'a'.
inside :: (forall a. Wrapper (t a))-> Wrapper (forall a. (t a)) inside x= x
results in the following error:
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). Edsko