[Haskell-beginners] Problem with GADTs and Parsec

[Brent Yorgey]

On Sun, Feb 09, 2014 at 09:21:15AM +0100, Lorenzo wrote:
> > In my opinion, this is one of the few places where existential
> > wrappers are really what you want.  If I were you, I would do
> > something like this:
> > 
> >   data ExprE where
> >     ExprE :: Expr a -> ExprE   -- existentially hides the expression
> > type
> > 
> > Now you can write your parser to return an ExprE, with the type of the
> > expression hidden inside. In order to be able to use the resulting
> > ExprE values, you will also want a function like
> > 
> >   withExprE :: ExprE -> (Expr a -> r) -> r
> >   withExprE (ExprE expr) k = k expr
> 
> Thanks. This is the kind of solution I was looking for.
> The problem is, when I try to access the "hidden" Expr type the compiler
> complains:
> 

Whoops! Sorry, I gave you the wrong type for withExprE.  And you can
see why it is wrong, based on the earlier explanation: the *caller* of
withExprE gets to choose the type a, but there is some particular
(unknown) type inside the ExprE, so there is no guarantee they will
match up.  Instead, we must write

  withExprE :: ExprE -> (forall a. Expr a -> r) -> r

(note you have to enable the Rank2Types extension).  This says that
the caller of ExprE must provide a function which works *no matter
what* the type a is, i.e. the implementation of withExprE gets to
choose the type a, rather than the caller.

-Brent