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.

1 files changed, 24 insertions, 15 deletions

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