Commit 50bab0e8 authored by Ryan Scott's avatar Ryan Scott

WIP: T18191

TODO RGS: Write that commit message

[ci skip]
parent 568d7279
......@@ -57,8 +57,9 @@ module GHC.Hs.Types (
hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy,
splitLHsForAllTyInvis, splitLHsQualTy, splitLHsSigmaTyInvis,
splitHsFunType, hsTyGetAppHead_maybe,
splitLHsForAllTyInvis, splitLHsQualTy,
splitLHsSigmaTyInvis, splitNestedLHsSigmaTysInvis,
splitLHsFunTys, hsTyGetAppHead_maybe,
mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
ignoreParens, hsSigType, hsSigWcType, hsPatSigType,
hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
......@@ -1227,18 +1228,44 @@ mkHsAppKindTy ext ty k
-}
---------------------------------
-- splitHsFunType decomposes a type (t1 -> t2 ... -> tn)
-- Breaks up any parens in the result type:
-- splitHsFunType (a -> (b -> c)) = ([a,b], c)
splitHsFunType :: LHsType GhcRn -> ([LHsType GhcRn], LHsType GhcRn)
splitHsFunType (L _ (HsParTy _ ty))
= splitHsFunType ty
splitHsFunType (L _ (HsFunTy _ x y))
| (args, res) <- splitHsFunType y
-- | 'splitLHsFunTys' decomposes a type @t1 -> t2 ... -> tn@ into the argument
-- and result types. For example:
--
-- @
-- 'splitLHsFunTys' (a -> b -> c) = ([a,b], c)
-- @
--
-- Note that this function looks through parentheses, so it will work on types
-- such as @(a -> (b -> c))@. The downside to this is that it is not
-- generally possible to take the returned types and reconstruct the original
-- type (parentheses and all) from them.
splitLHsFunTys :: LHsType GhcRn -> ([LHsType GhcRn], LHsType GhcRn)
splitLHsFunTys (L _ (HsParTy _ ty))
= splitLHsFunTys ty
splitLHsFunTys (L _ (HsFunTy _ x y))
| (args, res) <- splitLHsFunTys y
= (x:args, res)
splitHsFunType other = ([], other)
splitLHsFunTys other = ([], other)
-- | Returns 'Just (arg_ty, res_ty)@ if the supplied type is an 'HsFunTy',
-- where @arg_ty@ and @res_ty@ are the decomposed argument and result types,
-- respectively. Returns 'Nothing' otherwise. For example:
--
-- @
-- 'splitLHsFunTy_maybe' (a -> b) = 'Just' (a, b)
-- 'splitLHsFunTy_maybe' [a] = 'Nothing'
-- @
--
-- Note that this function looks through parentheses, so it will work on types
-- such as @((a -> b))@. The downside to this is that it is not
-- generally possible to take the returned types and reconstruct the original
-- type (parentheses and all) from them.
splitLHsFunTy_maybe :: LHsType pass -> Maybe (LHsType pass, LHsType pass)
splitLHsFunTy_maybe (L _ (HsParTy _ ty)) = splitLHsFunTy_maybe ty
splitLHsFunTy_maybe (L _ (HsFunTy _ x y)) = Just (x, y)
splitLHsFunTy_maybe _ = Nothing
-- retrieve the name of the "head" of a nested type application
-- somewhat like splitHsAppTys, but a little more thorough
......@@ -1332,6 +1359,67 @@ splitLHsSigmaTyInvis ty
, (ctxt, ty2) <- splitLHsQualTy ty1
= (tvs, ctxt, ty2)
-- | Decompose a type's @forall@s and contexts from its body, possibly looking
-- underneath 'HsFunTy's in the process. For example:
--
-- @
-- 'splitNestedLHsSigmaTysInvis' (forall a. a -> Show a => forall b. b -> a)
-- = ([a, b], [Show a], [a -> b -> a])
-- @
--
-- Note that this function looks through parentheses, so it will work on types
-- such as @(forall a. <...>)@. The downside to this is that it is not
-- generally possible to take the returned types and reconstruct the original
-- type (parentheses and all) from them.
splitNestedLHsSigmaTysInvis ::
LHsType (GhcPass p)
-> ([LHsTyVarBndr (GhcPass p)], LHsContext (GhcPass p), LHsType (GhcPass p))
splitNestedLHsSigmaTysInvis ty
-- If there's a forall, split it apart and try splitting the rho type
-- underneath it.
| Just (arg_tys, tvs1, theta1, rho1) <- deepSplitLHsSigmaTyInvis_maybe ty
= let (tvs2, theta2, rho2) = splitNestedLHsSigmaTysInvis rho1
in ( tvs1 ++ tvs2
, append_lhs_contexts theta1 theta2
, foldr mk_lhs_fun_ty rho2 arg_tys )
-- If there's no forall, we're done.
| otherwise = ([], noLHsContext, ty)
where
append_lhs_contexts :: LHsContext (GhcPass p) -> LHsContext (GhcPass p)
-> LHsContext (GhcPass p)
append_lhs_contexts (L _ ctxt1) (L _ ctxt2) = noLoc $ ctxt1 ++ ctxt2
mk_lhs_fun_ty :: LHsType (GhcPass p) -> LHsType (GhcPass p)
-> LHsType (GhcPass p)
mk_lhs_fun_ty arg_ty res_ty = noLoc $ HsFunTy noExtField arg_ty res_ty
-- | Helper function for 'deepSplitLHsSigmaTyInvis_maybe' that decomposes a
-- function type's arguments, followed by any @forall@s and contexts that
-- appear after the last function arrow. For example:
--
-- @
-- 'deepSplitLHsSigmaTyInvis_maybe' (Int -> Char -> forall a. Show a => a -> b)
-- = ([Int, Char], [a], [Show a], [a -> b])
-- @
--
-- Note that this function looks through parentheses, so it will work on types
-- such as @(forall a. <...>)@. The downside to this is that it is not
-- generally possible to take the returned types and reconstruct the original
-- type (parentheses and all) from them.
deepSplitLHsSigmaTyInvis_maybe ::
LHsType pass
-> Maybe ([LHsType pass], [LHsTyVarBndr pass], LHsContext pass, LHsType pass)
deepSplitLHsSigmaTyInvis_maybe ty
| Just (arg_ty, res_ty) <- splitLHsFunTy_maybe ty
, Just (arg_tys, tvs, theta, rho) <- deepSplitLHsSigmaTyInvis_maybe res_ty
= Just (arg_ty:arg_tys, tvs, theta, rho)
| (tvs, theta, rho) <- splitLHsSigmaTyInvis ty
, not (null tvs && null (unLoc theta))
= Just ([], tvs, theta, rho)
| otherwise = Nothing
-- | Decompose a type of the form @forall <tvs>. body@ into its constituent
-- parts. Note that only /invisible/ @forall@s
-- (i.e., @forall a.@, with a dot) are split apart; /visible/ @forall@s
......
......@@ -2235,9 +2235,8 @@ gadt_constr :: { LConDecl GhcPs }
-- see Note [Difference in parsing GADT and data constructors]
-- Returns a list because of: C,D :: ty
: con_list '::' sigtypedoc
{% let (gadt,anns) = mkGadtDecl (unLoc $1) $3
in ams (sLL $1 $> gadt)
(mu AnnDcolon $2:anns) }
{% ams (sLL $1 $> (mkGadtDecl (unLoc $1) $3))
[mu AnnDcolon $2] }
{- Note [Difference in parsing GADT and data constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......
......@@ -663,30 +663,41 @@ mkConDeclH98 name mb_forall mb_cxt args
, con_args = args
, con_doc = Nothing }
-- Construct a GADT-style data constructor from the constructor names and their
-- type. Does not perform any validity checking, as that it done later in
-- GHC.Rename.Module.rnConDecl.
mkGadtDecl :: [Located RdrName]
-> LHsType GhcPs -- Always a HsForAllTy
-> (ConDecl GhcPs, [AddAnn])
-> ConDecl GhcPs
mkGadtDecl names ty
= (ConDeclGADT { con_g_ext = noExtField
, con_names = names
, con_forall = L l $ isLHsForAllTy ty'
, con_qvars = mkHsQTvs tvs
, con_mb_cxt = mcxt
, con_args = args
, con_res_ty = res_ty
, con_doc = Nothing }
, anns1 ++ anns2)
= ConDeclGADT { con_g_ext = noExtField
, con_names = names
, con_forall = L (getLoc ty) $ isJust mtvs
, con_qvars = mkHsQTvs $ fromMaybe [] mtvs
, con_mb_cxt = mcxt
, con_args = args
, con_res_ty = res_ty
, con_doc = Nothing }
where
(ty'@(L l _),anns1) = peel_parens ty []
(tvs, rho) = splitLHsForAllTyInvis ty'
(mcxt, tau, anns2) = split_rho rho []
split_rho (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau })) ann
= (Just cxt, tau, ann)
split_rho (L l (HsParTy _ ty)) ann
= split_rho ty (ann++mkParensApiAnn l)
split_rho tau ann
= (Nothing, tau, ann)
(mtvs, rho) = split_sigma ty
(mcxt, tau) = split_rho rho
-- NB: We do not use splitLHsForAllTyInvis below, since that looks through
-- parentheses...
split_sigma (L _ (HsForAllTy { hst_fvf = ForallInvis, hst_bndrs = bndrs
, hst_body = rho }))
= (Just bndrs, rho)
split_sigma sigma
= (Nothing, sigma)
-- ...similarly, we do not use splitLHsQualTy below, since that also looks
-- through parentheses.
-- See Note [No nested foralls or contexts in GADT constructors] for why
-- this is important.
split_rho (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau }))
= (Just cxt, tau)
split_rho tau
= (Nothing, tau)
(args, res_ty) = split_tau tau
......@@ -696,10 +707,43 @@ mkGadtDecl names ty
split_tau tau
= (PrefixCon [], tau)
peel_parens (L l (HsParTy _ ty)) ann = peel_parens ty
(ann++mkParensApiAnn l)
peel_parens ty ann = (ty, ann)
{-
Note [No nested foralls or contexts in GADT constructors]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
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.
Because the presence of outermost parentheses can affect whether
`forall`s/contexts are nested, the parser is careful not to remove parentheses
when post-processing GADT constructors (in mkGadtDecl). Later, the renamer will
check for nested `forall`s/contexts (in GHC.Rename.Module.rnConDecl) after
it has determined what all of the argument types are.
(See Note [GADT abstract syntax] in GHC.Hs.Decls for why this check must wait
until the renamer.)
-}
setRdrNameSpace :: RdrName -> NameSpace -> RdrName
-- ^ This rather gruesome function is used mainly by the parser.
......
......@@ -59,7 +59,8 @@ import GHC.Types.Basic ( pprRuleName, TypeOrKind(..) )
import GHC.Data.FastString
import GHC.Types.SrcLoc as SrcLoc
import GHC.Driver.Session
import GHC.Utils.Misc ( debugIsOn, filterOut, lengthExceeds, partitionWith )
import GHC.Utils.Misc ( debugIsOn, filterOut, lengthExceeds, notNull
, partitionWith )
import GHC.Driver.Types ( HscEnv, hsc_dflags )
import GHC.Data.List.SetOps ( findDupsEq, removeDups, equivClasses )
import GHC.Data.Graph.Directed ( SCC, flattenSCC, flattenSCCs, Node(..)
......@@ -2102,17 +2103,22 @@ rnConDecl decl@(ConDeclGADT { con_names = names
do { (new_cxt, fvs1) <- rnMbContext ctxt mcxt
; (new_args, fvs2) <- rnConDeclDetails (unLoc (head new_names)) ctxt args
; (new_res_ty, fvs3) <- rnLHsType ctxt res_ty
; (args', res_ty') <-
case args of
InfixCon {} -> pprPanic "rnConDecl" (ppr names)
RecCon {} -> pure (new_args, new_res_ty)
PrefixCon as -> do
-- In the PrefixCon case, the parser puts the entire body of
-- the constructor type, including argument types, into res_ty.
-- We can properly determine what the argument types are after
-- renaming (see Note [GADT abstract syntax] in GHC.Hs.Decls),
-- so we do so by splitting new_res_ty below.
MASSERT( null as )
(arg_tys, final_res_ty) <-
split_prefix_gadt_ty ctxt explicit_tkvs new_cxt new_res_ty
pure (PrefixCon arg_tys, final_res_ty)
; let all_fvs = fvs1 `plusFV` fvs2 `plusFV` fvs3
(args', res_ty')
= case args of
InfixCon {} -> pprPanic "rnConDecl" (ppr names)
RecCon {} -> (new_args, new_res_ty)
PrefixCon as | (arg_tys, final_res_ty) <- splitHsFunType new_res_ty
-> ASSERT( null as )
-- See Note [GADT abstract syntax] in GHC.Hs.Decls
(PrefixCon arg_tys, final_res_ty)
new_qtvs = HsQTvs { hsq_ext = implicit_tkvs
, hsq_explicit = explicit_tkvs }
......@@ -2122,7 +2128,83 @@ rnConDecl decl@(ConDeclGADT { con_names = names
, con_args = args', con_res_ty = res_ty'
, con_doc = mb_doc' },
all_fvs) } }
where
-- Split the body of a prefix GADT constructor type into its argument
-- and result types. Furthermore, ensure that there are no nested `forall`s
-- or contexts, per
-- Note [No nested foralls or contexts in GADT constructors] in
-- GHC.Parser.PostProcess.
split_prefix_gadt_ty :: HsDocContext
-> [LHsTyVarBndr GhcRn]
-> Maybe (LHsContext GhcRn)
-> LHsType GhcRn
-> RnM ([LHsType GhcRn], LHsType GhcRn)
split_prefix_gadt_ty ctxt gadt_tvbs mb_gadt_cxt gadt_rho = do
-- Check for nested `forall`s or contexts
case gadt_res_ty of
L _ (HsForAllTy { hst_fvf = fvf })
| ForallVis <- fvf
-> addErr $ withHsDocContext ctxt $ vcat
[ hang (text "Illegal visible, dependent quantification" <+>
text "in the type of a term:")
2 (ppr orig_gadt_ty)
, text "(GHC does not yet support this)" ]
| ForallInvis <- fvf
-> nested_foralls_contexts_err
L _ (HsQualTy {})
-> nested_foralls_contexts_err
_ -> pure ()
pure (gadt_arg_tys, gadt_res_ty)
where
(gadt_arg_tys, gadt_res_ty) = splitLHsFunTys gadt_rho
-- If we are going to reject a GADT constructor type for having nested
-- `forall`s or contexts, then we can at least suggest an alternative
-- way to write the type without nesting. (#12087)
nested_foralls_contexts_err :: RnM ()
nested_foralls_contexts_err =
addErr $ withHsDocContext ctxt $
text "GADT constructor type signature cannot contain nested"
<+> quotes forAllLit <> text "s or contexts"
$+$ hang (text "Suggestion: instead use this type signature:")
2 (pprWithCommas ppr names <+> dcolon <+> ppr suggested_gadt_ty)
-- To construct a type that GHC would accept (suggested_gadt_ty), we:
--
-- 1) Split apart the return type (which is headed by a forall or a
-- context) using splitNestedLHsSigmaTysInvis, collecting the type
-- variables and predicates we find, as well as the rho type
-- lurking underneath the nested foralls and contexts.
-- 2) Reassemble the type variables, predicates, and rho type into
-- prenex form.
(suggested_tvbs, suggested_theta, suggested_rho) =
splitNestedLHsSigmaTysInvis orig_gadt_ty
mb_suggested_theta | null (unLoc suggested_theta) = Nothing
| otherwise = Just suggested_theta
orig_gadt_ty = mk_forall_ty explicit_forall gadt_tvbs $
mk_qual_ty mb_gadt_cxt gadt_rho
suggested_gadt_ty =
mk_forall_ty (notNull suggested_tvbs) suggested_tvbs $
mk_qual_ty mb_suggested_theta suggested_rho
mk_forall_ty exp_forall tvbs tau
| exp_forall = noLoc $
HsForAllTy { hst_xforall = noExtField
, hst_fvf = ForallInvis
, hst_bndrs = tvbs
, hst_body = tau }
| otherwise = tau
mk_qual_ty mb_ctxt rho =
case mb_ctxt of
Nothing -> rho
Just ctxt -> noLoc $
HsQualTy { hst_xqual = noExtField
, hst_ctxt = ctxt
, hst_body = rho }
rnMbContext :: HsDocContext -> Maybe (LHsContext GhcPs)
-> RnM (Maybe (LHsContext GhcRn), FreeVars)
......
......@@ -4733,50 +4733,12 @@ noClassTyVarErr clas fam_tc
badDataConTyCon :: DataCon -> Type -> SDoc
badDataConTyCon data_con res_ty_tmpl
| ASSERT( all isTyVar tvs )
tcIsForAllTy actual_res_ty
= nested_foralls_contexts_suggestion
| isJust (tcSplitPredFunTy_maybe actual_res_ty)
= nested_foralls_contexts_suggestion
| otherwise
= hang (text "Data constructor" <+> quotes (ppr data_con) <+>
text "returns type" <+> quotes (ppr actual_res_ty))
2 (text "instead of an instance of its parent type" <+> quotes (ppr res_ty_tmpl))
where
actual_res_ty = dataConOrigResTy data_con
-- This suggestion is useful for suggesting how to correct code like what
-- was reported in #12087:
--
-- data F a where
-- MkF :: Ord a => Eq a => a -> F a
--
-- Although nested foralls or contexts are allowed in function type
-- signatures, it is much more difficult to engineer GADT constructor type
-- signatures to allow something similar, so we error in the latter case.
-- Nevertheless, we can at least suggest how a user might reshuffle their
-- exotic GADT constructor type signature so that GHC will accept.
nested_foralls_contexts_suggestion =
text "GADT constructor type signature cannot contain nested"
<+> quotes forAllLit <> text "s or contexts"
$+$ hang (text "Suggestion: instead use this type signature:")
2 (ppr (dataConName data_con) <+> dcolon <+> ppr suggested_ty)
-- To construct a type that GHC would accept (suggested_ty), we:
--
-- 1) Find the existentially quantified type variables and the class
-- predicates from the datacon. (NB: We don't need the universally
-- quantified type variables, since rejigConRes won't substitute them in
-- the result type if it fails, as in this scenario.)
-- 2) Split apart the return type (which is headed by a forall or a
-- context) using tcSplitNestedSigmaTys, collecting the type variables
-- and class predicates we find, as well as the rho type lurking
-- underneath the nested foralls and contexts.
-- 3) Smash together the type variables and class predicates from 1) and
-- 2), and prepend them to the rho type from 2).
(tvs, theta, rho) = tcSplitNestedSigmaTys (dataConUserType data_con)
suggested_ty = mkSpecSigmaTy tvs theta rho
badGadtDecl :: Name -> SDoc
badGadtDecl tc_name
= vcat [ text "Illegal generalised algebraic data declaration for" <+> quotes (ppr tc_name)
......
......@@ -614,7 +614,7 @@ cvtConstr (GadtC c strtys ty)
; args <- mapM cvt_arg strtys
; L _ ty' <- cvtType ty
; c_ty <- mk_arr_apps args ty'
; returnL $ fst $ mkGadtDecl c' c_ty}
; returnL $ mkGadtDecl c' c_ty}
cvtConstr (RecGadtC [] _varstrtys _ty)
= failWith (text "RecGadtC must have at least one constructor name")
......@@ -625,7 +625,7 @@ cvtConstr (RecGadtC c varstrtys ty)
; rec_flds <- mapM cvt_id_arg varstrtys
; let rec_ty = noLoc (HsFunTy noExtField
(noLoc $ HsRecTy noExtField rec_flds) ty')
; returnL $ fst $ mkGadtDecl c' rec_ty }
; returnL $ mkGadtDecl c' rec_ty }
cvtSrcUnpackedness :: TH.SourceUnpackedness -> SrcUnpackedness
cvtSrcUnpackedness NoSourceUnpackedness = NoSrcUnpack
......
......@@ -79,6 +79,27 @@ Language
This change prepares the way for Quick Look impredicativity.
* GADT constructor types now properly adhere to :ref:`forall-or-nothing`. As
a result, GHC will now reject some GADT constructors that previous versions
of GHC would accept, such as the following: ::
data T where
MkT1 :: (forall a. a -> b -> T)
MkT2 :: (forall a. a -> T)
``MkT1`` and ``MkT2`` are rejected because the lack of an outermost
``forall`` triggers implicit quantification, making the explicit ``forall``s
nested. Furthermore, GADT constructors do not permit the use of nested
``forall``s, as explained in :ref:`formal-gadt-syntax`.
In addition to rejecting nested ``forall``s, GHC is now more stringent about
rejecting uses of nested *contexts* in GADT constructors. For example, the
following example, which previous versions of GHC would accept, is now
rejected:
data U a where
MkU :: (Show a => U a)
Compiler
~~~~~~~~
......@@ -148,11 +169,11 @@ Arrow notation
``hsGroupTopLevelFixitySigs`` function, which collects all top-level fixity
signatures, including those for class methods defined inside classes.
- The ``Exception`` module was boiled down acknowledging the existence of
- The ``Exception`` module was boiled down acknowledging the existence of
the ``exceptions`` dependency. In particular, the ``ExceptionMonad``
class is not a proper class anymore, but a mere synonym for ``MonadThrow``,
``MonadCatch``, ``MonadMask`` (all from ``exceptions``) and ``MonadIO``.
All of ``g*``-functions from the module (``gtry``, ``gcatch``, etc.) are
``MonadCatch``, ``MonadMask`` (all from ``exceptions``) and ``MonadIO``.
All of ``g*``-functions from the module (``gtry``, ``gcatch``, etc.) are
erased, and their ``exceptions``-alternatives are meant to be used in the
GHC code instead.
......
......@@ -45,4 +45,81 @@ Notes:
would warn about the unused type variable `a`.
.. _forall-or-nothing:
The ``forall``-or-nothing rule
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
In certain forms of types, type variables obey what is known as the
"``forall``-or-nothing" rule: if a type has an outermost, explicit
``forall``, then all of the type variables in the type must be explicitly
quantified. These two examples illustrate how the rule works: ::
f :: forall a b. a -> b -> b -- OK, `a` and `b` are explicitly bound
g :: forall a. a -> forall b. b -> b -- OK, `a` and `b` are explicitly bound
h :: forall a. a -> b -> b -- Rejected, `b` is not in scope
The type signatures for ``f``, ``g``, and ``h`` all begin with an outermost
``forall``, so every type variable in these signatures must be explicitly
bound by a ``forall``. Both ``f`` and ``g`` obey the ``forall``-or-nothing
rule, since they explicitly quantify ``a`` and ``b``. On the other hand,
``h`` does not explicitly quantify ``b``, so GHC will reject its type
signature for being improperly scoped.
In places where the ``forall``-or-nothing rule takes effect, if a type does
*not* have an outermost ``forall``, then any type variables that are not
explicitly bound by a ``forall`` become implicitly quantified. For example: ::
i :: a -> b -> b -- `a` and `b` are implicitly quantified
j :: a -> forall b. b -> b -- `a` is implicitly quantified
k :: (forall a. a -> b -> b) -- `b` is implicitly quantified
GHC will accept ``i``, ``j``, and ``k``'s type signatures. Note that:
- ``j``'s signature is accepted despite its mixture of implicit and explicit
quantification. As long as a ``forall`` is not an outermost one, it is fine
to use it among implicitly bound type variables.
- ``k``'s signature is accepted because the outermost parentheses imply that
the ``forall`` is not an outermost ``forall``. The ``forall``-or-nothing
rule is one of the few places in GHC where the presence or absence of
parentheses can be semantically significant!
The ``forall``-or-nothing rule takes effect in the following places:
- Type signature declarations for functions, values, and class methods
- Expression type annotations
- Instance declarations
- :ref:`class-default-signatures`
- Type signatures in a :ref:`specialize-pragma` or
:ref:`specialize-instance-pragma`
- :ref:`standalone-kind-signatures`
- Type signatures for :ref:`gadt` constructors
- Type signatures for :ref:`pattern-synonyms`
- :ref:`data-instance-declarations`, :ref:`type-instance-declarations`,
:ref:`closed-type-families`, and :ref:`assoc-inst`
- :ref:`rewrite-rules` in which the type variables are explicitly quantified
Notes:
- :ref:`pattern-type-sigs` are a notable example of a place where
types do *not* obey the ``forall``-or-nothing rule. For example, GHC will
accept the following: ::
f (g :: forall a. a -> b) x = g x :: b
Furthermore, :ref:`rewrite-rules` do not obey the ``forall``-or-nothing rule
when their type variables are not explicitly quantified: ::
{-# RULES "f" forall (g :: forall a. a -> b) x. f g x = g x :: b #-}
- GADT constructors are extra particular about their ``forall``s. In addition
to adhering to the ``forall``-or-nothing rule, GADT constructors also forbid
nested ``forall``s. For example, GHC would reject the following GADT: ::
data T where
MkT :: (forall a. a -> b -> T)
Because of the lack of an outermost ``forall`` in the type of ``MkT``, the
``b`` would be implicitly quantified. In effect, it would be as if one had
written ``MkT :: forall b. (forall a. a -> b -> T)``, which contains nested
``forall``s. See :ref:`formal-gadt-syntax`.
......@@ -103,6 +103,114 @@ implements this behaviour, odd though it is. But for GADT-style
declarations, GHC's behaviour is much more useful, as well as much more
intuitive.
.. _formal-gadt-syntax:
Formal syntax for GADTs
~~~~~~~~~~~~~~~~~~~~~~~
To make more precise what is and what is not permitted inside of a GADT-style
constructor, we provide a BNF-style grammar for GADT below. Note that this
grammar is subject to change in the future. ::
gadt_con ::= conids '::' opt_forall opt_ctxt gadt_body
conids ::= conid
| conid ',' conids
opt_forall ::= <empty>
| 'forall' tv_bndrs '.'
tv_bndrs ::= <empty>
| tv_bndr tv_bndrs
tv_bndr ::= tyvar
| '(' tyvar '::' ctype ')'
opt_ctxt ::= <empty>
| btype '=>'
| '(' ctxt ')' '=>'
ctxt ::= ctype
| ctype ',' ctxt
gadt_body ::= prefix_gadt_body
| record_gadt_body
prefix_gadt_body ::= '(' prefix_gadt_body ')'
| return_type
| opt_bang btype '->' prefix_gadt_body
record_gadt_body ::= '{' fieldtypes '}' '->' return_type
fieldtypes ::= <empty>
| fieldname '::' opt_bang ctype
| fieldname '::' opt_bang ctype ',' fieldtypes
opt_bang ::= <empty>
| '!'
| '~'
| {-# UNPACK #-}
| {-# NOUNPACK #-}
Where:
- ``btype`` is a type that is not allowed to have an outermost
``forall``/``=>`` unless it is surrounded by parentheses. For example,
``forall a. a`` and ``Eq a => a`` are not legal ``btype``s, but
``(forall a. a)`` and ``(Eq a => a)`` are legal.
- ``ctype`` is a ``btype`` that has no restrictions on an outermost
``forall``/``=>``, so ``forall a. a`` and ``Eq a => a`` are legal ``ctype``s.
- ``return_type`` is a type that is not allowed to have ``forall``s, ``=>``s,
or ``->``s.
This is a simplified grammar that does not fully delve into all of the
implementation details of GHC's parser (such as the placement of Haddock
comments), but it is sufficient to attain an understanding of what is
syntactically allowed. Some further various observations about this grammar:
- GADT constructor types are currently not permitted to have nested ``forall``s
or ``=>``s. (e.g., something like ``MkT :: Int -> forall a. a -> T`` would be
rejected.) As a result, ``gadt_sig`` puts all of its quantification and
constraints up front with ``opt_forall`` and ``opt_context``. Note that
higher-rank ``forall``s and ``=>``s are only permitted if they do not appear
directly to the right of a function arrow in a `prefix_gadt_body`. (e.g.,
something like ``MkS :: Int -> (forall a. a) -> S`` is allowed, since
parentheses separate the ``forall`` from the ``->``.)
- Furthermore, GADT constructors do not permit outermost parentheses that
surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
used. For example, ``MkU :: (forall a. a -> U)`` would be rejected, since
it would treat the ``forall`` as being nested.
Note that it is acceptable to use parentheses in a ``prefix_gadt_body``.
For instance, ``MkV1 :: forall a. (a) -> (V1)`` is acceptable, as is
``MkV2 :: forall a. (a -> V2)``.
- The function arrows in a ``prefix_gadt_body``, as well as the function
arrow in a ``record_gadt_body``, are required to be used infix. For
example, ``MkA :: (->) Int A`` would be rejected.
- GHC uses the function arrows in a ``prefix_gadt_body`` and
``prefix_gadt_body`` to syntactically demarcate the function and result
types. Note that GHC does not attempt to be clever about looking through
type synonyms here. If you attempt to do this, for instance: ::
type C = Int -> B
data B where
MkB :: C
Then GHC will interpret the return type of ``MkB`` to be ``C``, and since
GHC requires that the return type must be headed by ``B``, this will be
rejected. On the other hand, it is acceptable to use type synonyms within
the argument and result types themselves, so the following is permitted: ::
type B1 = Int
type B2 = B
data B where
MkB :: B1 -> B2
GADT syntax odds at ends
~~~~~~~~~~~~~~~~~~~~~~~~
The rest of this section gives further details about GADT-style data
type declarations.
......
T16326_Fail6.hs:9:3: error:
• GADT constructor type signature cannot contain nested ‘forall’s or contexts
Suggestion: instead use this type signature:
MkFoo :: forall a. a -> Foo a
• In the definition of data constructor ‘MkFoo’
In the data type declaration for ‘Foo’
Illegal visible, dependent quantification in the type of a term:
forall a -> a -> Foo a
(GHC does not yet support this)
In the definition of data constructor ‘MkFoo’