[Git][ghc/ghc][wip/T18191] Make GADT constructors adhere to the forall-or-nothing rule properly
Ryan Scott
gitlab at gitlab.haskell.org
Tue May 26 14:02:59 UTC 2020
Ryan Scott pushed to branch wip/T18191 at Glasgow Haskell Compiler / GHC
Commits:
448cfdfb by Ryan Scott at 2020-05-26T09:46:55-04:00
Make GADT constructors adhere to the forall-or-nothing rule properly
Issue #18191 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: the outermost
`forall` and/or context in a GADT constructor is not allowed to be
surrounded by parentheses. Doing so would make these
`forall`s/contexts nested, and GADTs do not support nested
`forall`s/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:
* `GHC.Parser.PostProcess.mkGadtDecl` no longer strips away
parentheses from the outermost `forall` and context. Instead, these
parentheses are preserved so that the renamer can check for nested
`forall`s/contexts later. See
`Note [No nested foralls or contexts in GADT constructors]` in
`GHC.Parser.PostProcess` for more details.
One nice side effect of this change is that we can get rid of the
explicit `AddAnn` tracking in `mkGadtDecl`, as we no longer need to
remember the `AddAnn`s for stripped-away parentheses.
* `GHC.Renamer.Module.rnConDecl` now checks for nested
`forall`s/contexts, rather than checking for this in the typechcker
(in `GHC.Tc.TyCl.badDataConTyCon`). For the most part, this code
was ported directly from `badDataConTyCon`, but designed to work
over `HsType`s instead of `Type`s.
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.
- - - - -
20 changed files:
- compiler/GHC/Parser.y
- compiler/GHC/Parser/PostProcess.hs
- compiler/GHC/Rename/Module.hs
- compiler/GHC/Tc/TyCl.hs
- compiler/GHC/ThToHs.hs
- docs/users_guide/8.12.1-notes.rst
- docs/users_guide/exts/explicit_forall.rst
- docs/users_guide/exts/gadt_syntax.rst
- testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
- testsuite/tests/gadt/T12087.stderr
- testsuite/tests/gadt/T14320.hs
- + testsuite/tests/gadt/T14320.stderr
- testsuite/tests/gadt/T16427.stderr
- + testsuite/tests/gadt/T18191.hs
- + testsuite/tests/gadt/T18191.stderr
- testsuite/tests/gadt/all.T
- testsuite/tests/ghc-api/annotations/T10399.stdout
- testsuite/tests/ghc-api/annotations/Test10399.hs
- testsuite/tests/parser/should_compile/T15323.hs
- testsuite/tests/parser/should_compile/T15323.stderr
Changes:
=====================================
compiler/GHC/Parser.y
=====================================
@@ -2248,9 +2248,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]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
=====================================
compiler/GHC/Parser/PostProcess.hs
=====================================
@@ -685,30 +685,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 = 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 = 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
@@ -718,10 +729,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.
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -2126,16 +2126,21 @@ 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 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)
; traceRn "rnConDecl2" (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
; return (decl { con_g_ext = implicit_tkvs, con_names = new_names
@@ -2143,7 +2148,42 @@ 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
+ -> LHsType GhcRn
+ -> RnM ([LHsType GhcRn], LHsType GhcRn)
+ split_prefix_gadt_ty ctxt gadt_rho = do
+ let split_gadt_rho@(_, gadt_res_ty) = splitHsFunType gadt_rho
+
+ -- Check for nested `forall`s or contexts
+ case gadt_res_ty of
+ L l (HsForAllTy { hst_fvf = fvf })
+ | ForallVis <- fvf
+ -> setSrcSpan l $ addErr $ withHsDocContext ctxt $ vcat
+ [ text "Illegal visible, dependent quantification" <+>
+ text "in the type of a term"
+ , text "(GHC does not yet support this)" ]
+ | ForallInvis <- fvf
+ -> nested_foralls_contexts_err l ctxt
+ L l (HsQualTy {})
+ -> nested_foralls_contexts_err l ctxt
+ _ -> pure ()
+
+ pure split_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 :: SrcSpan -> HsDocContext -> RnM ()
+ nested_foralls_contexts_err l ctxt =
+ setSrcSpan l $ addErr $ withHsDocContext ctxt $
+ text "GADT constructor type signature cannot contain nested"
+ <+> quotes forAllLit <> text "s or contexts"
rnMbContext :: HsDocContext -> Maybe (LHsContext GhcPs)
-> RnM (Maybe (LHsContext GhcRn), FreeVars)
=====================================
compiler/GHC/Tc/TyCl.hs
=====================================
@@ -4720,50 +4720,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)
=====================================
compiler/GHC/ThToHs.hs
=====================================
@@ -619,7 +619,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")
@@ -630,7 +630,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
=====================================
docs/users_guide/8.12.1-notes.rst
=====================================
@@ -95,7 +95,28 @@ Language
effectively allows users to choose which variables can or can't be
instantiated through visible type application. More information can be found
here: :ref:`Manually-defining-inferred-variables`.
-
+
+* 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
~~~~~~~~
=====================================
docs/users_guide/exts/explicit_forall.rst
=====================================
@@ -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`.
=====================================
docs/users_guide/exts/gadt_syntax.rst
=====================================
@@ -103,6 +103,123 @@ 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_unpack btype '->' prefix_gadt_body
+
+ record_gadt_body ::= '{' fieldtypes '}' '->' return_type
+
+ fieldtypes ::= <empty>
+ | fieldnames '::' opt_unpack ctype
+ | fieldnames '::' opt_unpack ctype ',' fieldtypes
+
+ fieldnames ::= fieldname
+ | fieldname ',' fieldnames
+
+ opt_unpack ::= opt_bang
+ : {-# UNPACK #-} opt_bang
+ | {-# NOUNPACK #-} opt_bang
+
+ opt_bang ::= <empty>
+ | '!'
+ | '~'
+
+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
+- GHC will accept any combination of ``!``/``~`` and
+ ``{-# UNPACK #-}``/``{-# NOUNPACK #-}``, although GHC will ignore some
+ combinations. For example, GHC will produce a warning if you write
+ ``{-# UNPACK #-} ~Int`` and proceed as if you had written ``Int``.
+
+GADT syntax odds and ends
+~~~~~~~~~~~~~~~~~~~~~~~~~
+
The rest of this section gives further details about GADT-style data
type declarations.
=====================================
testsuite/tests/dependent/should_fail/T16326_Fail6.stderr
=====================================
@@ -1,7 +1,5 @@
-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’
+T16326_Fail6.hs:9:12: error:
+ Illegal visible, dependent quantification in the type of a term
+ (GHC does not yet support this)
+ In the definition of data constructor ‘MkFoo’
=====================================
testsuite/tests/gadt/T12087.stderr
=====================================
@@ -1,35 +1,20 @@
-T12087.hs:6:3: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- MkF1 :: forall a. (Ord a, Eq a) => a -> F1 a
- • In the definition of data constructor ‘MkF1’
- In the data type declaration for ‘F1’
+T12087.hs:6:20: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkF1’
-T12087.hs:9:3: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- MkF2 :: forall a. (Ord a, Eq a) => a -> F2 a
- • In the definition of data constructor ‘MkF2’
- In the data type declaration for ‘F2’
+T12087.hs:9:25: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkF2’
-T12087.hs:12:3: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- MkF3 :: forall a b. (Eq a, Eq b) => a -> b -> F3 a
- • In the definition of data constructor ‘MkF3’
- In the data type declaration for ‘F3’
+T12087.hs:12:34: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkF3’
-T12087.hs:15:3: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- MkF4 :: forall a b. (Eq a, Eq b) => a -> b -> F4 a
- • In the definition of data constructor ‘MkF4’
- In the data type declaration for ‘F4’
+T12087.hs:15:36: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkF4’
-T12087.hs:18:3: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- MkF5 :: forall a b. Int -> Int -> a -> Int -> Int -> b -> F5 a
- • In the definition of data constructor ‘MkF5’
- In the data type declaration for ‘F5’
+T12087.hs:18:25: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkF5’
=====================================
testsuite/tests/gadt/T14320.hs
=====================================
@@ -10,8 +10,8 @@ data Exp :: Type where
newtype TypedExp :: Type -> Type where
TEGood :: forall a . (Exp -> (TypedExp a))
--- The only difference here is that the type is wrapped in parentheses,
--- but GHC 8.0.1 rejects this program
+-- The presence of outer parentheses makes the `forall` nested, and
+-- GADTs do not permit nested `forall`s.
--
newtype TypedExpToo :: Type -> Type where
TEBad :: (forall a . (Exp -> (TypedExpToo a)))
=====================================
testsuite/tests/gadt/T14320.stderr
=====================================
@@ -0,0 +1,4 @@
+
+T14320.hs:17:14: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘TEBad’
=====================================
testsuite/tests/gadt/T16427.stderr
=====================================
@@ -1,7 +1,4 @@
-T16427.hs:5:14: error:
- • GADT constructor type signature cannot contain nested ‘forall’s or contexts
- Suggestion: instead use this type signature:
- C :: forall b. Int -> b -> D
- • In the definition of data constructor ‘C’
- In the data type declaration for ‘D’
+T16427.hs:5:26: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘C’
=====================================
testsuite/tests/gadt/T18191.hs
=====================================
@@ -0,0 +1,12 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RankNTypes #-}
+module T18191 where
+
+data T where
+ MkT :: (forall a. a -> b -> T)
+
+data S a where
+ MkS :: (forall a. S a)
+
+data U a where
+ MkU :: (Show a => U a)
=====================================
testsuite/tests/gadt/T18191.stderr
=====================================
@@ -0,0 +1,12 @@
+
+T18191.hs:6:11: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkT’
+
+T18191.hs:9:11: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkS’
+
+T18191.hs:12:11: error:
+ GADT constructor type signature cannot contain nested ‘forall’s or contexts
+ In the definition of data constructor ‘MkU’
=====================================
testsuite/tests/gadt/all.T
=====================================
@@ -113,10 +113,11 @@ test('T7558', normal, compile_fail, [''])
test('T9380', normal, compile_and_run, [''])
test('T12087', normal, compile_fail, [''])
test('T12468', normal, compile_fail, [''])
-test('T14320', normal, compile, [''])
+test('T14320', normal, compile_fail, [''])
test('T14719', normal, compile_fail, ['-fdiagnostics-show-caret'])
test('T14808', normal, compile, [''])
test('T15009', normal, compile, [''])
test('T15558', normal, compile, [''])
test('T16427', normal, compile_fail, [''])
test('T17423', expect_broken(17423), compile_and_run, [''])
+test('T18191', normal, compile_fail, [''])
=====================================
testsuite/tests/ghc-api/annotations/T10399.stdout
=====================================
@@ -34,9 +34,9 @@
((Test10399.hs:12:30,AnnComma), [Test10399.hs:12:30]),
((Test10399.hs:12:31-32,AnnCloseP), [Test10399.hs:12:32]),
((Test10399.hs:12:31-32,AnnOpenP), [Test10399.hs:12:31]),
-((Test10399.hs:(14,1)-(18,55),AnnData), [Test10399.hs:14:1-4]),
-((Test10399.hs:(14,1)-(18,55),AnnSemi), [Test10399.hs:20:1]),
-((Test10399.hs:(14,1)-(18,55),AnnWhere), [Test10399.hs:14:21-25]),
+((Test10399.hs:(14,1)-(18,53),AnnData), [Test10399.hs:14:1-4]),
+((Test10399.hs:(14,1)-(18,53),AnnSemi), [Test10399.hs:20:1]),
+((Test10399.hs:(14,1)-(18,53),AnnWhere), [Test10399.hs:14:21-25]),
((Test10399.hs:15:5-64,AnnDcolon), [Test10399.hs:15:11-12]),
((Test10399.hs:15:5-64,AnnSemi), [Test10399.hs:16:5]),
((Test10399.hs:15:14-64,AnnDot), [Test10399.hs:15:23]),
@@ -48,37 +48,29 @@
((Test10399.hs:15:45-46,AnnBang), [Test10399.hs:15:45]),
((Test10399.hs:15:45-46,AnnRarrow), [Test10399.hs:15:48-49]),
((Test10399.hs:15:45-64,AnnRarrow), [Test10399.hs:15:48-49]),
-((Test10399.hs:(16,5)-(17,69),AnnCloseP), [Test10399.hs:17:69]),
-((Test10399.hs:(16,5)-(17,69),AnnDcolon), [Test10399.hs:16:12-13]),
-((Test10399.hs:(16,5)-(17,69),AnnOpenP), [Test10399.hs:16:27]),
-((Test10399.hs:(16,5)-(17,69),AnnSemi), [Test10399.hs:18:5]),
-((Test10399.hs:(16,15)-(17,69),AnnDot), [Test10399.hs:16:25]),
-((Test10399.hs:(16,15)-(17,69),AnnForall), [Test10399.hs:16:15-20]),
-((Test10399.hs:(16,27)-(17,69),AnnCloseP), [Test10399.hs:17:69]),
-((Test10399.hs:(16,27)-(17,69),AnnOpenP), [Test10399.hs:16:27]),
-((Test10399.hs:16:28-43,AnnCloseP), [Test10399.hs:16:43, Test10399.hs:16:43]),
-((Test10399.hs:16:28-43,AnnDarrow), [Test10399.hs:16:45-46]),
-((Test10399.hs:16:28-43,AnnOpenP), [Test10399.hs:16:28, Test10399.hs:16:28]),
-((Test10399.hs:16:30-33,AnnComma), [Test10399.hs:16:34]),
-((Test10399.hs:16:48,AnnRarrow), [Test10399.hs:16:50-51]),
-((Test10399.hs:(16,48)-(17,68),AnnRarrow), [Test10399.hs:16:50-51]),
-((Test10399.hs:16:53-66,AnnRarrow), [Test10399.hs:17:45-46]),
-((Test10399.hs:(16,53)-(17,68),AnnRarrow), [Test10399.hs:17:45-46]),
-((Test10399.hs:17:48,AnnRarrow), [Test10399.hs:17:50-51]),
-((Test10399.hs:17:48-68,AnnRarrow), [Test10399.hs:17:50-51]),
-((Test10399.hs:17:66-68,AnnCloseS), [Test10399.hs:17:68]),
-((Test10399.hs:17:66-68,AnnOpenS), [Test10399.hs:17:66]),
-((Test10399.hs:18:5-55,AnnCloseP), [Test10399.hs:18:55]),
-((Test10399.hs:18:5-55,AnnDcolon), [Test10399.hs:18:16-17]),
-((Test10399.hs:18:5-55,AnnOpenP), [Test10399.hs:18:19]),
-((Test10399.hs:18:19-55,AnnCloseP), [Test10399.hs:18:55]),
-((Test10399.hs:18:19-55,AnnOpenP), [Test10399.hs:18:19]),
-((Test10399.hs:18:20-54,AnnDot), [Test10399.hs:18:29]),
-((Test10399.hs:18:20-54,AnnForall), [Test10399.hs:18:20-25]),
-((Test10399.hs:18:31-36,AnnCloseP), [Test10399.hs:18:36]),
-((Test10399.hs:18:31-36,AnnOpenP), [Test10399.hs:18:31]),
-((Test10399.hs:18:31-36,AnnRarrow), [Test10399.hs:18:38-39]),
-((Test10399.hs:18:31-54,AnnRarrow), [Test10399.hs:18:38-39]),
+((Test10399.hs:(16,5)-(17,67),AnnDcolon), [Test10399.hs:16:12-13]),
+((Test10399.hs:(16,5)-(17,67),AnnSemi), [Test10399.hs:18:5]),
+((Test10399.hs:(16,15)-(17,67),AnnDot), [Test10399.hs:16:25]),
+((Test10399.hs:(16,15)-(17,67),AnnForall), [Test10399.hs:16:15-20]),
+((Test10399.hs:16:27-42,AnnCloseP), [Test10399.hs:16:42, Test10399.hs:16:42]),
+((Test10399.hs:16:27-42,AnnDarrow), [Test10399.hs:16:44-45]),
+((Test10399.hs:16:27-42,AnnOpenP), [Test10399.hs:16:27, Test10399.hs:16:27]),
+((Test10399.hs:16:29-32,AnnComma), [Test10399.hs:16:33]),
+((Test10399.hs:16:47,AnnRarrow), [Test10399.hs:16:49-50]),
+((Test10399.hs:(16,47)-(17,67),AnnRarrow), [Test10399.hs:16:49-50]),
+((Test10399.hs:16:52-65,AnnRarrow), [Test10399.hs:17:44-45]),
+((Test10399.hs:(16,52)-(17,67),AnnRarrow), [Test10399.hs:17:44-45]),
+((Test10399.hs:17:47,AnnRarrow), [Test10399.hs:17:49-50]),
+((Test10399.hs:17:47-67,AnnRarrow), [Test10399.hs:17:49-50]),
+((Test10399.hs:17:65-67,AnnCloseS), [Test10399.hs:17:67]),
+((Test10399.hs:17:65-67,AnnOpenS), [Test10399.hs:17:65]),
+((Test10399.hs:18:5-53,AnnDcolon), [Test10399.hs:18:16-17]),
+((Test10399.hs:18:19-53,AnnDot), [Test10399.hs:18:28]),
+((Test10399.hs:18:19-53,AnnForall), [Test10399.hs:18:19-24]),
+((Test10399.hs:18:30-35,AnnCloseP), [Test10399.hs:18:35]),
+((Test10399.hs:18:30-35,AnnOpenP), [Test10399.hs:18:30]),
+((Test10399.hs:18:30-35,AnnRarrow), [Test10399.hs:18:37-38]),
+((Test10399.hs:18:30-53,AnnRarrow), [Test10399.hs:18:37-38]),
((Test10399.hs:20:1-25,AnnCloseQ), [Test10399.hs:20:24-25]),
((Test10399.hs:20:1-25,AnnOpen), [Test10399.hs:20:1-3]),
((Test10399.hs:20:1-25,AnnSemi), [Test10399.hs:22:1]),
=====================================
testsuite/tests/ghc-api/annotations/Test10399.hs
=====================================
@@ -13,9 +13,9 @@ mkPoli = mkBila . map ((,,(),,()) <$> P.base <*> P.pos <*> P.form)
data MaybeDefault v where
SetTo :: forall v . ( Eq v, Show v ) => !v -> MaybeDefault v
- SetTo4 :: forall v a. (( Eq v, Show v ) => v -> MaybeDefault v
- -> a -> MaybeDefault [a])
- TestParens :: (forall v . (Eq v) -> MaybeDefault v)
+ SetTo4 :: forall v a. ( Eq v, Show v ) => v -> MaybeDefault v
+ -> a -> MaybeDefault [a]
+ TestParens :: forall v . (Eq v) -> MaybeDefault v
[t| Map.Map T.Text $tc |]
=====================================
testsuite/tests/parser/should_compile/T15323.hs
=====================================
@@ -3,4 +3,4 @@
module T15323 where
data MaybeDefault v where
- TestParens :: (forall v . (Eq v) => MaybeDefault v)
+ TestParens :: forall v . (Eq v) => MaybeDefault v
=====================================
testsuite/tests/parser/should_compile/T15323.stderr
=====================================
@@ -8,7 +8,7 @@
{ModuleName: T15323}))
(Nothing)
[]
- [({ T15323.hs:(5,1)-(6,56) }
+ [({ T15323.hs:(5,1)-(6,54) }
(TyClD
(NoExtField)
(DataDecl
@@ -33,60 +33,60 @@
[])
(Nothing)
(Nothing)
- [({ T15323.hs:6:5-56 }
+ [({ T15323.hs:6:5-54 }
(ConDeclGADT
(NoExtField)
[({ T15323.hs:6:5-14 }
(Unqual
{OccName: TestParens}))]
- ({ T15323.hs:6:21-55 }
+ ({ T15323.hs:6:20-54 }
(True))
- [({ T15323.hs:6:28 }
+ [({ T15323.hs:6:27 }
(UserTyVar
(NoExtField)
(SpecifiedSpec)
- ({ T15323.hs:6:28 }
+ ({ T15323.hs:6:27 }
(Unqual
{OccName: v}))))]
(Just
- ({ T15323.hs:6:32-37 }
- [({ T15323.hs:6:32-37 }
+ ({ T15323.hs:6:31-36 }
+ [({ T15323.hs:6:31-36 }
(HsParTy
(NoExtField)
- ({ T15323.hs:6:33-36 }
+ ({ T15323.hs:6:32-35 }
(HsAppTy
(NoExtField)
- ({ T15323.hs:6:33-34 }
+ ({ T15323.hs:6:32-33 }
(HsTyVar
(NoExtField)
(NotPromoted)
- ({ T15323.hs:6:33-34 }
+ ({ T15323.hs:6:32-33 }
(Unqual
{OccName: Eq}))))
- ({ T15323.hs:6:36 }
+ ({ T15323.hs:6:35 }
(HsTyVar
(NoExtField)
(NotPromoted)
- ({ T15323.hs:6:36 }
+ ({ T15323.hs:6:35 }
(Unqual
{OccName: v}))))))))]))
(PrefixCon
[])
- ({ T15323.hs:6:42-55 }
+ ({ T15323.hs:6:41-54 }
(HsAppTy
(NoExtField)
- ({ T15323.hs:6:42-53 }
+ ({ T15323.hs:6:41-52 }
(HsTyVar
(NoExtField)
(NotPromoted)
- ({ T15323.hs:6:42-53 }
+ ({ T15323.hs:6:41-52 }
(Unqual
{OccName: MaybeDefault}))))
- ({ T15323.hs:6:55 }
+ ({ T15323.hs:6:54 }
(HsTyVar
(NoExtField)
(NotPromoted)
- ({ T15323.hs:6:55 }
+ ({ T15323.hs:6:54 }
(Unqual
{OccName: v}))))))
(Nothing)))]
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/448cfdfb7c50463a092d35ea48c5b1a33eee3ba0
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/448cfdfb7c50463a092d35ea48c5b1a33eee3ba0
You're receiving this email because of your account on gitlab.haskell.org.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-commits/attachments/20200526/d3b40cbb/attachment-0001.html>
More information about the ghc-commits
mailing list