The types of both forms of GADT constructors are very structured, as they
must consist of the quantified type variables (if provided), followed by the
context (if provided), followed by the argument types (if provided), followed
by the result type. (See "Wrinkle: No nested foralls or contexts" below for
more discussion on the restrictions imposed here.) As a result, instead of
storing the type of a GADT constructor as a single LHsType, we split it up
into its constituent components for easier access.
There are two broad ways to classify GADT constructors:
* Record-syntax constructors. For example:
data T a where
K :: forall a. Ord a => { x :: [a], ... } -> T a
* Prefix constructors, which do not use record syntax. For example:
data T a where
K :: forall a. Ord a => [a] -> ... -> T a
This distinction is recorded in the `con_args :: HsConDetails pass`, which
tracks if we're dealing with a RecCon or PrefixCon. It is easy to distinguish
the two in the AST since record GADT constructors use HsRecTy. This distinction
is made in GHC.Parser.PostProcess.mkGadtDecl.
It is worth elaborating a bit more on the process of splitting the argument
types of a GADT constructor, since there are some non-obvious details involved.
While splitting the argument types of a record GADT constructor is easy (they
are stored in an HsRecTy), splitting the arguments of a prefix GADT constructor
is trickier. The basic idea is that we must split along the outermost function
arrows ((->) and (%1 ->)) in the type, which GHC.Hs.Type.splitHsFunType
accomplishes. But what about type operators? Consider:
C :: a :*: b -> a :*: b -> a :+: b
This could parse in many different ways depending on the precedences of each
type operator. In particular, if (:*:) were to have lower precedence than (->),
then it could very well parse like this:
a :*: ((b -> a) :*: ((b -> a) :+: b)))
This would give the false impression that the whole type is part of one large
return type, with no arguments. Note that we do not fully resolve the exact
precedences of each user-defined type operator until the renamer, so this a
more difficult task for the parser.
Fortunately, there is no risk of the above happening. GHC's parser gives
special treatment to function arrows, and as a result, they are always parsed
with a lower precedence than any other type operator. As a result, the type
above is actually parsed like this:
(a :*: b) -> ((a :*: b) -> (a :+: b))
While we won't know the exact precedences of (:*:) and (:+:) until the renamer,
all we are concerned about in the parser is identifying the overall shape of
the argument and result types, which we can accomplish by piggybacking on the
special treatment given to function arrows. In a future where function arrows
aren't given special status in the parser, we will likely have to modify
GHC.Parser.PostProcess.mkHsOpTyPV to preserve this trick.
Wrinkle: No nested foralls or contexts
GADT constructors provide some freedom to change the order of foralls in their
types (see Note [DataCon user type variable binders] in GHC.Core.DataCon), but
this freedom is still limited. GADTs still require that all quantification
occurs "prenex". That is, any explicitly quantified type variables must occur
at the front of the GADT type, followed by any contexts, followed by the body of
the GADT type, in precisely that order. For instance:
data T where
MkT1 :: forall a b. (Eq a, Eq b) => a -> b -> T
OK
MkT2 :: forall a. Eq a => forall b. a -> b -> T
Rejected, `forall b` is nested
MkT3 :: forall a b. Eq a => Eq b => a -> b -> T
Rejected, `Eq b` is nested
MkT4 :: Int -> forall a. a -> T
Rejected, `forall a` is nested
MkT5 :: forall a. Int -> Eq a => a -> T
Rejected, `Eq a` is nested
MkT6 :: (forall a. a -> T)
Rejected, `forall a` is nested due to the surrounding parentheses
MkT7 :: (Eq a => a -> t)
Rejected, `Eq a` is nested due to the surrounding parentheses
For the full details, see the "Formal syntax for GADTs" section of the GHC
User's Guide. GHC enforces that GADT constructors do not have nested `forall`s
or contexts in two parts:
1. GHC, in the process of splitting apart a GADT's type,
extracts out the leading `forall` and context (if they are provided). To
accomplish this splitting, the renamer uses the
GHC.Hs.Type.splitLHsGADTPrefixTy function, which is careful not to remove
parentheses surrounding the leading `forall` or context (as these
parentheses can be syntactically significant). If the third result returned
by splitLHsGADTPrefixTy contains any `forall`s or contexts, then they must
be nested, so they will be rejected.
Note that this step applies to both prefix and record GADTs alike, as they
both have syntax which permits `forall`s and contexts. The difference is
where this step happens:
* For prefix GADTs, this happens in the renamer (in rnConDecl), as we cannot
split until after the type operator fixities have been resolved.
* For record GADTs, this happens in the parser (in mkGadtDecl).
2. If the GADT type is prefix, the renamer (in the ConDeclGADTPrefixPs case of
rnConDecl) will then check for nested `forall`s/contexts in the body of a
prefix GADT type, after it has determined what all of the argument types are.
This step is necessary to catch examples like MkT4 above, where the nested
quantification occurs after a visible argument type.