[Haskell-cafe] Moving "forall" over type constructors

[Edsko de Vries]

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