The GADTs extension implies ExistentialQuantification

Summary

According to the User's Guide section on GADTs, the extension implies only MonoLocalBinds and GADTSyntax.

http://downloads.haskell.org/~ghc/latest/docs/html/users_guide/exts/gadt.html

However the following short program compiles so it seems that ExistentialQuantification is also implied by GADTs:

{-# LANGUAGE GADTs #-}

module T16344 where

data T3 a = forall b. MkT3 (T3 b)

Proposed improvements or changes

I'm assuming this is an oversight in User's Guide, rather than a GHC bug. IMO it makes sense to require ExistentialQuantification: it's definitely allowed in GADT-style declarations, so why not in regular syntax as well?

In this case, the fix is trivial: just add the ExistentialQuantification to the two extensions already implied by GADTs.

Environment

• GHC version used (if appropriate): 9.2.1