Sending to the right list this time, with some additions.
Just to show what kind of problems we are currently facing. The following type checks in our EHC compiler and in Hugs, but not in the GHC:
module Test where
data T s = forall x. T (s -> (x -> s) -> (x, s, Int))
run :: (forall s . T s) -> Int run ts = case ts of T g -> let (x,_, b) = g x id in b
Consider this additional code which also typechecks in Hugs: v :: forall s . T s v = T f f :: s -> ([s] -> s) -> ([s], s, Int) f v g = let x = [v] in (x, g x, 0) run v gives 0. Apparently id has type [s] -> s. I'm not sure if we're ending up with the infinite type s = [s], or maybe something really bad would happen in run v, if it were not for parametricity keeping us from examining the first two elements of the triple too closely (I tried adding Show constraints, but couldn't get code like that to typecheck). Now for wild speculation: Simplifing T and assuming full existentials, you might define something akin to run with a type like (forall s . exists x. (x -> s) -> (x, s)) -> (exists t . (t -> t) -> (t, t)), which suggest to me two ingredients (in a language with type operators), a functional axiom of choice plus fixpoints of type operators, ac :: (forall a . exists b. X) -> exists f::*->*. forall a . X[f(a)/b] and fixT :: (* -> *) -> * Then you might implement the type above as equalize pkg = open ac pkg as {exists F. body} in close {fixT F, body} Brandon