[Haskell] polymorphism and existential types

[Louis-Julien Guillemette]

Supposing a polymorphic value (of type, say, forall a . ExpT a t) is
stored inside an existential package (of type, say, forall a . Exp a),
I wonder how to recover a polymorphic value when eliminating the
existential.  The ``natural way'' to write this doesn't work:

{-# OPTIONS -fglasgow-exts #-}

data ExpT a t
data Exp a = forall t . Exp (ExpT a t)

f :: (forall a . ExpT a t) -> ()
f e = ()

g :: (forall a . ExpT a t) -> ()
g e =
   let e1 :: forall a . Exp a
       e1 = Exp e
   in case e1 of
        Exp e' -> f e'

{-
Test.hs:18:17:
     Inferred type is less polymorphic than expected
       Quantified type variable `a' is mentioned in the environment:
         e' :: ExpT a t (bound at Test.hs:18:11)
     In the first argument of `f', namely `e''
     In the expression: f e'
     In a case alternative: Exp e' -> f e'
Failed, modules loaded: none.
-}


In particular, the solution of pushing the forall inside doesn't work
for me (it breaks other parts of my code...) :

data Exp' = forall t . Exp' (forall a . ExpT a t)

g' :: (forall a . ExpT a t) -> ()
g' e =
   let e1 :: Exp'
       e1 = Exp' e
   in case e1 of
        Exp' e' -> f e'


Any help welcome!

Louis-Julien