Make GADT constructors adhere to the forall-or-nothing rule properly

Issue #18191 revealed that the types of GADT constructors don't quite
adhere to the `forall`-or-nothing rule. This patch serves to clean up
this sad state of affairs somewhat. The main change is not in the
code itself, but in the documentation, as this patch introduces two
sections to the GHC User's Guide:

* A "Formal syntax for GADTs" section that presents a BNF-style
  grammar for what is and isn't allowed in GADT constructor types.
  This mostly exists to codify GHC's existing behavior, but it also
  imposes a new restriction that addresses #18191: the outermost
  `forall` and/or context in a GADT constructor is not allowed to be
  surrounded by parentheses. Doing so would make these
  `forall`s/contexts nested, and GADTs do not support nested
  `forall`s/contexts at present.

* A "`forall`-or-nothing rule" section that describes exactly what
  the `forall`-or-nothing rule is all about. Surprisingly, there was
  no mention of this anywhere in the User's Guide up until now!

To adhere the new specification in the "Formal syntax for GADTs"
section of the User's Guide, the following code changes were made:

* A new function, `GHC.Hs.Type.splitLHsGADTPrefixTy`, was introduced.
  This is very much like `splitLHsSigmaTy`, except that it avoids
  splitting apart any parentheses, which can be syntactically
  significant for GADT types. See
  `Note [No nested foralls or contexts in GADT constructors]` in
  `GHC.Hs.Type`.

* `ConDeclGADTPrefixPs`, an extension constructor for `XConDecl`, was
  introduced so that `GHC.Parser.PostProcess.mkGadtDecl` can return
  it when given a prefix GADT constructor. Unlike `ConDeclGADT`,
  `ConDeclGADTPrefixPs` does not split the GADT type into its argument
  and result types, as this cannot be done until after the type is
  renamed (see `Note [GADT abstract syntax]` in `GHC.Hs.Decls` for why
  this is the case).

* `GHC.Renamer.Module.rnConDecl` now has an additional case for
  `ConDeclGADTPrefixPs` that (1) splits apart the full `LHsType` into
  its `forall`s, context, argument types, and result type, and
  (2) checks for nested `forall`s/contexts. Step (2) used to be
  performed the typechecker (in `GHC.Tc.TyCl.badDataConTyCon`) rather
  than the renamer, but now the relevant code from the typechecker
  can simply be deleted.

  One nice side effect of this change is that we are able to give a
  more accurate error message for GADT constructors that use visible
  dependent quantification (e.g., `MkFoo :: forall a -> a -> Foo a`),
  which improves the stderr in the `T16326_Fail6` test case.

Fixes #18191. Bumps the Haddock submodule.

26 files changed, 713 insertions, 297 deletions

diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index 9edd0ff871..f800d934b6 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -5,6 +5,7 @@
 
 {-# LANGUAGE DeriveDataTypeable, DeriveFunctor, DeriveFoldable,
              DeriveTraversable #-}
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE StandaloneDeriving #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE FlexibleInstances #-}
@@ -70,7 +71,7 @@ module GHC.Hs.Decls (
   ForeignDecl(..), LForeignDecl, ForeignImport(..), ForeignExport(..),
   CImportSpec(..),
   -- ** Data-constructor declarations
-  ConDecl(..), LConDecl,
+  ConDecl(..), LConDecl, ConDeclGADTPrefixPs(..),
   HsConDeclDetails, hsConDeclArgTys, hsConDeclTheta,
   getConNames, getConArgs,
   -- ** Document comments
@@ -109,6 +110,7 @@ import GHC.Core.Coercion
 import GHC.Types.ForeignCall
 import GHC.Hs.Extension
 import GHC.Types.Name
+import GHC.Types.Name.Reader
 import GHC.Types.Name.Set
 
 -- others:
@@ -1422,54 +1424,144 @@ type instance XConDeclGADT GhcRn = [Name] -- Implicitly bound type variables
 type instance XConDeclGADT GhcTc = NoExtField
 
 type instance XConDeclH98  (GhcPass _) = NoExtField
-type instance XXConDecl    (GhcPass _) = NoExtCon
+
+type instance XXConDecl GhcPs = ConDeclGADTPrefixPs
+type instance XXConDecl GhcRn = NoExtCon
+type instance XXConDecl GhcTc = NoExtCon
+
+-- | Stores the types of prefix GADT constructors in the parser. This is used
+-- in lieu of ConDeclGADT, which requires knowing the specific argument and
+-- result types, as this is difficult to determine in general in the parser.
+-- See @Note [GADT abstract syntax]@.
+data ConDeclGADTPrefixPs = ConDeclGADTPrefixPs
+  { con_gp_names :: [Located RdrName]
+    -- ^ The GADT constructor declaration's names.
+  , con_gp_ty    :: LHsSigType GhcPs
+    -- ^ The type after the @::@.
+  , con_gp_doc   :: Maybe LHsDocString
+    -- ^ A possible Haddock comment.
+  }
 
 {- Note [GADT abstract syntax]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-There's a wrinkle in ConDeclGADT
-
-* For record syntax, it's all uniform.  Given:
-      data T a where
-        K :: forall a. Ord a => { x :: [a], ... } -> T a
-    we make the a ConDeclGADT for K with
-       con_qvars  = {a}
-       con_mb_cxt = Just [Ord a]
-       con_args   = RecCon <the record fields>
-       con_res_ty = T a
-
-  We need the RecCon before the reanmer, so we can find the record field
-  binders in GHC.Hs.Utils.hsConDeclsBinders.
-
-* However for a GADT constr declaration which is not a record, it can
-  be hard parse until we know operator fixities. Consider for example
-     C :: a :*: b -> a :*: b -> a :+: b
-  Initially this type will parse as
-      a :*: (b -> (a :*: (b -> (a :+: b))))
-  so it's hard to split up the arguments until we've done the precedence
-  resolution (in the renamer).
-
-  So:  - In the parser (GHC.Parser.PostProcess.mkGadtDecl), we put the whole constr
-         type into the res_ty for a ConDeclGADT for now, and use
-         PrefixCon []
-            con_args   = PrefixCon []
-            con_res_ty = a :*: (b -> (a :*: (b -> (a :+: b))))
-
-       - In the renamer (GHC.Rename.Module.rnConDecl), we unravel it after
-         operator fixities are sorted. So we generate. So we end
-         up with
-            con_args   = PrefixCon [ a :*: b, a :*: b ]
-            con_res_ty = a :+: b
+There are two broad ways to classify GADT constructors:
+
+* Record-syntax constructors. For example:
+
+    data T a where
+      K :: forall a. Ord a => { x :: [a], ... } -> T a
+
+* Prefix constructors, which do not use record syntax. For example:
+
+    data T a where
+      K :: forall a. Ord a => [a] -> ... -> T a
+
+Initially, both forms of GADT constructors are initially parsed as a single
+LHsType. However, GADTs have a certain structure, requiring distinct argument
+and result types, as well as imposing restrictions on where `forall`s and
+contexts can be (see "Wrinkle: No nested foralls or contexts" below). As a
+result, it is convenient to split up the LHsType into its individual
+components, which are stored in the ConDeclGADT constructor of ConDecl.
+
+Where should this splitting occur? For GADT constructors with record syntax,
+we split in the parser (in GHC.Parser.PostProcess.mkGadtDecl). We must do this
+splitting before the renamer, as we need the record field names for use in
+GHC.Hs.Utils.hsConDeclsBinders.
+
+For prefix GADT constructors, however, the situation is more complicated. It
+can be difficult to split a prefix GADT type until we know type operator
+fixities. Consider this, for example:
+
+  C :: a :*: b -> a :*: b -> a :+: b
+
+Initially, the type of C will parse as:
+
+  a :*: (b -> (a :*: (b -> (a :+: b))))
+
+So it's hard to split up the arguments until we've done the precedence
+resolution (in the renamer). (Unlike prefix GADT types, record GADT types
+do not have this problem because of their uniform syntax.)
+
+As a result, we deliberately avoid splitting prefix GADT types in the parser.
+Instead, we store the entire LHsType in ConDeclGADTPrefixPs, a GHC-specific
+extension constructor to ConDecl. Later, in the renamer
+(in GHC.Rename.Module.rnConDecl), we resolve the fixities of all type operators
+in the LHsType, which facilitates splitting it into argument and result types
+accurately. We finish renaming a ConDeclGADTPrefixPs by putting the split
+components into a ConDeclGADT. This is why ConDeclGADTPrefixPs has the suffix
+-Ps, as it is only used by the parser.
+
+Note that the existence of ConDeclGADTPrefixPs does not imply that ConDeclGADT
+goes completely unused by the parser. Other consumers of GHC's abstract syntax
+are still free to use ConDeclGADT. Indeed, both Haddock and Template Haskell
+construct values of type `ConDecl GhcPs` by way of ConDeclGADT, as neither of
+them have the same difficulties with operator precedence that GHC's parser
+does. As an example, see GHC.ThToHs.cvtConstr, which converts Template Haskell
+syntax into GHC syntax.
+
+-----
+-- Wrinkle: No nested foralls or contexts
+-----
+
+GADT constructors provide some freedom to change the order of foralls in their
+types (see Note [DataCon user type variable binders] in GHC.Core.DataCon), but
+this freedom is still limited. GADTs still require that all quantification
+occurs "prenex". That is, any explicitly quantified type variables must occur
+at the front of the GADT type, followed by any contexts, followed by the body of
+the GADT type, in precisely that order. For instance:
+
+  data T where
+    MkT1 :: forall a b. (Eq a, Eq b) => a -> b -> T
+      -- OK
+    MkT2 :: forall a. Eq a => forall b. a -> b -> T
+      -- Rejected, `forall b` is nested
+    MkT3 :: forall a b. Eq a => Eq b => a -> b -> T
+      -- Rejected, `Eq b` is nested
+    MkT4 :: Int -> forall a. a -> T
+      -- Rejected, `forall a` is nested
+    MkT5 :: forall a. Int -> Eq a => a -> T
+      -- Rejected, `Eq a` is nested
+    MkT6 :: (forall a. a -> T)
+      -- Rejected, `forall a` is nested due to the surrounding parentheses
+    MkT7 :: (Eq a => a -> t)
+      -- Rejected, `Eq a` is nested due to the surrounding parentheses
+
+For the full details, see the "Formal syntax for GADTs" section of the GHC
+User's Guide. GHC enforces that GADT constructors do not have nested `forall`s
+or contexts in two parts:
+
+1. GHC, in the process of splitting apart a GADT's type,
+   extracts out the leading `forall` and context (if they are provided). To
+   accomplish this splitting, the renamer uses the
+   GHC.Hs.Type.splitLHsGADTPrefixTy function, which is careful not to remove
+   parentheses surrounding the leading `forall` or context (as these
+   parentheses can be syntactically significant). If the third result returned
+   by splitLHsGADTPrefixTy contains any `forall`s or contexts, then they must
+   be nested, so they will be rejected.
+
+   Note that this step applies to both prefix and record GADTs alike, as they
+   both have syntax which permits `forall`s and contexts. The difference is
+   where this step happens:
+
+   * For prefix GADTs, this happens in the renamer (in rnConDecl), as we cannot
+     split until after the type operator fixities have been resolved.
+   * For record GADTs, this happens in the parser (in mkGadtDecl).
+2. If the GADT type is prefix, the renamer (in the ConDeclGADTPrefixPs case of
+   rnConDecl) will then check for nested `forall`s/contexts in the body of a
+   prefix GADT type, after it has determined what all of the argument types are.
+   This step is necessary to catch examples like MkT4 above, where the nested
+   quantification occurs after a visible argument type.
 -}
 
 -- | Haskell data Constructor Declaration Details
 type HsConDeclDetails pass
    = HsConDetails (LBangType pass) (Located [LConDeclField pass])
 
-getConNames :: ConDecl (GhcPass p) -> [Located (IdP (GhcPass p))]
+getConNames :: ConDecl GhcRn -> [Located Name]
 getConNames ConDeclH98  {con_name  = name}  = [name]
 getConNames ConDeclGADT {con_names = names} = names
 
-getConArgs :: ConDecl pass -> HsConDeclDetails pass
+getConArgs :: ConDecl GhcRn -> HsConDeclDetails GhcRn
 getConArgs d = con_args d
 
 hsConDeclArgTys :: HsConDeclDetails pass -> [LBangType pass]
@@ -1518,16 +1610,30 @@ instance Outputable NewOrData where
   ppr NewType  = text "newtype"
   ppr DataType = text "data"
 
-pp_condecls :: (OutputableBndrId p) => [LConDecl (GhcPass p)] -> SDoc
-pp_condecls cs@(L _ ConDeclGADT{} : _) -- In GADT syntax
+pp_condecls :: forall p. OutputableBndrId p => [LConDecl (GhcPass p)] -> SDoc
+pp_condecls cs
+  | gadt_syntax                  -- In GADT syntax
   = hang (text "where") 2 (vcat (map ppr cs))
-pp_condecls cs                    -- In H98 syntax
+  | otherwise                    -- In H98 syntax
   = equals <+> sep (punctuate (text " |") (map ppr cs))
+  where
+    gadt_syntax = case cs of
+      []                      -> False
+      (L _ ConDeclH98{}  : _) -> False
+      (L _ ConDeclGADT{} : _) -> True
+      (L _ (XConDecl x)  : _) ->
+        case ghcPass @p of
+          GhcPs |  ConDeclGADTPrefixPs{} <- x
+                -> True
+#if __GLASGOW_HASKELL__ < 811
+          GhcRn -> noExtCon x
+          GhcTc -> noExtCon x
+#endif
 
 instance (OutputableBndrId p) => Outputable (ConDecl (GhcPass p)) where
     ppr = pprConDecl
 
-pprConDecl :: (OutputableBndrId p) => ConDecl (GhcPass p) -> SDoc
+pprConDecl :: forall p. OutputableBndrId p => ConDecl (GhcPass p) -> SDoc
 pprConDecl (ConDeclH98 { con_name = L _ con
                        , con_ex_tvs = ex_tvs
                        , con_mb_cxt = mcxt
@@ -1558,6 +1664,16 @@ pprConDecl (ConDeclGADT { con_names = cons, con_qvars = qvars
     ppr_arrow_chain (a:as) = sep (a : map (arrow <+>) as)
     ppr_arrow_chain []     = empty
 
+pprConDecl (XConDecl x) =
+  case ghcPass @p of
+    GhcPs |  ConDeclGADTPrefixPs { con_gp_names = cons, con_gp_ty = ty
+                                 , con_gp_doc = doc } <- x
+          -> ppr_mbDoc doc <+> ppr_con_names cons <+> dcolon <+> ppr ty
+#if __GLASGOW_HASKELL__ < 811
+    GhcRn -> noExtCon x
+    GhcTc -> noExtCon x
+#endif
+
 ppr_con_names :: (OutputableBndr a) => [Located a] -> SDoc
 ppr_con_names = pprWithCommas (pprPrefixOcc . unLoc)
 
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 61cb81006b..99d627965d 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -166,6 +166,8 @@ deriving instance Data (ConDecl GhcPs)
 deriving instance Data (ConDecl GhcRn)
 deriving instance Data (ConDecl GhcTc)
 
+deriving instance Data ConDeclGADTPrefixPs
+
 -- deriving instance DataIdLR p p   => Data (TyFamInstDecl p)
 deriving instance Data (TyFamInstDecl GhcPs)
 deriving instance Data (TyFamInstDecl GhcRn)
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 8dfc317cd9..ef935cc59f 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -58,7 +58,8 @@ module GHC.Hs.Type (
         hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
         splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
         splitLHsPatSynTy,
-        splitLHsForAllTyInvis, splitLHsQualTy, splitLHsSigmaTyInvis,
+        splitLHsForAllTyInvis, splitLHsQualTy,
+        splitLHsSigmaTyInvis, splitLHsGADTPrefixTy,
         splitHsFunType, hsTyGetAppHead_maybe,
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
         ignoreParens, hsSigType, hsSigWcType, hsPatSigType,
@@ -1348,6 +1349,43 @@ splitLHsSigmaTyInvis ty
   , (ctxt, ty2) <- splitLHsQualTy ty1
   = (tvs, ctxt, ty2)
 
+-- | Decompose a prefix GADT type into its constituent parts.
+-- Returns @(mb_tvbs, mb_ctxt, body)@, where:
+--
+-- * @mb_tvbs@ are @Just@ the leading @forall@s, if they are provided.
+--   Otherwise, they are @Nothing@.
+--
+-- * @mb_ctxt@ is @Just@ the context, if it is provided.
+--   Otherwise, it is @Nothing@.
+--
+-- * @body@ is the body of the type after the optional @forall@s and context.
+--
+-- This function is careful not to look through parentheses.
+-- See @Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)@
+-- "GHC.Hs.Decls" for why this is important.
+splitLHsGADTPrefixTy ::
+     LHsType pass
+  -> (Maybe [LHsTyVarBndr Specificity pass], Maybe (LHsContext pass), LHsType pass)
+splitLHsGADTPrefixTy ty
+  | (mb_tvbs, rho) <- split_forall ty
+  , (mb_ctxt, tau) <- split_ctxt rho
+  = (mb_tvbs, mb_ctxt, tau)
+  where
+    -- NB: We do not use splitLHsForAllTyInvis below, since that looks through
+    -- parentheses...
+    split_forall (L _ (HsForAllTy { hst_fvf = ForallInvis, hst_bndrs = bndrs
+                                  , hst_body = rho }))
+      = (Just bndrs, rho)
+    split_forall sigma
+      = (Nothing, sigma)
+
+    -- ...similarly, we do not use splitLHsQualTy below, since that also looks
+    -- through parentheses.
+    split_ctxt (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau }))
+      = (Just cxt, tau)
+    split_ctxt tau
+      = (Nothing, tau)
+
 -- | Decompose a type of the form @forall <tvs>. body@ into its constituent
 -- parts. Only splits type variable binders that
 -- were quantified invisibly (e.g., @forall a.@, with a dot).
diff --git a/compiler/GHC/Hs/Utils.hs b/compiler/GHC/Hs/Utils.hs
index cbb21b1ad0..f8199b3332 100644
--- a/compiler/GHC/Hs/Utils.hs
+++ b/compiler/GHC/Hs/Utils.hs
@@ -1242,7 +1242,8 @@ hsTyClForeignBinders tycl_decls foreign_decls
     getSelectorNames (ns, fs) = map unLoc ns ++ map (extFieldOcc . unLoc) fs
 
 -------------------
-hsLTyClDeclBinders :: Located (TyClDecl (GhcPass p))
+hsLTyClDeclBinders :: IsPass p
+                   => Located (TyClDecl (GhcPass p))
                    -> ([Located (IdP (GhcPass p))], [LFieldOcc (GhcPass p)])
 -- ^ Returns all the /binding/ names of the decl.  The first one is
 -- guaranteed to be the name of the decl. The first component
@@ -1304,7 +1305,8 @@ getPatSynBinds binds
           , L _ (PatSynBind _ psb) <- bagToList lbinds ]
 
 -------------------
-hsLInstDeclBinders :: LInstDecl (GhcPass p)
+hsLInstDeclBinders :: IsPass p
+                   => LInstDecl (GhcPass p)
                    -> ([Located (IdP (GhcPass p))], [LFieldOcc (GhcPass p)])
 hsLInstDeclBinders (L _ (ClsInstD
                              { cid_inst = ClsInstDecl
@@ -1316,7 +1318,8 @@ hsLInstDeclBinders (L _ (TyFamInstD {})) = mempty
 
 -------------------
 -- | the 'SrcLoc' returned are for the whole declarations, not just the names
-hsDataFamInstBinders :: DataFamInstDecl (GhcPass p)
+hsDataFamInstBinders :: IsPass p
+                     => DataFamInstDecl (GhcPass p)
                      -> ([Located (IdP (GhcPass p))], [LFieldOcc (GhcPass p)])
 hsDataFamInstBinders (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
                        FamEqn { feqn_rhs = defn }}})
@@ -1325,7 +1328,8 @@ hsDataFamInstBinders (DataFamInstDecl { dfid_eqn = HsIB { hsib_body =
 
 -------------------
 -- | the 'SrcLoc' returned are for the whole declarations, not just the names
-hsDataDefnBinders :: HsDataDefn (GhcPass p)
+hsDataDefnBinders :: IsPass p
+                  => HsDataDefn (GhcPass p)
                   -> ([Located (IdP (GhcPass p))], [LFieldOcc (GhcPass p)])
 hsDataDefnBinders (HsDataDefn { dd_cons = cons })
   = hsConDeclsBinders cons
@@ -1335,7 +1339,8 @@ hsDataDefnBinders (HsDataDefn { dd_cons = cons })
 type Seen p = [LFieldOcc (GhcPass p)] -> [LFieldOcc (GhcPass p)]
                  -- Filters out ones that have already been seen
 
-hsConDeclsBinders :: [LConDecl (GhcPass p)]
+hsConDeclsBinders :: forall p. IsPass p
+                  => [LConDecl (GhcPass p)]
                   -> ([Located (IdP (GhcPass p))], [LFieldOcc (GhcPass p)])
    -- See hsLTyClDeclBinders for what this does
    -- The function is boringly complicated because of the records
@@ -1365,6 +1370,16 @@ hsConDeclsBinders cons
                 (remSeen', flds) = get_flds remSeen args
                 (ns, fs) = go remSeen' rs
 
+           XConDecl x -> case ghcPass @p of
+             GhcPs |  ConDeclGADTPrefixPs { con_gp_names = names } <- x
+                   -> (map (L loc . unLoc) names ++ ns, fs)
+#if __GLASGOW_HASKELL__ < 811
+             GhcRn -> noExtCon x
+             GhcTc -> noExtCon x
+#endif
+             where
+               (ns, fs) = go remSeen rs
+
     get_flds :: Seen p -> HsConDeclDetails (GhcPass p)
              -> (Seen p, [LFieldOcc (GhcPass p)])
     get_flds remSeen (RecCon flds)
diff --git a/compiler/GHC/Parser.y b/compiler/GHC/Parser.y
index 50459c673e..a081205033 100644
--- a/compiler/GHC/Parser.y
+++ b/compiler/GHC/Parser.y
@@ -2250,9 +2250,8 @@ gadt_constr :: { LConDecl GhcPs }
     -- see Note [Difference in parsing GADT and data constructors]
     -- Returns a list because of:   C,D :: ty
         : con_list '::' sigtypedoc
-                {% let (gadt,anns) = mkGadtDecl (unLoc $1) $3
-                   in ams (sLL $1 $> gadt)
-                       (mu AnnDcolon $2:anns) }
+                {% ams (sLL $1 $> (mkGadtDecl (unLoc $1) $3))
+                       [mu AnnDcolon $2] }
 
 {- Note [Difference in parsing GADT and data constructors]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 273fa0d704..645f56fc54 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -685,43 +685,35 @@ mkConDeclH98 name mb_forall mb_cxt args
                , con_args   = args
                , con_doc    = Nothing }
 
+-- | Construct a GADT-style data constructor from the constructor names and
+-- their type. This will return different AST forms for record syntax
+-- constructors and prefix constructors, as the latter must be handled
+-- specially in the renamer. See @Note [GADT abstract syntax]@ in
+-- "GHC.Hs.Decls" for the full story.
 mkGadtDecl :: [Located RdrName]
-           -> LHsType GhcPs     -- Always a HsForAllTy
-           -> (ConDecl GhcPs, [AddAnn])
+           -> LHsType GhcPs
+           -> ConDecl GhcPs
 mkGadtDecl names ty
-  = (ConDeclGADT { con_g_ext  = noExtField
-                 , con_names  = names
-                 , con_forall = L l $ isLHsForAllTy ty'
-                 , con_qvars  = tvs
-                 , con_mb_cxt = mcxt
-                 , con_args   = args
-                 , con_res_ty = res_ty
-                 , con_doc    = Nothing }
-    , anns1 ++ anns2)
+  | Just (mtvs, mcxt, args, res_ty) <- mb_record_gadt ty
+  = ConDeclGADT { con_g_ext  = noExtField
+                , con_names  = names
+                , con_forall = L (getLoc ty) $ isJust mtvs
+                , con_qvars  = fromMaybe [] mtvs
+                , con_mb_cxt = mcxt
+                , con_args   = args
+                , con_res_ty = res_ty
+                , con_doc    = Nothing }
+  | otherwise
+  = XConDecl $ ConDeclGADTPrefixPs { con_gp_names = names
+                                   , con_gp_ty    = mkLHsSigType ty
+                                   , con_gp_doc   = Nothing }
   where
-    (ty'@(L l _),anns1) = peel_parens ty []
-    (tvs, rho) = splitLHsForAllTyInvis ty'
-    (mcxt, tau, anns2) = split_rho rho []
-
-    split_rho (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau })) ann
-      = (Just cxt, tau, ann)
-    split_rho (L l (HsParTy _ ty)) ann
-      = split_rho ty (ann++mkParensApiAnn l)
-    split_rho tau                  ann
-      = (Nothing, tau, ann)
-
-    (args, res_ty) = split_tau tau
-
-    -- See Note [GADT abstract syntax] in GHC.Hs.Decls
-    split_tau (L _ (HsFunTy _ (L loc (HsRecTy _ rf)) res_ty))
-      = (RecCon (L loc rf), res_ty)
-    split_tau tau
-      = (PrefixCon [], tau)
-
-    peel_parens (L l (HsParTy _ ty)) ann = peel_parens ty
-                                                       (ann++mkParensApiAnn l)
-    peel_parens ty                   ann = (ty, ann)
-
+    mb_record_gadt ty
+      | (mtvs, mcxt, body_ty) <- splitLHsGADTPrefixTy ty
+      , L _ (HsFunTy _ (L loc (HsRecTy _ rf)) res_ty) <- body_ty
+      = Just (mtvs, mcxt, RecCon (L loc rf), res_ty)
+      | otherwise
+      = Nothing
 
 setRdrNameSpace :: RdrName -> NameSpace -> RdrName
 -- ^ This rather gruesome function is used mainly by the parser.
diff --git a/compiler/GHC/Parser/PostProcess/Haddock.hs b/compiler/GHC/Parser/PostProcess/Haddock.hs
index f232113c2e..409b0c120f 100644
--- a/compiler/GHC/Parser/PostProcess/Haddock.hs
+++ b/compiler/GHC/Parser/PostProcess/Haddock.hs
@@ -12,24 +12,28 @@ import Control.Monad
 -- -----------------------------------------------------------------------------
 -- Adding documentation to record fields (used in parsing).
 
-addFieldDoc :: LConDeclField a -> Maybe LHsDocString -> LConDeclField a
+addFieldDoc :: LConDeclField GhcPs -> Maybe LHsDocString -> LConDeclField GhcPs
 addFieldDoc (L l fld) doc
   = L l (fld { cd_fld_doc = cd_fld_doc fld `mplus` doc })
 
-addFieldDocs :: [LConDeclField a] -> Maybe LHsDocString -> [LConDeclField a]
+addFieldDocs :: [LConDeclField GhcPs] -> Maybe LHsDocString -> [LConDeclField GhcPs]
 addFieldDocs [] _ = []
 addFieldDocs (x:xs) doc = addFieldDoc x doc : xs
 
 
-addConDoc :: LConDecl a -> Maybe LHsDocString -> LConDecl a
+addConDoc :: LConDecl GhcPs -> Maybe LHsDocString -> LConDecl GhcPs
 addConDoc decl    Nothing = decl
-addConDoc (L p c) doc     = L p ( c { con_doc = con_doc c `mplus` doc } )
+addConDoc (L p c) doc     = L p $ case c of
+  ConDeclH98  { con_doc = old_doc } -> c { con_doc = old_doc `mplus` doc }
+  ConDeclGADT { con_doc = old_doc } -> c { con_doc = old_doc `mplus` doc }
+  XConDecl x@(ConDeclGADTPrefixPs { con_gp_doc = old_doc }) ->
+    XConDecl (x { con_gp_doc = old_doc `mplus` doc })
 
-addConDocs :: [LConDecl a] -> Maybe LHsDocString -> [LConDecl a]
+addConDocs :: [LConDecl GhcPs] -> Maybe LHsDocString -> [LConDecl GhcPs]
 addConDocs [] _ = []
 addConDocs [x] doc = [addConDoc x doc]
 addConDocs (x:xs) doc = x : addConDocs xs doc
 
-addConDocFirst :: [LConDecl a] -> Maybe LHsDocString -> [LConDecl a]
+addConDocFirst :: [LConDecl GhcPs] -> Maybe LHsDocString -> [LConDecl GhcPs]
 addConDocFirst [] _ = []
 addConDocFirst (x:xs) doc = addConDoc x doc : xs
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 5e9d4dec64..0a355b01ee 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -1746,8 +1746,9 @@ rnDataDefn doc (HsDataDefn { dd_ND = new_or_data, dd_cType = cType
         }
   where
     h98_style = case condecls of  -- Note [Stupid theta]
-                     (L _ (ConDeclGADT {})) : _  -> False
-                     _                           -> True
+                     (L _ (ConDeclGADT {}))                    : _ -> False
+                     (L _ (XConDecl (ConDeclGADTPrefixPs {}))) : _ -> False
+                     _                                             -> True
 
     rn_derivs (L loc ds)
       = do { deriv_strats_ok <- xoptM LangExt.DerivingStrategies
@@ -2084,7 +2085,7 @@ rnConDecl decl@(ConDeclH98 { con_name = name, con_ex_tvs = ex_tvs
     do  { (new_context, fvs1) <- rnMbContext ctxt mcxt
         ; (new_args,    fvs2) <- rnConDeclDetails (unLoc new_name) ctxt args
         ; let all_fvs  = fvs1 `plusFV` fvs2
-        ; traceRn "rnConDecl" (ppr name <+> vcat
+        ; traceRn "rnConDecl (ConDeclH98)" (ppr name <+> vcat
              [ text "ex_tvs:" <+> ppr ex_tvs
              , text "new_ex_dqtvs':" <+> ppr new_ex_tvs ])
 
@@ -2127,22 +2128,68 @@ rnConDecl decl@(ConDeclGADT { con_names   = names
         ; (new_res_ty, fvs3) <- rnLHsType ctxt res_ty
 
         ; let all_fvs = fvs1 `plusFV` fvs2 `plusFV` fvs3
-              (args', res_ty')
-                  = case args of
-                      InfixCon {}  -> pprPanic "rnConDecl" (ppr names)
-                      RecCon {}    -> (new_args, new_res_ty)
-                      PrefixCon as | (arg_tys, final_res_ty) <- splitHsFunType new_res_ty
-                                   -> ASSERT( null as )
-                                      -- See Note [GADT abstract syntax] in GHC.Hs.Decls
-                                      (PrefixCon arg_tys, final_res_ty)
-
-        ; traceRn "rnConDecl2" (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
+
+        ; traceRn "rnConDecl (ConDeclGADT)"
+            (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
         ; return (decl { con_g_ext = implicit_tkvs, con_names = new_names
                        , con_qvars = explicit_tkvs, con_mb_cxt = new_cxt
-                       , con_args = args', con_res_ty = res_ty'
+                       , con_args = new_args, con_res_ty = new_res_ty
                        , con_doc = mb_doc' },
                   all_fvs) } }
 
+-- This case is only used for prefix GADT constructors generated by GHC's
+-- parser, where we do not know the argument types until type operator
+-- precedence has been resolved. See Note [GADT abstract syntax] in
+-- GHC.Hs.Decls for the full story.
+rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
+                                         , con_gp_doc = mb_doc }))
+  = do { mapM_ (addLocM checkConName) names
+       ; new_names <- mapM lookupLocatedTopBndrRn names
+       ; mb_doc'   <- rnMbLHsDoc mb_doc
+
+       ; let ctxt = ConDeclCtx new_names
+       ; (ty', fvs) <- rnHsSigType ctxt TypeLevel Nothing ty
+
+         -- Now that operator precedence has been resolved, we can split the
+         -- GADT type into its individual components below.
+       ; let HsIB { hsib_ext = implicit_tkvs, hsib_body = body } = ty'
+             (mb_explicit_tkvs, mb_cxt, tau) = splitLHsGADTPrefixTy body
+             lhas_forall       = L (getLoc body) $ isJust mb_explicit_tkvs
+             explicit_tkvs     = fromMaybe [] mb_explicit_tkvs
+             (arg_tys, res_ty) = splitHsFunType tau
+             arg_details       = PrefixCon arg_tys
+               -- NB: The only possibility here is PrefixCon. RecCon is handled
+               -- separately, through ConDeclGADT, from the parser onwards.
+
+         -- Ensure that there are no nested `forall`s or contexts, per
+         -- Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)
+         -- in GHC.Hs.Type.
+       ; case res_ty of
+           L l (HsForAllTy { hst_fvf = fvf })
+             |  ForallVis <- fvf
+             -> setSrcSpan l $ addErr $ withHsDocContext ctxt $ vcat
+                [ text "Illegal visible, dependent quantification" <+>
+                  text "in the type of a term"
+                , text "(GHC does not yet support this)" ]
+             |  ForallInvis <- fvf
+             -> nested_foralls_contexts_err l ctxt
+           L l (HsQualTy {})
+             -> nested_foralls_contexts_err l ctxt
+           _ -> pure ()
+
+       ; traceRn "rnConDecl (ConDeclGADTPrefixPs)"
+           (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
+       ; pure (ConDeclGADT { con_g_ext = implicit_tkvs, con_names = new_names
+                           , con_forall = lhas_forall, con_qvars = explicit_tkvs
+                           , con_mb_cxt = mb_cxt, con_args = arg_details
+                           , con_res_ty = res_ty, con_doc = mb_doc' },
+               fvs) }
+  where
+    nested_foralls_contexts_err :: SrcSpan -> HsDocContext -> RnM ()
+    nested_foralls_contexts_err l ctxt =
+      setSrcSpan l $ addErr $ withHsDocContext ctxt $
+      text "GADT constructor type signature cannot contain nested"
+      <+> quotes forAllLit <> text "s or contexts"
 
 rnMbContext :: HsDocContext -> Maybe (LHsContext GhcPs)
             -> RnM (Maybe (LHsContext GhcRn), FreeVars)
diff --git a/compiler/GHC/Tc/TyCl.hs b/compiler/GHC/Tc/TyCl.hs
index 98550132c5..8ff9ad0d3e 100644
--- a/compiler/GHC/Tc/TyCl.hs
+++ b/compiler/GHC/Tc/TyCl.hs
@@ -3058,7 +3058,7 @@ dataDeclChecks tc_name new_or_data (L _ stupid_theta) cons
 
 
 -----------------------------------
-consUseGadtSyntax :: [LConDecl a] -> Bool
+consUseGadtSyntax :: [LConDecl GhcRn] -> Bool
 consUseGadtSyntax (L _ (ConDeclGADT {}) : _) = True
 consUseGadtSyntax _                          = False
                  -- All constructors have same shape
@@ -4705,50 +4705,12 @@ noClassTyVarErr clas fam_tc
 
 badDataConTyCon :: DataCon -> Type -> SDoc
 badDataConTyCon data_con res_ty_tmpl
-  | ASSERT( all isTyVar tvs )
-    tcIsForAllTy actual_res_ty
-  = nested_foralls_contexts_suggestion
-  | isJust (tcSplitPredFunTy_maybe actual_res_ty)
-  = nested_foralls_contexts_suggestion
-  | otherwise
   = hang (text "Data constructor" <+> quotes (ppr data_con) <+>
                 text "returns type" <+> quotes (ppr actual_res_ty))
        2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
   where
     actual_res_ty = dataConOrigResTy data_con
 
-    -- This suggestion is useful for suggesting how to correct code like what
-    -- was reported in #12087:
-    --
-    --   data F a where
-    --     MkF :: Ord a => Eq a => a -> F a
-    --
-    -- Although nested foralls or contexts are allowed in function type
-    -- signatures, it is much more difficult to engineer GADT constructor type
-    -- signatures to allow something similar, so we error in the latter case.
-    -- Nevertheless, we can at least suggest how a user might reshuffle their
-    -- exotic GADT constructor type signature so that GHC will accept.
-    nested_foralls_contexts_suggestion =
-      text "GADT constructor type signature cannot contain nested"
-      <+> quotes forAllLit <> text "s or contexts"
-      $+$ hang (text "Suggestion: instead use this type signature:")
-             2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
-
-    -- To construct a type that GHC would accept (suggested_ty), we
-    -- simply drag all the foralls and (=>) contexts to the front
-    -- of the type.
-    suggested_ty = mkSpecSigmaTy tvs theta rho
-    (tvs, theta, rho) = go (dataConUserType data_con)
-
-    go :: Type -> ([TyVar],ThetaType,Type)
-    -- The returned Type has no foralls or =>, even to the right of an (->)
-    go ty | null arg_tys = (tvs1, theta1, rho1)
-          | otherwise    = (tvs1 ++ tvs2, theta1 ++ theta2, mkVisFunTys arg_tys rho2)
-      where
-        (tvs1, theta1, rho1) = tcSplitNestedSigmaTys ty
-        (arg_tys, ty2)       = tcSplitFunTys rho1
-        (tvs2, theta2, rho2) = go ty2
-
 badGadtDecl :: Name -> SDoc
 badGadtDecl tc_name
   = vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index d5b4ef28f1..219072e824 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -50,7 +50,6 @@ import GHC.Utils.Lexeme
 import GHC.Utils.Misc
 import GHC.Data.FastString
 import GHC.Utils.Outputable as Outputable
-import GHC.Utils.Monad ( foldrM )
 
 import qualified Data.ByteString as BS
 import Control.Monad( unless, ap )
@@ -595,6 +594,8 @@ cvtConstr (ForallC tvs ctxt con)
     add_cxt (L loc cxt1) (Just (L _ cxt2))
       = Just (L loc (cxt1 ++ cxt2))
 
+    add_forall :: [LHsTyVarBndr Hs.Specificity GhcPs] -> LHsContext GhcPs
+               -> ConDecl GhcPs -> ConDecl GhcPs
     add_forall tvs' cxt' con@(ConDeclGADT { con_qvars = qvars, con_mb_cxt = cxt })
       = con { con_forall = noLoc $ not (null all_tvs)
             , con_qvars  = all_tvs
@@ -609,7 +610,13 @@ cvtConstr (ForallC tvs ctxt con)
       where
         all_tvs = tvs' ++ ex_tvs
 
-    add_forall _    _    (XConDecl nec) = noExtCon nec
+    -- The GadtC and RecGadtC cases of cvtConstr will always return a
+    -- ConDeclGADT, not a ConDeclGADTPrefixPs, so this case is unreachable.
+    -- See Note [GADT abstract syntax] in GHC.Hs.Decls for more on the
+    -- distinction between ConDeclGADT and ConDeclGADTPrefixPs.
+    add_forall _ _ con@(XConDecl (ConDeclGADTPrefixPs {})) =
+      pprPanic "cvtConstr.add_forall: Unexpected ConDeclGADTPrefixPs"
+               (Outputable.ppr con)
 
 cvtConstr (GadtC [] _strtys _ty)
   = failWith (text "GadtC must have at least one constructor name")
@@ -617,9 +624,8 @@ cvtConstr (GadtC [] _strtys _ty)
 cvtConstr (GadtC c strtys ty)
   = do  { c'      <- mapM cNameL c
         ; args    <- mapM cvt_arg strtys
-        ; L _ ty' <- cvtType ty
-        ; c_ty    <- mk_arr_apps args ty'
-        ; returnL $ fst $ mkGadtDecl c' c_ty}
+        ; ty'     <- cvtType ty
+        ; returnL $ mk_gadt_decl c' (PrefixCon args) ty'}
 
 cvtConstr (RecGadtC [] _varstrtys _ty)
   = failWith (text "RecGadtC must have at least one constructor name")
@@ -628,9 +634,19 @@ cvtConstr (RecGadtC c varstrtys ty)
   = do  { c'       <- mapM cNameL c
         ; ty'      <- cvtType ty
         ; rec_flds <- mapM cvt_id_arg varstrtys
-        ; let rec_ty = noLoc (HsFunTy noExtField
-                                           (noLoc $ HsRecTy noExtField rec_flds) ty')
-        ; returnL $ fst $ mkGadtDecl c' rec_ty }
+        ; returnL $ mk_gadt_decl c' (RecCon $ noLoc rec_flds) ty' }
+
+mk_gadt_decl :: [Located RdrName] -> HsConDeclDetails GhcPs -> LHsType GhcPs
+             -> ConDecl GhcPs
+mk_gadt_decl names args res_ty
+  = ConDeclGADT { con_g_ext  = noExtField
+                , con_names  = names
+                , con_forall = noLoc False
+                , con_qvars  = []
+                , con_mb_cxt = Nothing
+                , con_args   = args
+                , con_res_ty = res_ty
+                , con_doc    = Nothing }
 
 cvtSrcUnpackedness :: TH.SourceUnpackedness -> SrcUnpackedness
 cvtSrcUnpackedness NoSourceUnpackedness = NoSrcUnpack
@@ -1647,13 +1663,6 @@ See (among other closed issued) https://gitlab.haskell.org/ghc/ghc/issues/14289
 -}
 -- ---------------------------------------------------------------------
 
--- | Constructs an arrow type with a specified return type
-mk_arr_apps :: [LHsType GhcPs] -> HsType GhcPs -> CvtM (LHsType GhcPs)
-mk_arr_apps tys return_ty = foldrM go return_ty tys >>= returnL
-    where go :: LHsType GhcPs -> HsType GhcPs -> CvtM (HsType GhcPs)
-          go arg ret_ty = do { ret_ty_l <- returnL ret_ty
-                             ; return (HsFunTy noExtField arg ret_ty_l) }
-
 split_ty_app :: TH.Type -> CvtM (TH.Type, [LHsTypeArg GhcPs])
 split_ty_app ty = go ty []
   where
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index 38b20df1f8..22b9e0b571 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -103,6 +103,27 @@ Language
   instantiated through visible type application. More information can be found
   here: :ref:`Manually-defining-inferred-variables`.
 
+* GADT constructor types now properly adhere to :ref:`forall-or-nothing`. As
+  a result, GHC will now reject some GADT constructors that previous versions
+  of GHC would accept, such as the following: ::
+
+    data T where
+      MkT1 :: (forall a. a -> b -> T)
+      MkT2 :: (forall a. a -> T)
+
+  ``MkT1`` and ``MkT2`` are rejected because the lack of an outermost
+  ``forall`` triggers implicit quantification, making the explicit ``forall``s
+  nested. Furthermore, GADT constructors do not permit the use of nested
+  ``forall``s, as explained in :ref:`formal-gadt-syntax`.
+
+  In addition to rejecting nested ``forall``s, GHC is now more stringent about
+  rejecting uses of nested *contexts* in GADT constructors. For example, the
+  following example, which previous versions of GHC would accept, is now
+  rejected:
+
+    data U a where
+      MkU :: (Show a => U a)
+
 Compiler
 ~~~~~~~~
 
diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 38c6e0f441..6b4fc9cef7 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/docs/users_guide/exts/explicit_forall.rst
@@ -45,4 +45,81 @@ Notes:
 
   would warn about the unused type variable `a`.
 
+.. _forall-or-nothing:
+
+The ``forall``-or-nothing rule
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+In certain forms of types, type variables obey what is known as the
+"``forall``-or-nothing" rule: if a type has an outermost, explicit
+``forall``, then all of the type variables in the type must be explicitly
+quantified. These two examples illustrate how the rule works: ::
+
+  f  :: forall a b. a -> b -> b         -- OK, `a` and `b` are explicitly bound
+  g  :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound
+  h  :: forall a. a -> b -> b           -- Rejected, `b` is not in scope
+
+The type signatures for ``f``, ``g``, and ``h`` all begin with an outermost
+``forall``, so every type variable in these signatures must be explicitly
+bound by a ``forall``. Both ``f`` and ``g`` obey the ``forall``-or-nothing
+rule, since they explicitly quantify ``a`` and ``b``. On the other hand,
+``h`` does not explicitly quantify ``b``, so GHC will reject its type
+signature for being improperly scoped.
+
+In places where the ``forall``-or-nothing rule takes effect, if a type does
+*not* have an outermost ``forall``, then any type variables that are not
+explicitly bound by a ``forall`` become implicitly quantified. For example: ::
+
+  i :: a -> b -> b             -- `a` and `b` are implicitly quantified
+  j :: a -> forall b. b -> b   -- `a` is implicitly quantified
+  k :: (forall a. a -> b -> b) -- `b` is implicitly quantified
+
+GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that:
+
+- ``j``'s signature is accepted despite its mixture of implicit and explicit
+  quantification. As long as a ``forall`` is not an outermost one, it is fine
+  to use it among implicitly bound type variables.
+- ``k``'s signature is accepted because the outermost parentheses imply that
+  the ``forall`` is not an outermost ``forall``. The ``forall``-or-nothing
+  rule is one of the few places in GHC where the presence or absence of
+  parentheses can be semantically significant!
+
+The ``forall``-or-nothing rule takes effect in the following places:
+
+- Type signature declarations for functions, values, and class methods
+- Expression type annotations
+- Instance declarations
+- :ref:`class-default-signatures`
+- Type signatures in a :ref:`specialize-pragma` or
+  :ref:`specialize-instance-pragma`
+- :ref:`standalone-kind-signatures`
+- Type signatures for :ref:`gadt` constructors
+- Type signatures for :ref:`pattern-synonyms`
+- :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
+  :ref:`closed-type-families`, and :ref:`assoc-inst`
+- :ref:`rewrite-rules` in which the type variables are explicitly quantified
 
+Notes:
+
+- :ref:`pattern-type-sigs` are a notable example of a place where
+  types do *not* obey the ``forall``-or-nothing rule. For example, GHC will
+  accept the following: ::
+
+    f (g :: forall a. a -> b) x = g x :: b
+
+  Furthermore, :ref:`rewrite-rules` do not obey the ``forall``-or-nothing rule
+  when their type variables are not explicitly quantified: ::
+
+    {-# RULES "f" forall (g :: forall a. a -> b) x. f g x = g x :: b #-}
+
+- GADT constructors are extra particular about their ``forall``s. In addition
+  to adhering to the ``forall``-or-nothing rule, GADT constructors also forbid
+  nested ``forall``s. For example, GHC would reject the following GADT: ::
+
+    data T where
+      MkT :: (forall a. a -> b -> T)
+
+  Because of the lack of an outermost ``forall`` in the type of ``MkT``, the
+  ``b`` would be implicitly quantified. In effect, it would be as if one had
+  written ``MkT :: forall b. (forall a. a -> b -> T)``, which contains nested
+  ``forall``s. See :ref:`formal-gadt-syntax`.
diff --git a/docs/users_guide/exts/gadt_syntax.rst b/docs/users_guide/exts/gadt_syntax.rst
index f89888ff3b..9b20c27ab1 100644
--- a/docs/users_guide/exts/gadt_syntax.rst
+++ b/docs/users_guide/exts/gadt_syntax.rst
@@ -103,6 +103,123 @@ 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.
 
+.. _formal-gadt-syntax:
+
+Formal syntax for GADTs
+~~~~~~~~~~~~~~~~~~~~~~~
+
+To make more precise what is and what is not permitted inside of a GADT-style
+constructor, we provide a BNF-style grammar for GADT below. Note that this
+grammar is subject to change in the future. ::
+
+  gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body
+
+  conids ::= conid
+          |  conid ',' conids
+
+  opt_forall ::= <empty>
+              |  'forall' tv_bndrs '.'
+
+  tv_bndrs ::= <empty>
+            |  tv_bndr tv_bndrs
+
+  tv_bndr ::= tyvar
+           |  '(' tyvar '::' ctype ')'
+
+  opt_ctxt ::= <empty>
+            |  btype '=>'
+            |  '(' ctxt ')' '=>'
+
+  ctxt ::= ctype
+        |  ctype ',' ctxt
+
+  gadt_body ::= prefix_gadt_body
+             |  record_gadt_body
+
+  prefix_gadt_body ::= '(' prefix_gadt_body ')'
+                    |  return_type
+                    |  opt_unpack btype '->' prefix_gadt_body
+
+  record_gadt_body ::= '{' fieldtypes '}' '->' return_type
+
+  fieldtypes ::= <empty>
+              |  fieldnames '::' opt_unpack ctype
+              |  fieldnames '::' opt_unpack ctype ',' fieldtypes
+
+  fieldnames ::= fieldname
+              |  fieldname ',' fieldnames
+
+  opt_unpack ::= opt_bang
+              :  {-# UNPACK #-} opt_bang
+              |  {-# NOUNPACK #-} opt_bang
+
+  opt_bang ::= <empty>
+            |  '!'
+            |  '~'
+
+Where:
+
+- ``btype`` is a type that is not allowed to have an outermost
+  ``forall``/``=>`` unless it is surrounded by parentheses. For example,
+  ``forall a. a`` and ``Eq a => a`` are not legal ``btype``s, but
+  ``(forall a. a)`` and ``(Eq a => a)`` are legal.
+- ``ctype`` is a ``btype`` that has no restrictions on an outermost
+  ``forall``/``=>``, so ``forall a. a`` and ``Eq a => a`` are legal ``ctype``s.
+- ``return_type`` is a type that is not allowed to have ``forall``s, ``=>``s,
+  or ``->``s.
+
+This is a simplified grammar that does not fully delve into all of the
+implementation details of GHC's parser (such as the placement of Haddock
+comments), but it is sufficient to attain an understanding of what is
+syntactically allowed. Some further various observations about this grammar:
+
+- GADT constructor types are currently not permitted to have nested ``forall``s
+  or ``=>``s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be
+  rejected.) As a result, ``gadt_sig`` puts all of its quantification and
+  constraints up front with ``opt_forall`` and ``opt_context``. Note that
+  higher-rank ``forall``s and ``=>``s are only permitted if they do not appear
+  directly to the right of a function arrow in a `prefix_gadt_body`. (e.g.,
+  something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since
+  parentheses separate the ``forall`` from the ``->``.)
+- Furthermore, GADT constructors do not permit outermost parentheses that
+  surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
+  used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since
+  it would treat the ``forall`` as being nested.
+
+  Note that it is acceptable to use parentheses in a ``prefix_gadt_body``.
+  For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is
+  ``MkV2 :: forall a. (a -> V2)``.
+- The function arrows in a ``prefix_gadt_body``, as well as the function
+  arrow in a ``record_gadt_body``, are required to be used infix. For
+  example, ``MkA :: (->) Int A`` would be rejected.
+- GHC uses the function arrows in a ``prefix_gadt_body`` and
+  ``prefix_gadt_body`` to syntactically demarcate the function and result
+  types. Note that GHC does not attempt to be clever about looking through
+  type synonyms here. If you attempt to do this, for instance: ::
+
+    type C = Int -> B
+
+    data B where
+      MkB :: C
+
+  Then GHC will interpret the return type of ``MkB`` to be ``C``, and since
+  GHC requires that the return type must be headed by ``B``, this will be
+  rejected. On the other hand, it is acceptable to use type synonyms within
+  the argument and result types themselves, so the following is permitted: ::
+
+    type B1 = Int
+    type B2 = B
+
+    data B where
+      MkB :: B1 -> B2
+- GHC will accept any combination of ``!``/``~`` and
+  ``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some
+  combinations. For example, GHC will produce a warning if you write
+  ``{-# UNPACK #-} ~Int`` and proceed as if you had written ``Int``.
+
+GADT syntax odds and ends
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
 The rest of this section gives further details about GADT-style data
 type declarations.
 
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
index bb78e2f457..e4acd7a7fd 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
+++ b/testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
@@ -1,7 +1,5 @@
 
-T16326_Fail6.hs:9:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkFoo :: forall a. a -> Foo a
-    • In the definition of data constructor ‘MkFoo’
-      In the data type declaration for ‘Foo’
+T16326_Fail6.hs:9:12: error:
+    Illegal visible, dependent quantification in the type of a term
+    (GHC does not yet support this)
+    In the definition of data constructor ‘MkFoo’
diff --git a/testsuite/tests/gadt/T12087.stderr b/testsuite/tests/gadt/T12087.stderr
index 0039e98657..ef0251a003 100644
--- a/testsuite/tests/gadt/T12087.stderr
+++ b/testsuite/tests/gadt/T12087.stderr
@@ -1,35 +1,20 @@
 
-T12087.hs:6:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkF1 :: forall a. (Ord a, Eq a) => a -> F1 a
-    • In the definition of data constructor ‘MkF1’
-      In the data type declaration for ‘F1’
+T12087.hs:6:20: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkF1’
 
-T12087.hs:9:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkF2 :: forall a. (Ord a, Eq a) => a -> F2 a
-    • In the definition of data constructor ‘MkF2’
-      In the data type declaration for ‘F2’
+T12087.hs:9:25: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkF2’
 
-T12087.hs:12:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkF3 :: forall a b. (Eq a, Eq b) => a -> b -> F3 a
-    • In the definition of data constructor ‘MkF3’
-      In the data type declaration for ‘F3’
+T12087.hs:12:34: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkF3’
 
-T12087.hs:15:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkF4 :: forall a b. (Eq a, Eq b) => a -> b -> F4 a
-    • In the definition of data constructor ‘MkF4’
-      In the data type declaration for ‘F4’
+T12087.hs:15:36: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkF4’
 
-T12087.hs:18:3: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        MkF5 :: forall a b. Int -> Int -> a -> Int -> Int -> b -> F5 a
-    • In the definition of data constructor ‘MkF5’
-      In the data type declaration for ‘F5’
+T12087.hs:18:25: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkF5’
diff --git a/testsuite/tests/gadt/T14320.hs b/testsuite/tests/gadt/T14320.hs
index 77c68ee92e..270c92c37c 100644
--- a/testsuite/tests/gadt/T14320.hs
+++ b/testsuite/tests/gadt/T14320.hs
@@ -10,8 +10,8 @@ data Exp :: Type where
 newtype TypedExp :: Type -> Type where
   TEGood ::  forall a . (Exp -> (TypedExp a))
 
--- The only difference here is that the type is wrapped in parentheses,
--- but GHC 8.0.1 rejects this program
+-- The presence of outer parentheses makes the `forall` nested, and
+-- GADTs do not permit nested `forall`s.
 --
 newtype TypedExpToo :: Type -> Type where
   TEBad  :: (forall a . (Exp -> (TypedExpToo a)))
diff --git a/testsuite/tests/gadt/T14320.stderr b/testsuite/tests/gadt/T14320.stderr
new file mode 100644
index 0000000000..9cfb6ed9fc
--- /dev/null
+++ b/testsuite/tests/gadt/T14320.stderr
@@ -0,0 +1,4 @@
+
+T14320.hs:17:14: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘TEBad’
diff --git a/testsuite/tests/gadt/T16427.stderr b/testsuite/tests/gadt/T16427.stderr
index 1c80190e29..b7288c9cd6 100644
--- a/testsuite/tests/gadt/T16427.stderr
+++ b/testsuite/tests/gadt/T16427.stderr
@@ -1,7 +1,4 @@
 
-T16427.hs:5:14: error:
-    • GADT constructor type signature cannot contain nested ‘forall’s or contexts
-      Suggestion: instead use this type signature:
-        C :: forall b. Int -> b -> D
-    • In the definition of data constructor ‘C’
-      In the data type declaration for ‘D’
+T16427.hs:5:26: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘C’
diff --git a/testsuite/tests/gadt/T18191.hs b/testsuite/tests/gadt/T18191.hs
new file mode 100644
index 0000000000..e30c7ad5b1
--- /dev/null
+++ b/testsuite/tests/gadt/T18191.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module T18191 where
+
+data T where
+  MkT :: (forall a. a -> b -> T)
+
+data S a where
+  MkS :: (forall a. S a)
+
+data U a where
+  MkU :: (Show a => U a)
+
+data Z a where
+  MkZ1 :: forall a. forall b. { unZ1 :: (a, b) } -> Z (a, b)
+  MkZ2 :: Eq a => Eq b => { unZ1 :: (a, b) } -> Z (a, b)
diff --git a/testsuite/tests/gadt/T18191.stderr b/testsuite/tests/gadt/T18191.stderr
new file mode 100644
index 0000000000..b8c6c60bdc
--- /dev/null
+++ b/testsuite/tests/gadt/T18191.stderr
@@ -0,0 +1,20 @@
+
+T18191.hs:6:11: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkT’
+
+T18191.hs:9:11: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkS’
+
+T18191.hs:12:11: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkU’
+
+T18191.hs:15:21: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkZ1’
+
+T18191.hs:16:19: error:
+    GADT constructor type signature cannot contain nested ‘forall’s or contexts
+    In the definition of data constructor ‘MkZ2’
diff --git a/testsuite/tests/gadt/all.T b/testsuite/tests/gadt/all.T
index 29bde94100..3c146820ae 100644
--- a/testsuite/tests/gadt/all.T
+++ b/testsuite/tests/gadt/all.T
@@ -113,10 +113,11 @@ test('T7558', normal, compile_fail, [''])
 test('T9380', normal, compile_and_run, [''])
 test('T12087', normal, compile_fail, [''])
 test('T12468', normal, compile_fail, [''])
-test('T14320', normal, compile, [''])
+test('T14320', normal, compile_fail, [''])
 test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
 test('T14808', normal, compile, [''])
 test('T15009', normal, compile, [''])
 test('T15558', normal, compile, [''])
 test('T16427', normal, compile_fail, [''])
 test('T17423', expect_broken(17423), compile_and_run, [''])
+test('T18191', normal, compile_fail, [''])
diff --git a/testsuite/tests/ghc-api/annotations/T10399.stdout b/testsuite/tests/ghc-api/annotations/T10399.stdout
index a71abc4139..7588393264 100644
--- a/testsuite/tests/ghc-api/annotations/T10399.stdout
+++ b/testsuite/tests/ghc-api/annotations/T10399.stdout
@@ -34,9 +34,9 @@
 ((Test10399.hs:12:30,AnnComma), [Test10399.hs:12:30]),
 ((Test10399.hs:12:31-32,AnnCloseP), [Test10399.hs:12:32]),
 ((Test10399.hs:12:31-32,AnnOpenP), [Test10399.hs:12:31]),
-((Test10399.hs:(14,1)-(18,55),AnnData), [Test10399.hs:14:1-4]),
-((Test10399.hs:(14,1)-(18,55),AnnSemi), [Test10399.hs:20:1]),
-((Test10399.hs:(14,1)-(18,55),AnnWhere), [Test10399.hs:14:21-25]),
+((Test10399.hs:(14,1)-(18,53),AnnData), [Test10399.hs:14:1-4]),
+((Test10399.hs:(14,1)-(18,53),AnnSemi), [Test10399.hs:20:1]),
+((Test10399.hs:(14,1)-(18,53),AnnWhere), [Test10399.hs:14:21-25]),
 ((Test10399.hs:15:5-64,AnnDcolon), [Test10399.hs:15:11-12]),
 ((Test10399.hs:15:5-64,AnnSemi), [Test10399.hs:16:5]),
 ((Test10399.hs:15:14-64,AnnDot), [Test10399.hs:15:23]),
@@ -48,37 +48,29 @@
 ((Test10399.hs:15:45-46,AnnBang), [Test10399.hs:15:45]),
 ((Test10399.hs:15:45-46,AnnRarrow), [Test10399.hs:15:48-49]),
 ((Test10399.hs:15:45-64,AnnRarrow), [Test10399.hs:15:48-49]),
-((Test10399.hs:(16,5)-(17,69),AnnCloseP), [Test10399.hs:17:69]),
-((Test10399.hs:(16,5)-(17,69),AnnDcolon), [Test10399.hs:16:12-13]),
-((Test10399.hs:(16,5)-(17,69),AnnOpenP), [Test10399.hs:16:27]),
-((Test10399.hs:(16,5)-(17,69),AnnSemi), [Test10399.hs:18:5]),
-((Test10399.hs:(16,15)-(17,69),AnnDot), [Test10399.hs:16:25]),
-((Test10399.hs:(16,15)-(17,69),AnnForall), [Test10399.hs:16:15-20]),
-((Test10399.hs:(16,27)-(17,69),AnnCloseP), [Test10399.hs:17:69]),
-((Test10399.hs:(16,27)-(17,69),AnnOpenP), [Test10399.hs:16:27]),
-((Test10399.hs:16:28-43,AnnCloseP), [Test10399.hs:16:43, Test10399.hs:16:43]),
-((Test10399.hs:16:28-43,AnnDarrow), [Test10399.hs:16:45-46]),
-((Test10399.hs:16:28-43,AnnOpenP), [Test10399.hs:16:28, Test10399.hs:16:28]),
-((Test10399.hs:16:30-33,AnnComma), [Test10399.hs:16:34]),
-((Test10399.hs:16:48,AnnRarrow), [Test10399.hs:16:50-51]),
-((Test10399.hs:(16,48)-(17,68),AnnRarrow), [Test10399.hs:16:50-51]),
-((Test10399.hs:16:53-66,AnnRarrow), [Test10399.hs:17:45-46]),
-((Test10399.hs:(16,53)-(17,68),AnnRarrow), [Test10399.hs:17:45-46]),
-((Test10399.hs:17:48,AnnRarrow), [Test10399.hs:17:50-51]),
-((Test10399.hs:17:48-68,AnnRarrow), [Test10399.hs:17:50-51]),
-((Test10399.hs:17:66-68,AnnCloseS), [Test10399.hs:17:68]),
-((Test10399.hs:17:66-68,AnnOpenS), [Test10399.hs:17:66]),
-((Test10399.hs:18:5-55,AnnCloseP), [Test10399.hs:18:55]),
-((Test10399.hs:18:5-55,AnnDcolon), [Test10399.hs:18:16-17]),
-((Test10399.hs:18:5-55,AnnOpenP), [Test10399.hs:18:19]),
-((Test10399.hs:18:19-55,AnnCloseP), [Test10399.hs:18:55]),
-((Test10399.hs:18:19-55,AnnOpenP), [Test10399.hs:18:19]),
-((Test10399.hs:18:20-54,AnnDot), [Test10399.hs:18:29]),
-((Test10399.hs:18:20-54,AnnForall), [Test10399.hs:18:20-25]),
-((Test10399.hs:18:31-36,AnnCloseP), [Test10399.hs:18:36]),
-((Test10399.hs:18:31-36,AnnOpenP), [Test10399.hs:18:31]),
-((Test10399.hs:18:31-36,AnnRarrow), [Test10399.hs:18:38-39]),
-((Test10399.hs:18:31-54,AnnRarrow), [Test10399.hs:18:38-39]),
+((Test10399.hs:(16,5)-(17,67),AnnDcolon), [Test10399.hs:16:12-13]),
+((Test10399.hs:(16,5)-(17,67),AnnSemi), [Test10399.hs:18:5]),
+((Test10399.hs:(16,15)-(17,67),AnnDot), [Test10399.hs:16:25]),
+((Test10399.hs:(16,15)-(17,67),AnnForall), [Test10399.hs:16:15-20]),
+((Test10399.hs:16:27-42,AnnCloseP), [Test10399.hs:16:42, Test10399.hs:16:42]),
+((Test10399.hs:16:27-42,AnnDarrow), [Test10399.hs:16:44-45]),
+((Test10399.hs:16:27-42,AnnOpenP), [Test10399.hs:16:27, Test10399.hs:16:27]),
+((Test10399.hs:16:29-32,AnnComma), [Test10399.hs:16:33]),
+((Test10399.hs:16:47,AnnRarrow), [Test10399.hs:16:49-50]),
+((Test10399.hs:(16,47)-(17,67),AnnRarrow), [Test10399.hs:16:49-50]),
+((Test10399.hs:16:52-65,AnnRarrow), [Test10399.hs:17:44-45]),
+((Test10399.hs:(16,52)-(17,67),AnnRarrow), [Test10399.hs:17:44-45]),
+((Test10399.hs:17:47,AnnRarrow), [Test10399.hs:17:49-50]),
+((Test10399.hs:17:47-67,AnnRarrow), [Test10399.hs:17:49-50]),
+((Test10399.hs:17:65-67,AnnCloseS), [Test10399.hs:17:67]),
+((Test10399.hs:17:65-67,AnnOpenS), [Test10399.hs:17:65]),
+((Test10399.hs:18:5-53,AnnDcolon), [Test10399.hs:18:16-17]),
+((Test10399.hs:18:19-53,AnnDot), [Test10399.hs:18:28]),
+((Test10399.hs:18:19-53,AnnForall), [Test10399.hs:18:19-24]),
+((Test10399.hs:18:30-35,AnnCloseP), [Test10399.hs:18:35]),
+((Test10399.hs:18:30-35,AnnOpenP), [Test10399.hs:18:30]),
+((Test10399.hs:18:30-35,AnnRarrow), [Test10399.hs:18:37-38]),
+((Test10399.hs:18:30-53,AnnRarrow), [Test10399.hs:18:37-38]),
 ((Test10399.hs:20:1-25,AnnCloseQ), [Test10399.hs:20:24-25]),
 ((Test10399.hs:20:1-25,AnnOpen), [Test10399.hs:20:1-3]),
 ((Test10399.hs:20:1-25,AnnSemi), [Test10399.hs:22:1]),
diff --git a/testsuite/tests/ghc-api/annotations/Test10399.hs b/testsuite/tests/ghc-api/annotations/Test10399.hs
index 6a35712bfd..bb3265000d 100644
--- a/testsuite/tests/ghc-api/annotations/Test10399.hs
+++ b/testsuite/tests/ghc-api/annotations/Test10399.hs
@@ -13,9 +13,9 @@ mkPoli = mkBila . map ((,,(),,()) <$> P.base <*> P.pos <*> P.form)
 
 data MaybeDefault v where
     SetTo :: forall v . ( Eq v, Show v ) => !v -> MaybeDefault v
-    SetTo4 :: forall v a. (( Eq v, Show v ) => v -> MaybeDefault v
-                                            -> a -> MaybeDefault [a])
-    TestParens :: (forall v . (Eq v) -> MaybeDefault v)
+    SetTo4 :: forall v a. ( Eq v, Show v ) => v -> MaybeDefault v
+                                           -> a -> MaybeDefault [a]
+    TestParens :: forall v . (Eq v) -> MaybeDefault v
 
 [t| Map.Map T.Text $tc |]
 
diff --git a/testsuite/tests/parser/should_compile/T15323.hs b/testsuite/tests/parser/should_compile/T15323.hs
index ffc8ad85f0..42eb616141 100644
--- a/testsuite/tests/parser/should_compile/T15323.hs
+++ b/testsuite/tests/parser/should_compile/T15323.hs
@@ -3,4 +3,4 @@
 module T15323 where
 
 data MaybeDefault v where
-    TestParens  :: (forall v . (Eq v) => MaybeDefault v)
+    TestParens  :: forall v . (Eq v) => MaybeDefault v
diff --git a/testsuite/tests/parser/should_compile/T15323.stderr b/testsuite/tests/parser/should_compile/T15323.stderr
index c69f94afba..c07f2d6a43 100644
--- a/testsuite/tests/parser/should_compile/T15323.stderr
+++ b/testsuite/tests/parser/should_compile/T15323.stderr
@@ -8,7 +8,7 @@
     {ModuleName: T15323}))
   (Nothing)
   []
-  [({ T15323.hs:(5,1)-(6,56) }
+  [({ T15323.hs:(5,1)-(6,54) }
     (TyClD
      (NoExtField)
      (DataDecl
@@ -33,63 +33,67 @@
         [])
        (Nothing)
        (Nothing)
-       [({ T15323.hs:6:5-56 }
-         (ConDeclGADT
-          (NoExtField)
-          [({ T15323.hs:6:5-14 }
-            (Unqual
-             {OccName: TestParens}))]
-          ({ T15323.hs:6:21-55 }
-           (True))
-          [({ T15323.hs:6:28 }
-            (UserTyVar
-             (NoExtField)
-             (SpecifiedSpec)
-             ({ T15323.hs:6:28 }
-              (Unqual
-               {OccName: v}))))]
-          (Just
-           ({ T15323.hs:6:32-37 }
-            [({ T15323.hs:6:32-37 }
-              (HsParTy
-               (NoExtField)
-               ({ T15323.hs:6:33-36 }
-                (HsAppTy
-                 (NoExtField)
-                 ({ T15323.hs:6:33-34 }
-                  (HsTyVar
-                   (NoExtField)
-                   (NotPromoted)
-                   ({ T15323.hs:6:33-34 }
-                    (Unqual
-                     {OccName: Eq}))))
-                 ({ T15323.hs:6:36 }
-                  (HsTyVar
-                   (NoExtField)
-                   (NotPromoted)
-                   ({ T15323.hs:6:36 }
-                    (Unqual
-                     {OccName: v}))))))))]))
-          (PrefixCon
-           [])
-          ({ T15323.hs:6:42-55 }
-           (HsAppTy
+       [({ T15323.hs:6:5-54 }
+         (XConDecl
+          (ConDeclGADTPrefixPs
+           [({ T15323.hs:6:5-14 }
+             (Unqual
+              {OccName: TestParens}))]
+           (HsIB
             (NoExtField)
-            ({ T15323.hs:6:42-53 }
-             (HsTyVar
+            ({ T15323.hs:6:20-54 }
+             (HsForAllTy
               (NoExtField)
-              (NotPromoted)
-              ({ T15323.hs:6:42-53 }
-               (Unqual
-                {OccName: MaybeDefault}))))
-            ({ T15323.hs:6:55 }
-             (HsTyVar
-              (NoExtField)
-              (NotPromoted)
-              ({ T15323.hs:6:55 }
-               (Unqual
-                {OccName: v}))))))
-          (Nothing)))]
+              (ForallInvis)
+              [({ T15323.hs:6:27 }
+                (UserTyVar
+                 (NoExtField)
+                 (SpecifiedSpec)
+                 ({ T15323.hs:6:27 }
+                  (Unqual
+                   {OccName: v}))))]
+              ({ T15323.hs:6:31-54 }
+               (HsQualTy
+                (NoExtField)
+                ({ T15323.hs:6:31-36 }
+                 [({ T15323.hs:6:31-36 }
+                   (HsParTy
+                    (NoExtField)
+                    ({ T15323.hs:6:32-35 }
+                     (HsAppTy
+                      (NoExtField)
+                      ({ T15323.hs:6:32-33 }
+                       (HsTyVar
+                        (NoExtField)
+                        (NotPromoted)
+                        ({ T15323.hs:6:32-33 }
+                         (Unqual
+                          {OccName: Eq}))))
+                      ({ T15323.hs:6:35 }
+                       (HsTyVar
+                        (NoExtField)
+                        (NotPromoted)
+                        ({ T15323.hs:6:35 }
+                         (Unqual
+                          {OccName: v}))))))))])
+                ({ T15323.hs:6:41-54 }
+                 (HsAppTy
+                  (NoExtField)
+                  ({ T15323.hs:6:41-52 }
+                   (HsTyVar
+                    (NoExtField)
+                    (NotPromoted)
+                    ({ T15323.hs:6:41-52 }
+                     (Unqual
+                      {OccName: MaybeDefault}))))
+                  ({ T15323.hs:6:54 }
+                   (HsTyVar
+                    (NoExtField)
+                    (NotPromoted)
+                    ({ T15323.hs:6:54 }
+                     (Unqual
+                      {OccName: v})))))))))))
+           (Nothing))))]
        ({ <no location info> }
         [])))))]
   (Nothing)
diff --git a/utils/haddock b/utils/haddock
-Subproject 792b82861a8abd03579a281dfdcbbb708166899
+Subproject c849a39a6996221541a47a46a8b8826977ed8a5