Skip to content

Make GADT constructors adhere to the forall-or-nothing rule properly

Ryan Scott requested to merge wip/T18191 into master

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 these foralls/contexts nested, and GADTs do not support nested foralls/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 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 T16326_Fail6 test case.

Fixes #18191 (closed). Bumps the Haddock submodule.

Edited by Ryan Scott

Merge request reports