Donald Bruce Stewart wrote:
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'
IIUC, this is not possible. I believe that the type given for e1 is strictly weaker than the type of e, so that recovering the type of e from that of e1 can not be done. This is because (up-to iso) e :: exists t . forall a . ExpT a t e1:: forall a . exists t . ExpT a t Clearly, the first one (where t is fixed) is stronger than the second, (where t might depend on a). Regards, Roberto Zunino.