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
forall
and/or context in a GADT constructor is not allowed to be surrounded by parentheses. Doing so would make theseforall
s/contexts nested, and GADTs do not support nestedforall
s/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.mkGadtDecl
can return it when given a prefix GADT constructor. UnlikeConDeclGADT
,ConDeclGADTPrefixPs
does 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.Decls
for why this is the case). -
GHC.Renamer.Module.rnConDecl
now has an additional case forConDeclGADTPrefixPs
that (1) splits apart the fullLHsType
into itsforall
s, context, argument types, and result type, and (2) checks for nestedforall
s/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_Fail6
test case.
Fixes #18191 (closed). Bumps the Haddock submodule.