The paper "Lexically scoped type variables" by Simon Peyton Jones and Mark Shields describes two ways to give type variables lexical scoping. They state that one of the advantages of the GHC-style type-sharing approach over the SML-style type-lambda approach is that the former allows for existential quantification in addition to universal quantification. As an example, they give this code: data Ap = forall a. Ap [a] ([a] -> Int) The constructor `Ap` has the type: Ap :: forall a. [a] -> ([a] -> Int) -> Ap And one can write a function: revap :: Ap -> Int revap (Ap (xs :: [a]) f) = f ys where ys :: [a] ys = reverse xs with the annotations on `xs` and `ys` being existential instead of universal. But I'm a little confused about *why* type-lambdas don't allow this. Aren't both Haskell and SML translatable into System F, from which type-lambda is directly taken? What does the translation for the above code even look like? Why isn't it possible to write something like: fun 'a revap (Ap (xs : 'a list) f) = f ys where ys :: 'a list ys = reverse xs in SML? -Kangyuan Niu