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 theseforalls/contexts nested, and GADTs do not support nestedforalls/contexts at present. -
A "
forall-or-nothing rule" section that describes exactly what theforall-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 likesplitLHsSigmaTy, except that it avoids splitting apart any parentheses, which can be syntactically significant for GADT types. SeeNote [No nested foralls or contexts in GADT constructors]inGHC.Hs.Type. -
ConDeclGADTPrefixPs, an extension constructor forXConDecl, was introduced so thatGHC.Parser.PostProcess.mkGadtDeclcan return it when given a prefix GADT constructor. UnlikeConDeclGADT,ConDeclGADTPrefixPsdoes not split the GADT type into its argument and result types, as this cannot be done until after the type is renamed (seeNote [GADT abstract syntax]inGHC.Hs.Declsfor why this is the case). -
GHC.Renamer.Module.rnConDeclnow has an additional case forConDeclGADTPrefixPsthat (1) splits apart the fullLHsTypeinto itsforalls, context, argument types, and result type, and (2) checks for nestedforalls/contexts. Step (2) used to be performed the typechecker (inGHC.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 theT16326_Fail6test case.
Fixes #18191 (closed). Bumps the Haddock submodule.