Make GADT constructors adhere to the forall-or-nothing rule properly
Issue #18191 (closed) 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 (closed): the outermost
foralland/or context in a GADT constructor is not allowed to be surrounded by parentheses. Doing so would make these
foralls/contexts nested, and GADTs do not support nested
foralls/contexts at present.
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
ConDeclGADTPrefixPs, an extension constructor for
XConDecl, was introduced so that
GHC.Parser.PostProcess.mkGadtDeclcan return it when given a prefix GADT constructor. Unlike
ConDeclGADTPrefixPsdoes 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.Declsfor why this is the case).
GHC.Renamer.Module.rnConDeclnow has an additional case for
ConDeclGADTPrefixPsthat (1) splits apart the full
foralls, context, argument types, and result type, and (2) checks for nested
foralls/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
Fixes #18191 (closed). Bumps the Haddock submodule.