> While normaly forall plays a role of the "universal quantifier", it can also play a role of the "existential quantifier" (depends on the situation).

> What is interesting is that in this case, forall plays the role of an existential quantifier (therefore the name of extension, ExistentialQuantification), unlike the role of universal quantifier it normally plays.

This isn't really true. While you can indeed use "forall" to write something equivalent to an existentially quantified type, that doesn't mean it's playing that role. That'd be like saying that the English words "all" and "some" mean the same thing just because "not all X are Y" and "some X are not Y" mean the same thing.

I always write existential quantification

  data Showable = forall a. Show a => Showable a

with GADT syntax because it can be confusing for people to infer the type of `Showable' from the above definition when you can write it out

  data Showable where
    Showable :: Show a => a -> Showable

josephcsible is right. `forall.' in that context doesn't play a different role. Rather a variable bound by `forall.' is logically the same as existential quantification if it does not appear in the return type which `a' doesn't:

  Showable :: forall a. Show a => a -> Showable

We will get a proper existential quantifier soon

* https://github.com/ghc-proposals/ghc-proposals/pull/473 * https://richarde.dev/papers/2021/exists/exists.pdf

and then

  length :: forall a. [a] -> Int

can be replaced with

  length :: (exists a. [a]) -> Int

and `Showable' will be isomorphic to the "packed constraint" `exists a. Show a ∧ a', explained in the paper. This is a tupled constraint, not a function: `(Dict (Show a), a)'