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)'