# [Haskell-cafe] [Redirect] polymorphism and existential types

Donald Bruce Stewart dons at cse.unsw.edu.au
Mon Nov 27 23:01:25 EST 2006

```Redirected to haskell-cafe at haskell.org, the right list.

-- Don

----- Forwarded message from Louis-Julien Guillemette <guillelj at iro.umontreal.ca> -----

Date: Mon, 27 Nov 2006 16:15:26 -0500 (EST)
From: Louis-Julien Guillemette
Subject: [Haskell] polymorphism and existential types

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'
-}

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
_______________________________________________