The paper &quot;Lexically scoped type variables&quot; 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:<div>

<br></div><div>    data Ap = forall a. Ap [a] ([a] -&gt; Int)</div><div><br></div><div>The constructor `Ap` has the type:</div><div><br></div><div>    Ap :: forall a. [a] -&gt; ([a] -&gt; Int) -&gt; Ap</div><div><br></div>

<div>And one can write a function:</div><div><br></div><div>    revap :: Ap -&gt; Int</div><div>    revap (Ap (xs :: [a]) f) = f ys</div><div>      where</div><div>        ys :: [a]</div><div>        ys = reverse xs</div>

<div><br></div><div>with the annotations on `xs` and `ys` being existential instead of universal.</div><div><br></div><div>But I&#39;m a little confused about *why* type-lambdas don&#39;t allow this. Aren&#39;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&#39;t it possible to write something like:</div>

<div><br></div><div><div>    fun &#39;a revap (Ap (xs : &#39;a list) f) = f ys</div><div>      where</div><div>        ys :: &#39;a list</div><div>        ys = reverse xs</div></div><div><br></div><div>in SML?</div><div>
<br>
</div><div>-Kangyuan Niu</div>