Why aren't existential types implemented in any mainstream language?
OCaml's idea of modules roughly correspond with existential types ;)

Let's set up some rough semantics in order to frame this correspondence properly. First, I'll give the intro/elimination rules for existential types (I'll only use a variable $\to$ type context $\Gamma$ for the sake of simplicity here):
$$
\frac{\Gamma \vdash e\{\alpha\mapsto \tau\} : \sigma\{\alpha\mapsto \tau\}}{\Gamma \vdash [\tau, e] : \exists \alpha. \sigma} ({\rm Pack}) ~~~~~~~ 
\frac{\Gamma \vdash e : \exists \alpha.\sigma ~~~ \Gamma, x:\sigma \vdash e' : \tau'}{\Gamma \vdash {\rm let} ~ [\alpha, x] = e ~ {\rm in} ~ e' : \tau'}({\rm Unpack})
$$
where $e\{\alpha \mapsto \tau\}$ substitutes all occurrences of the type variable $\alpha$ with the concrete type $\tau$. In practice, we will also decorate the packed form with its existential type in order to disambiguate the semantics.

Operationally, we have the context reductions:
$$
\frac{e \Downarrow v}{[\tau, e] \Downarrow [\tau, v]} ~~~~~~ \frac{e \Downarrow v}{{\rm let} ~ [\alpha, x] = e ~ {\rm in} ~ e' \Downarrow {\rm let} ~ [\alpha, x] = v ~ {\rm in} ~ e'}
$$
which corresponds to the reduction strategies that reduces the expressions in the existential packages and the expressions to be unpacked.

Finally, we have the extensional $\eta$-reduction rule:
$$
\frac{}{{\rm let} ~ [\alpha, x] = [\tau, v]_{\exists \alpha. \sigma} ~ {\rm in} ~ e \to e \{\alpha \mapsto \tau, x \mapsto v\}}
$$

So for example, the program
\begin{align*}
{\rm let} ~ [\alpha, x] &amp;= [{\rm int}, (0, {\rm succ})]_{\exists \alpha. \alpha \times (\alpha \to \alpha)} ~ {\rm in} ~ ({\rm snd} ~ x : \alpha \to \alpha)({\rm fst} ~ x : \alpha)\\
&amp;\to^{\eta} ({\rm snd} ~ (0, {\rm succ}) : {\rm int} \to {\rm int})({\rm fst} ~ (0, {\rm succ}) : {\rm int}) \\
&amp;\to^* {\rm succ} ~ 0 \\
&amp;\to^\beta 1
\end{align*}

This exact idea is present in OCaml's concept of modules, save that the packed type must be a record (but which can be made to be isomorphic to any other OCaml type). For example, the creation of an existential type is done through the module type keyword:



module type Bundle =
sig
  type α
  val data : α * (α -&gt; α)
end


This signature corresponds to the existential type $\exists \alpha. \alpha \times (\alpha \to \alpha)$. We can witness an inhabitant of this type by instantiating it with the struct keyword:

module BundleInt : Bundle = struct
  type α = int
  val data = (0, (+) 1)
end


which corresponds to the pack/intro $[{\rm int}, (0, (+) 1)]_{\exists \alpha. \alpha \times (\alpha \to \alpha)}$. Unfortunately, there is no explicit ${\rm let} \dots$ elimination form, but something like open BundleInt is equivalent to let [α, data] = BundleInt in ... where α and data are specified in the creation of the module type Bundle.

So while module types aren't exactly the same as your traditional existential types (the variables to be bound are explicitly pushed into the intro-form rather than in the elimination-form), their expressiveness are the same.