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, 61 insertions, 14 deletions

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)