User's guide: newtype decls can use GADTSyntax

The user's guide failed to explicitly mention that GADTSyntax
can be used to declare newtypes, so we add an example and a couple
of explanations.

Also explains that `-XGADTs` generalises `-XExistentialQuantification`.

Fixes #20848 and #20865.

5 files changed, 39 insertions, 4 deletions

diff --git a/docs/users_guide/exts/existential_quantification.rst b/docs/users_guide/exts/existential_quantification.rst
index 42f5cbdc83..4652f2cae0 100644
--- a/docs/users_guide/exts/existential_quantification.rst
+++ b/docs/users_guide/exts/existential_quantification.rst
@@ -176,6 +176,8 @@ For example: ::
     upd4 g x = g { g2=x }   -- BAD (g2's type mentions c, which is not a simple
                             --      type-variable argument in G1's result type)
 
+.. _existential-restrictions:
+
 Restrictions
 ~~~~~~~~~~~~
 
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index 3463bd63da..99902cc76d 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -80,13 +80,32 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
    each constructor must end with ``Term ty``, but the ``ty`` need not
    be a type variable (e.g. the ``Lit`` constructor).
 
+-  GADT constructors can include contexts and existential variables,
+   generalising existential quantification (:ref:`existential-quantification`).
+   For example: ::
+
+        data SomeShow where
+            SomeShow :: Show a => a -> SomeShow
+              -- `a` is existential, as it does not appear in the return type
+
+        data G a where
+            MkG :: (a ~ Int) => a -> a -> G a
+         -- essentially the same as:
+         -- MkG :: Int -> Int -> G Int
+
 -  It is permitted to declare an ordinary algebraic data type using
    GADT-style syntax. What makes a GADT into a GADT is not the syntax,
    but rather the presence of data constructors whose result type is not
-   just ``T a b``.
+   just ``T a b``, or which include contexts.
+
+-  A newtype may use GADT-style syntax, but it must declare an ordinary
+   data type, not a GADT. That is, the constructor must not bind
+   existential variables (as per :ref:`existential-quantification`)
+   nor include a context.
 
 -  You cannot use a ``deriving`` clause for a GADT; only for an ordinary
-   data type.
+   data type (possibly using GADT-style syntax). However, you can still use a
+   :ref:`stand-alone-deriving` declaration.
 
 -  As mentioned in :ref:`gadt-style`, record syntax is supported. For
    example:
diff --git a/docs/users_guide/exts/gadt_syntax.rst b/docs/users_guide/exts/gadt_syntax.rst
index 5b0e1631f3..c0cc6167c9 100644
--- a/docs/users_guide/exts/gadt_syntax.rst
+++ b/docs/users_guide/exts/gadt_syntax.rst
@@ -19,6 +19,9 @@ explicitly. For example: ::
           Nothing :: Maybe a
           Just    :: a -> Maybe a
 
+      newtype Down a where
+        Down :: a -> Down a
+
 The form is called a "GADT-style declaration" because Generalised
 Algebraic Data Types, described in :ref:`gadt`, can only be declared
 using this form.
@@ -30,8 +33,8 @@ are equivalent: ::
       data Foo = forall a. MkFoo a (a -> Bool)
       data Foo' where { MKFoo :: a -> (a->Bool) -> Foo' }
 
-Any data type that can be declared in standard Haskell 98 syntax can
-also be declared using GADT-style syntax. The choice is largely
+Any datatype (or newtype) that can be declared in standard Haskell 98 syntax,
+can also be declared using GADT-style syntax. The choice is largely
 stylistic, but GADT-style declarations differ in one important respect:
 they treat class constraints on the data constructors differently.
 Specifically, if the constructor is given a type-class context, that
@@ -103,6 +106,10 @@ implements this behaviour, odd though it is. But for GADT-style
 declarations, GHC's behaviour is much more useful, as well as much more
 intuitive.
 
+Note that the restrictions of :ref:`existential-restrictions` are still
+in place; for example, a newtype declared with ``GADTSyntax`` cannot
+use existential quantification.
+
 .. _formal-gadt-syntax:
 
 Formal syntax for GADTs
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 3152f3561b..ce30d570f3 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -97,6 +97,7 @@ test('T3651', normal, compile_fail, [''])
 test('T3638', normal, compile, [''])
 
 test('gadtSyntax001', normal, compile, [''])
+test('gadtSyntax002', normal, compile, [''])
 test('gadtSyntaxFail001', normal, compile_fail, [''])
 test('gadtSyntaxFail002', normal, compile_fail, [''])
 test('gadtSyntaxFail003', normal, compile_fail, [''])
diff --git a/testsuite/tests/gadt/gadtSyntax002.hs b/testsuite/tests/gadt/gadtSyntax002.hs
new file mode 100644
index 0000000000..46ccfb320c
--- /dev/null
+++ b/testsuite/tests/gadt/gadtSyntax002.hs
@@ -0,0 +1,6 @@
+{-# LANGUAGE GADTSyntax #-}
+
+module GADTSyntax002 where
+
+newtype Down a where
+  Down :: { getDown :: a } -> Down a