[Git][ghc/ghc][wip/T18240] Reject nested foralls/contexts in instance types more consistently
Ryan Scott
gitlab at gitlab.haskell.org
Fri Jun 12 02:05:04 UTC 2020
Ryan Scott pushed to branch wip/T18240 at Glasgow Haskell Compiler / GHC
Commits:
15bfa78c by Ryan Scott at 2020-06-11T22:04:36-04:00
Reject nested foralls/contexts in instance types more consistently
GHC is very wishy-washy about rejecting instance declarations with
nested `forall`s or contexts that are surrounded by outermost
parentheses. This can even lead to some strange interactions with
`ScopedTypeVariables`, as demonstrated in #18240. This patch makes
GHC more consistently reject instance types with nested
`forall`s/contexts so as to prevent these strange interactions.
On the implementation side, this patch tweaks `splitLHsInstDeclTy`
and `getLHsInstDeclHead` to not look through parentheses, which can
be semantically significant. I've added a
`Note [No nested foralls or contexts in instance types]` in
`GHC.Hs.Type` to explain why. This also introduces a
`no_nested_foralls_contexts_err` function in `GHC.Rename.HsType` to
catch nested `forall`s/contexts in instance types. This function is
now used in `rnClsInstDecl` (for ordinary instance declarations) and
`rnSrcDerivDecl` (for standalone `deriving` declarations), the latter
of which fixes #18271.
On the documentation side, this adds a new
"Formal syntax for instance declaration types" section to the GHC
User's Guide that presents a BNF-style grammar for what is and isn't
allowed in instance types.
Fixes #18240. Fixes #18271.
- - - - -
23 changed files:
- compiler/GHC/Hs/Type.hs
- compiler/GHC/Rename/Module.hs
- docs/users_guide/8.12.1-notes.rst
- docs/users_guide/exts/explicit_forall.rst
- docs/users_guide/exts/instances.rst
- docs/users_guide/exts/scoped_type_variables.rst
- testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
- + testsuite/tests/dependent/should_fail/T18271.hs
- + testsuite/tests/dependent/should_fail/T18271.stderr
- testsuite/tests/dependent/should_fail/all.T
- testsuite/tests/deriving/should_compile/T15831.hs
- testsuite/tests/deriving/should_compile/deriving-via-standalone.hs
- testsuite/tests/deriving/should_fail/deriving-via-fail.hs
- testsuite/tests/deriving/should_fail/deriving-via-fail4.hs
- testsuite/tests/parser/should_fail/T3811c.stderr
- testsuite/tests/rename/should_fail/T16114.stderr
- + testsuite/tests/rename/should_fail/T18240a.hs
- + testsuite/tests/rename/should_fail/T18240a.stderr
- + testsuite/tests/rename/should_fail/T18240b.hs
- + testsuite/tests/rename/should_fail/T18240b.stderr
- testsuite/tests/rename/should_fail/T5951.stderr
- testsuite/tests/rename/should_fail/all.T
- testsuite/tests/typecheck/should_fail/T16394.stderr
Changes:
=====================================
compiler/GHC/Hs/Type.hs
=====================================
@@ -58,7 +58,7 @@ module GHC.Hs.Type (
hsLTyVarName, hsLTyVarNames, hsLTyVarLocName, hsExplicitLTyVarNames,
splitLHsInstDeclTy, getLHsInstDeclHead, getLHsInstDeclClass_maybe,
splitLHsPatSynTy,
- splitLHsForAllTyInvis, splitLHsQualTy,
+ splitLHsForAllTyInvis, splitLHsForAllTyInvis_KP, splitLHsQualTy,
splitLHsSigmaTyInvis, splitLHsGADTPrefixTy,
splitHsFunType, hsTyGetAppHead_maybe,
mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
@@ -93,10 +93,10 @@ import GHC.Types.Basic
import GHC.Types.SrcLoc
import GHC.Utils.Outputable
import GHC.Data.FastString
-import GHC.Data.Maybe( isJust )
import GHC.Utils.Misc ( count )
import Data.Data hiding ( Fixity, Prefix, Infix )
+import Data.Maybe
{-
************************************************************************
@@ -1257,10 +1257,10 @@ splitHsFunType (L _ (HsFunTy _ x y))
splitHsFunType other = ([], other)
--- retrieve the name of the "head" of a nested type application
--- somewhat like splitHsAppTys, but a little more thorough
--- used to examine the result of a GADT-like datacon, so it doesn't handle
--- *all* cases (like lists, tuples, (~), etc.)
+-- | Retrieve the name of the \"head\" of a nested type application.
+-- This is somewhat like @GHC.Tc.Gen.HsType.splitHsAppTys@, but a little more
+-- thorough. The purpose of this function is to examine instance heads, so it
+-- doesn't handle *all* cases (like lists, tuples, @(~)@, etc.).
hsTyGetAppHead_maybe :: LHsType (GhcPass p)
-> Maybe (Located (IdP (GhcPass p)))
hsTyGetAppHead_maybe = go
@@ -1356,6 +1356,26 @@ splitLHsSigmaTyInvis ty
, (ctxt, ty2) <- splitLHsQualTy ty1
= (tvs, ctxt, ty2)
+-- | Decompose a sigma type (of the form @forall <tvs>. context => body@)
+-- into its constituent parts.
+-- Only splits type variable binders that were
+-- quantified invisibly (e.g., @forall a.@, with a dot).
+--
+-- This function is used to split apart certain types, such as instance
+-- declaration types, which disallow visible @forall at s. For instance, if GHC
+-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that
+-- declaration would mistakenly be accepted!
+--
+-- Unlike 'splitLHsSigmaTyInvis', this function does not look through
+-- parentheses, hence the suffix @_KP@ (short for \"Keep Parentheses\").
+splitLHsSigmaTyInvis_KP ::
+ LHsType pass
+ -> (Maybe [LHsTyVarBndr Specificity pass], Maybe (LHsContext pass), LHsType pass)
+splitLHsSigmaTyInvis_KP ty
+ | (mb_tvbs, ty1) <- splitLHsForAllTyInvis_KP ty
+ , (mb_ctxt, ty2) <- splitLHsQualTy_KP ty1
+ = (mb_tvbs, mb_ctxt, ty2)
+
-- | Decompose a prefix GADT type into its constituent parts.
-- Returns @(mb_tvbs, mb_ctxt, body)@, where:
--
@@ -1373,25 +1393,7 @@ splitLHsSigmaTyInvis ty
splitLHsGADTPrefixTy ::
LHsType pass
-> (Maybe [LHsTyVarBndr Specificity pass], Maybe (LHsContext pass), LHsType pass)
-splitLHsGADTPrefixTy ty
- | (mb_tvbs, rho) <- split_forall ty
- , (mb_ctxt, tau) <- split_ctxt rho
- = (mb_tvbs, mb_ctxt, tau)
- where
- -- NB: We do not use splitLHsForAllTyInvis below, since that looks through
- -- parentheses...
- split_forall (L _ (HsForAllTy { hst_fvf = ForallInvis, hst_bndrs = bndrs
- , hst_body = rho }))
- = (Just bndrs, rho)
- split_forall sigma
- = (Nothing, sigma)
-
- -- ...similarly, we do not use splitLHsQualTy below, since that also looks
- -- through parentheses.
- split_ctxt (L _ (HsQualTy { hst_ctxt = cxt, hst_body = tau }))
- = (Just cxt, tau)
- split_ctxt tau
- = (Nothing, tau)
+splitLHsGADTPrefixTy = splitLHsSigmaTyInvis_KP
-- | Decompose a type of the form @forall <tvs>. body@ into its constituent
-- parts. Only splits type variable binders that
@@ -1406,14 +1408,33 @@ splitLHsGADTPrefixTy ty
-- 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.
-splitLHsForAllTyInvis :: LHsType pass -> ([LHsTyVarBndr Specificity pass], LHsType pass)
-splitLHsForAllTyInvis lty@(L _ ty) =
+-- Unlike 'splitLHsSigmaTyInvis', this function does not look through
+-- parentheses, hence the suffix @_KP@ (short for \"Keep Parentheses\").
+splitLHsForAllTyInvis ::
+ LHsType pass -> ([LHsTyVarBndr Specificity pass], LHsType pass)
+splitLHsForAllTyInvis ty
+ | (mb_tvbs, body) <- splitLHsForAllTyInvis_KP (ignoreParens ty)
+ = (fromMaybe [] mb_tvbs, body)
+
+-- | Decompose a type of the form @forall <tvs>. body@ into its constituent
+-- parts. Only splits type variable binders that
+-- were quantified invisibly (e.g., @forall a.@, with a dot).
+--
+-- This function is used to split apart certain types, such as instance
+-- declaration types, which disallow visible @forall at s. For instance, if GHC
+-- split apart the @forall@ in @instance forall a -> Show (Blah a)@, then that
+-- declaration would mistakenly be accepted!
+--
+-- Unlike 'splitLHsForAllTyInvis', this function does not look through
+-- parentheses, hence the suffix @_KP@ (short for \"Keep Parentheses\").
+splitLHsForAllTyInvis_KP ::
+ LHsType pass -> (Maybe [LHsTyVarBndr Specificity pass], LHsType pass)
+splitLHsForAllTyInvis_KP lty@(L _ ty) =
case ty of
- HsParTy _ ty' -> splitLHsForAllTyInvis ty'
HsForAllTy { hst_fvf = fvf', hst_bndrs = tvs', hst_body = body' }
| fvf' == ForallInvis
- -> (tvs', body')
- _ -> ([], lty)
+ -> (Just tvs', body')
+ _ -> (Nothing, lty)
-- | Decompose a type of the form @context => body@ into its constituent parts.
--
@@ -1422,40 +1443,136 @@ splitLHsForAllTyInvis lty@(L _ ty) =
-- generally possible to take the returned types and reconstruct the original
-- type (parentheses and all) from them.
splitLHsQualTy :: LHsType pass -> (LHsContext pass, LHsType pass)
-splitLHsQualTy (L _ (HsParTy _ ty)) = splitLHsQualTy ty
-splitLHsQualTy (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body })) = (ctxt, body)
-splitLHsQualTy body = (noLHsContext, body)
+splitLHsQualTy ty
+ | (mb_ctxt, body) <- splitLHsQualTy_KP (ignoreParens ty)
+ = (fromMaybe noLHsContext mb_ctxt, body)
+
+-- | Decompose a type of the form @context => body@ into its constituent parts.
+--
+-- Unlike 'splitLHsQualTy', this function does not look through
+-- parentheses, hence the suffix @_KP@ (short for \"Keep Parentheses\").
+splitLHsQualTy_KP :: LHsType pass -> (Maybe (LHsContext pass), LHsType pass)
+splitLHsQualTy_KP (L _ (HsQualTy { hst_ctxt = ctxt, hst_body = body }))
+ = (Just ctxt, body)
+splitLHsQualTy_KP body = (Nothing, body)
-- | Decompose a type class instance type (of the form
-- @forall <tvs>. context => instance_head@) into its constituent parts.
+-- Note that the @[Name]@s returned correspond to either:
--
--- Note that this function looks through parentheses, so it will work on types
--- such as @(forall <tvs>. <...>)@. 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.
+-- * The implicitly bound type variables (if the type lacks an outermost
+-- @forall@), or
+--
+-- * The explicitly bound type variables (if the type has an outermost
+-- @forall@).
+--
+-- This function is careful not to look through parentheses.
+-- See @Note [No nested foralls or contexts in instance types]@
+-- for why this is important.
splitLHsInstDeclTy :: LHsSigType GhcRn
-> ([Name], LHsContext GhcRn, LHsType GhcRn)
--- Split up an instance decl type, returning the pieces
splitLHsInstDeclTy (HsIB { hsib_ext = itkvs
, hsib_body = inst_ty })
- | (tvs, cxt, body_ty) <- splitLHsSigmaTyInvis inst_ty
- = (itkvs ++ hsLTyVarNames tvs, cxt, body_ty)
- -- Return implicitly bound type and kind vars
- -- For an instance decl, all of them are in scope
+ | (mb_tvs, mb_cxt, body_ty) <- splitLHsSigmaTyInvis_KP inst_ty
+ = (itkvs ++ maybe [] hsLTyVarNames mb_tvs, fromMaybe noLHsContext mb_cxt, body_ty)
+ -- Because of the forall-or-nothing rule (see Note [forall-or-nothing rule]
+ -- in GHC.Rename.HsType), at least one of itkvs (the implicitly bound type
+ -- variables) or mb_tvs (the explicitly bound type variables) will be
+ -- empty. Still, if ScopedTypeVariables is enabled, we must bring one or
+ -- the other into scope over the bodies of the instance methods, so we
+ -- simply combine them into a single list.
+-- | Decompose a type class instance type (of the form
+-- @forall <tvs>. context => instance_head@) into the @instance_head at .
getLHsInstDeclHead :: LHsSigType (GhcPass p) -> LHsType (GhcPass p)
-getLHsInstDeclHead inst_ty
- | (_tvs, _cxt, body_ty) <- splitLHsSigmaTyInvis (hsSigType inst_ty)
+getLHsInstDeclHead (HsIB { hsib_body = inst_ty })
+ | (_mb_tvs, _mb_cxt, body_ty) <- splitLHsSigmaTyInvis_KP inst_ty
= body_ty
+-- | Decompose a type class instance type (of the form
+-- @forall <tvs>. context => instance_head@) into the @instance_head@ and
+-- retrieve the underlying class type constructor (if it exists).
getLHsInstDeclClass_maybe :: LHsSigType (GhcPass p)
-> Maybe (Located (IdP (GhcPass p)))
--- Works on (HsSigType RdrName)
+-- Works on (LHsSigType GhcPs)
getLHsInstDeclClass_maybe inst_ty
= do { let head_ty = getLHsInstDeclHead inst_ty
; cls <- hsTyGetAppHead_maybe head_ty
; return cls }
+{-
+Note [No nested foralls or contexts in instance types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The type at the top of an instance declaration is one of the few places in GHC
+where nested `forall`s or contexts are not permitted, even with RankNTypes
+enabled. For example, the following will be rejected:
+
+ instance forall a. forall b. Show (Either a b) where ...
+ instance Eq a => Eq b => Show (Either a b) where ...
+ instance (forall a. Show (Maybe a)) where ...
+ instance (Eq a => Show (Maybe a)) where ...
+
+This restriction is partly motivated by an unusual quirk of instance
+declarations. Namely, if ScopedTypeVariables is enabled, then the type
+variables from the top of an instance will scope over the bodies of the
+instance methods, /even if the type variables are implicitly quantified/.
+For example, GHC will accept the following:
+
+ instance Monoid a => Monoid (Identity a) where
+ mempty = Identity (mempty @a)
+
+Moreover, the type in the top of an instance declaration must obey the
+forall-or-nothing rule (see Note [forall-or-nothing rule] in
+GHC.Rename.HsType). If instance types allowed nested `forall`s, this could
+result in some strange interactions. For example, consider the following:
+
+ class C a where
+ m :: Proxy a
+ instance (forall a. C (Either a b)) where
+ m = Proxy @(Either a b)
+
+Somewhat surprisingly, old versions of GHC would accept the instance above.
+Even though the `forall` only quantifies `a`, the outermost parentheses mean
+that the `forall` is nested, and per the forall-or-nothing rule, this means
+that implicit quantification would occur. Therefore, the `a` is explicitly
+bound and the `b` is implicitly bound. Moreover, ScopedTypeVariables would
+bring /both/ sorts of type variables into scope over the body of `m`.
+How utterly confusing!
+
+To avoid this sort of confusion, we simply disallow nested `forall`s in
+instance types, which makes things like the instance above become illegal.
+For the sake of consistency, we also disallow nested contexts, even though they
+don't have the same strange interaction with ScopedTypeVariables.
+
+-----
+-- Wrinkle: Derived instances
+-----
+
+Just as GHC forbids nested `forall`s in the top of instance declarations, it
+also forbids them in types involved with `deriving`:
+
+1. In the `via` types in DerivingVia. For example, this is rejected:
+
+ deriving via (forall x. V x) instance C (S x)
+
+ Just like the types in instance declarations, `via` types can also bring
+ both implicitly and explicitly bound type variables into scope. As a result,
+ we adopt the same no-nested-`forall`s rule in `via` types to avoid confusing
+ behavior like in the example below:
+
+ deriving via (forall x. T x y) instance W x y (Foo a b)
+ -- Both x and y are brought into scope???
+2. In the classes in `deriving` clauses. For example, this is rejected:
+
+ data T = MkT deriving (C1, (forall x. C2 x y))
+
+ This is because the generated instance would look like:
+
+ instance forall x y. C2 x y T where ...
+
+ So really, the same concerns as instance declarations apply here as well.
+-}
+
{-
************************************************************************
* *
=====================================
compiler/GHC/Rename/Module.hs
=====================================
@@ -65,6 +65,7 @@ import GHC.Data.List.SetOps ( findDupsEq, removeDups, equivClasses )
import GHC.Data.Graph.Directed ( SCC, flattenSCC, flattenSCCs, Node(..)
, stronglyConnCompFromEdgedVerticesUniq )
import GHC.Types.Unique.Set
+import GHC.Data.Maybe ( whenIsJust )
import GHC.Data.OrdList
import qualified GHC.LanguageExtensions as LangExt
@@ -601,27 +602,43 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
, cid_sigs = uprags, cid_tyfam_insts = ats
, cid_overlap_mode = oflag
, cid_datafam_insts = adts })
- = do { (inst_ty', inst_fvs)
- <- rnHsSigType (GenericCtx $ text "an instance declaration") TypeLevel inf_err inst_ty
+ = do { (inst_ty', inst_fvs) <- rnHsSigType ctxt TypeLevel inf_err inst_ty
; let (ktv_names, _, head_ty') = splitLHsInstDeclTy inst_ty'
- ; cls <-
- case hsTyGetAppHead_maybe head_ty' of
- Just (L _ cls) -> pure cls
- Nothing -> do
- -- The instance is malformed. We'd still like
- -- to make *some* progress (rather than failing outright), so
- -- we report an error and continue for as long as we can.
- -- Importantly, this error should be thrown before we reach the
- -- typechecker, lest we encounter different errors that are
- -- hopelessly confusing (such as the one in #16114).
- addErrAt (getLoc (hsSigType inst_ty)) $
- hang (text "Illegal class instance:" <+> quotes (ppr inst_ty))
- 2 (vcat [ text "Class instances must be of the form"
- , nest 2 $ text "context => C ty_1 ... ty_n"
- , text "where" <+> quotes (char 'C')
- <+> text "is a class"
- ])
- pure $ mkUnboundName (mkTcOccFS (fsLit "<class>"))
+ -- Check if there are any nested `forall`s or contexts, which are
+ -- illegal in the type of an instance declaration (see
+ -- Note [No nested foralls or contexts in instance types] in
+ -- GHC.Hs.Type)...
+ mb_nested_msg = no_nested_foralls_contexts_err
+ (text "Instance head") head_ty'
+ -- ...then check if the instance head is actually headed by a
+ -- class type constructor...
+ eith_cls = case hsTyGetAppHead_maybe head_ty' of
+ Just (L _ cls) -> Right cls
+ Nothing -> Left
+ ( getLoc head_ty'
+ , hang (text "Illegal head of an instance declaration:"
+ <+> quotes (ppr head_ty'))
+ 2 (vcat [ text "Instance heads must be of the form"
+ , nest 2 $ text "C ty_1 ... ty_n"
+ , text "where" <+> quotes (char 'C')
+ <+> text "is a class"
+ ])
+ )
+ -- ...finally, attempt to retrieve the class type constructor, failing
+ -- with an error message if there isn't one. To avoid excessive
+ -- amounts of error messages, we will only report one of the errors
+ -- from mb_nested_msg or eith_cls at a time.
+ ; cls <- case maybe eith_cls Left mb_nested_msg of
+ Right cls -> pure cls
+ Left (l, err_msg) -> do
+ -- The instance is malformed. We'd still like
+ -- to make *some* progress (rather than failing outright), so
+ -- we report an error and continue for as long as we can.
+ -- Importantly, this error should be thrown before we reach the
+ -- typechecker, lest we encounter different errors that are
+ -- hopelessly confusing (such as the one in #16114).
+ addErrAt l $ withHsDocContext ctxt err_msg
+ pure $ mkUnboundName (mkTcOccFS (fsLit "<class>"))
-- Rename the bindings
-- The typechecker (not the renamer) checks that all
@@ -660,6 +677,7 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
-- strange, but should not matter (and it would be more work
-- to remove the context).
where
+ ctxt = GenericCtx $ text "an instance declaration"
inf_err = Just (text "Inferred type variables are not allowed")
rnFamInstEqn :: HsDocContext
@@ -993,11 +1011,19 @@ rnSrcDerivDecl (DerivDecl _ ty mds overlap)
= do { standalone_deriv_ok <- xoptM LangExt.StandaloneDeriving
; unless standalone_deriv_ok (addErr standaloneDerivErr)
; (mds', ty', fvs)
- <- rnLDerivStrategy DerivDeclCtx mds $
- rnHsSigWcType DerivDeclCtx inf_err ty
+ <- rnLDerivStrategy ctxt mds $ rnHsSigWcType ctxt inf_err ty
+ -- Check if there are any nested `forall`s or contexts, which are
+ -- illegal in the type of an instance declaration (see
+ -- Note [No nested foralls or contexts in instance types] in
+ -- GHC.Hs.Type).
+ ; whenIsJust (no_nested_foralls_contexts_err
+ (text "Standalone-derived instance head")
+ (getLHsInstDeclHead $ dropWildCards ty')) $ \(l, err_msg) ->
+ addErrAt l $ withHsDocContext ctxt err_msg
; warnNoDerivStrat mds' loc
; return (DerivDecl noExtField ty' mds' overlap, fvs) }
where
+ ctxt = DerivDeclCtx
inf_err = Just (text "Inferred type variables are not allowed")
loc = getLoc $ hsib_body $ hswc_body ty
@@ -1805,14 +1831,26 @@ rnLHsDerivingClause doc
, deriv_clause_strategy = dcs
, deriv_clause_tys = L loc' dct }))
= do { (dcs', dct', fvs)
- <- rnLDerivStrategy doc dcs $ mapFvRn (rnHsSigType doc TypeLevel inf_err) dct
+ <- rnLDerivStrategy doc dcs $ mapFvRn rn_clause_pred dct
; warnNoDerivStrat dcs' loc
; pure ( L loc (HsDerivingClause { deriv_clause_ext = noExtField
, deriv_clause_strategy = dcs'
, deriv_clause_tys = L loc' dct' })
, fvs ) }
where
- inf_err = Just (text "Inferred type variables are not allowed")
+ rn_clause_pred :: LHsSigType GhcPs -> RnM (LHsSigType GhcRn, FreeVars)
+ rn_clause_pred pred_ty = do
+ let inf_err = Just (text "Inferred type variables are not allowed")
+ ret@(pred_ty', _) <- rnHsSigType doc TypeLevel inf_err pred_ty
+ -- Check if there are any nested `forall`s, which are illegal in a
+ -- `deriving` clause.
+ -- See Note [No nested foralls or contexts in instance types]
+ -- (Wrinkle: Derived instances) in GHC.Hs.Type.
+ whenIsJust (no_nested_foralls_contexts_err
+ (text "Derived class type")
+ (getLHsInstDeclHead pred_ty')) $ \(l, err_msg) ->
+ addErrAt l $ withHsDocContext doc err_msg
+ pure ret
rnLDerivStrategy :: forall a.
HsDocContext
@@ -1848,9 +1886,17 @@ rnLDerivStrategy doc mds thing_inside
do (via_ty', fvs1) <- rnHsSigType doc TypeLevel inf_err via_ty
let HsIB { hsib_ext = via_imp_tvs
, hsib_body = via_body } = via_ty'
- (via_exp_tv_bndrs, _, _) = splitLHsSigmaTyInvis via_body
- via_exp_tvs = hsLTyVarNames via_exp_tv_bndrs
+ (via_exp_tv_bndrs, via_rho) = splitLHsForAllTyInvis_KP via_body
+ via_exp_tvs = maybe [] hsLTyVarNames via_exp_tv_bndrs
via_tvs = via_imp_tvs ++ via_exp_tvs
+ -- Check if there are any nested `forall`s, which are illegal in a
+ -- `via` type.
+ -- See Note [No nested foralls or contexts in instance types]
+ -- (Wrinkle: Derived instances) in GHC.Hs.Type.
+ whenIsJust (no_nested_foralls_contexts_err
+ (quotes (text "via") <+> text "type")
+ via_rho) $ \(l, err_msg) ->
+ addErrAt l $ withHsDocContext doc err_msg
(thing, fvs2) <- extendTyVarEnvFVRn via_tvs thing_inside
pure (ViaStrategy via_ty', thing, fvs1 `plusFV` fvs2)
@@ -2181,18 +2227,10 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
-- Ensure that there are no nested `forall`s or contexts, per
-- Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)
-- in GHC.Hs.Type.
- ; case 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 ()
+ ; whenIsJust (no_nested_foralls_contexts_err
+ (text "GADT constructor type signature")
+ res_ty) $ \(l, err_msg) ->
+ addErrAt l $ withHsDocContext ctxt err_msg
; traceRn "rnConDecl (ConDeclGADTPrefixPs)"
(ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
@@ -2201,12 +2239,6 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
, con_mb_cxt = mb_cxt, con_args = arg_details
, con_res_ty = res_ty, con_doc = mb_doc' },
fvs) }
- where
- 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)
@@ -2236,6 +2268,41 @@ rnConDeclDetails con doc (RecCon (L l fields))
-- since that is done by GHC.Rename.Names.extendGlobalRdrEnvRn
; return (RecCon (L l new_fields), fvs) }
+-- | Examines a non-outermost type for @forall at s or contexts, which are assumed
+-- to be nested. Returns @'Just' err_msg@ if such a @forall@ or context is
+-- found, and returns @Nothing@ otherwise.
+--
+-- This is currently used in two places:
+--
+-- * In GADT constructor types (in 'rnConDecl').
+-- See @Note [GADT abstract syntax] (Wrinkle: No nested foralls or contexts)@
+-- in "GHC.Hs.Type".
+--
+-- * In instance declaration types (in 'rnClsIntDecl' and 'rnSrcDerivDecl').
+-- See @Note [No nested foralls or contexts in instance types]@ in
+-- "GHC.Hs.Type".
+no_nested_foralls_contexts_err :: SDoc -> LHsType GhcRn -> Maybe (SrcSpan, SDoc)
+no_nested_foralls_contexts_err what lty =
+ case ignoreParens lty of
+ L l (HsForAllTy { hst_fvf = fvf })
+ | ForallVis <- fvf
+ -- The only two places where this function is called correspond to
+ -- types of terms, so we give a slightly more descriptive error
+ -- message in the event that they contain visible dependent
+ -- quantification (currently only allowed in kinds).
+ -> Just (l, vcat [ text "Illegal visible, dependent quantification" <+>
+ text "in the type of a term"
+ , text "(GHC does not yet support this)" ])
+ | ForallInvis <- fvf
+ -> Just (l, nested_foralls_contexts_err)
+ L l (HsQualTy {})
+ -> Just (l, nested_foralls_contexts_err)
+ _ -> Nothing
+ where
+ nested_foralls_contexts_err =
+ what <+> text "cannot contain nested"
+ <+> quotes forAllLit <> text "s or contexts"
+
-------------------------------------------------
-- | Brings pattern synonym names and also pattern synonym selectors
=====================================
docs/users_guide/8.12.1-notes.rst
=====================================
@@ -124,6 +124,22 @@ Language
data U a where
MkU :: (Show a => U a)
+* GHC more strictly enforces the rule that the type in the top of an instance
+ declaration is not permitted to contain nested ``forall``s or contexts, as
+ documented in :ref:`formal-instance-syntax`. For example, the following
+ examples, which previous versions of GHC would accept, are now rejected:
+
+ instance (forall a. C a) where ...
+ instance (Show a => C a) where ...
+
+ In addition, GHC now enforces the rule that the types in ``deriving`` clauses
+ and ``via`` types (for instances derived with :extension:`DerivingVia`)
+ cannot contain nested ``forall``s or contexts. For example, the following
+ examples, which previous versions of GHC would accept, are now rejected: ::
+
+ data T = MkT deriving (C1, (forall x. C2 x))
+ deriving via (forall x. V x) instance C (S x)
+
Compiler
~~~~~~~~
=====================================
docs/users_guide/exts/explicit_forall.rst
=====================================
@@ -37,6 +37,11 @@ Notes:
instance forall a. Eq a => Eq [a] where ...
+ Note that the use of ``forall``s in instance declarations is somewhat
+ restricted in comparison to other types. For example, instance declarations
+ are not allowed to contain nested ``forall``s. See
+ :ref:`formal-instance-syntax` for more information.
+
- If the :ghc-flag:`-Wunused-foralls` flag is enabled, a warning will be emitted
when you write a type variable in an explicit ``forall`` statement that is
otherwise unused. For instance: ::
=====================================
docs/users_guide/exts/instances.rst
=====================================
@@ -99,6 +99,77 @@ GHC relaxes this rule in two ways:
However, the instance declaration must still conform to the rules for
instance termination: see :ref:`instance-termination`.
+.. _formal-instance-syntax:
+
+Formal syntax for instance declaration types
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+The top of an instance declaration only permits very specific forms of types.
+To make more precise what forms of types are or are not permitted, we provide a
+BNF-style grammar for the tops of instance declarations below: ::
+
+ inst_top ::= 'instance' opt_forall opt_ctxt inst_head opt_where
+
+ 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
+
+ inst_head ::= '(' inst_head ')'
+ | prefix_cls_tycon arg_types
+ | arg_type infix_cls_tycon arg_type
+ | '(' arg_type infix_cls_tycon arg_type ')' arg_types
+
+ arg_type ::= <empty>
+ | arg_type arg_types
+
+ opt_where ::= <empty>
+ | 'where'
+
+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.
+- ``arg_type`` is a type that is not allowed to have ``forall``s or ``=>``s
+- ``prefix_cls_tycon`` is a class type constructor written prefix (e.g.,
+ ``Show`` or ``(&&&)``), while ``infix_cls_tycon`` is a class type constructor
+ written infix (e.g., ```Show``` or ``&&&``).
+
+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:
+
+- Instance declarations are not allowed to be declared with nested ``forall``s
+ or ``=>``s. For example, this would be rejected: ::
+
+ instance forall a. forall b. C (Either a b) where ...
+
+ As a result, ``inst_top`` puts all of its quantification and constraints up
+ front with ``opt_forall`` and ``opt_context``.
+- Furthermore, instance declarations types do not permit outermost parentheses
+ that surround the ``opt_forall`` or ``opt_ctxt``, if at least one of them are
+ used. For example, ``instance (forall a. C a)`` would be rejected, since GHC
+ would treat the ``forall`` as being nested.
+
+ Note that it is acceptable to use parentheses in a ``inst_head``. For
+ instance, ``instance (C a)`` is accepted, as is ``instance forall a. (C a)``.
+
.. _instance-rules:
Relaxed rules for instance contexts
=====================================
docs/users_guide/exts/scoped_type_variables.rst
=====================================
@@ -16,11 +16,11 @@ Lexically scoped type variables
.. tip::
- ``ScopedTypeVariables`` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
+ :extension:`ScopedTypeVariables` breaks GHC's usual rule that explicit ``forall`` is optional and doesn't affect semantics.
For the :ref:`decl-type-sigs` (or :ref:`exp-type-sigs`) examples in this section,
the explicit ``forall`` is required.
(If omitted, usually the program will not compile; in a few cases it will compile but the functions get a different signature.)
- To trigger those forms of ``ScopedTypeVariables``, the ``forall`` must appear against the top-level signature (or outer expression)
+ To trigger those forms of :extension:`ScopedTypeVariables`, the ``forall`` must appear against the top-level signature (or outer expression)
but *not* against nested signatures referring to the same type variables.
Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :ref:`pattern-type-sigs`.
@@ -261,11 +261,12 @@ the pattern, rather than the pattern binding the variable.
Class and instance declarations
-------------------------------
-The type variables in the head of a ``class`` or ``instance``
-declaration scope over the methods defined in the ``where`` part. You do
-not even need an explicit ``forall`` (although you are allowed an explicit
-``forall`` in an ``instance`` declaration; see :ref:`explicit-foralls`).
-For example: ::
+:extension:`ScopedTypeVariables` allow the type variables bound by the top of a
+``class`` or ``instance`` declaration to scope over the methods defined in the
+``where`` part. Unlike :ref`decl-type-sigs`, type variables from class and
+instance declarations can be lexically scoped without an explicit ``forall``
+(although you are allowed an explicit ``forall`` in an ``instance``
+declaration; see :ref:`explicit-foralls`). For example: ::
class C a where
op :: [a] -> a
@@ -278,4 +279,36 @@ For example: ::
instance C b => C [b] where
op xs = reverse (head (xs :: [[b]]))
+ -- Alternatively, one could write the instance above as:
+ instance forall b. C b => C [b] where
+ op xs = reverse (head (xs :: [[b]]))
+
+While :extension:`ScopedTypeVariables` is required for type variables from the
+top of a class or instance declaration to scope over the /bodies/ of the
+methods, it is not required for the type variables to scope over the /type
+signatures/ of the methods. For example, the following will be accepted without
+explicitly enabling :extension:`ScopedTypeVariables`: ::
+
+ class D a where
+ m :: [a] -> a
+
+ instance D [a] where
+ m :: [a] -> [a]
+ m = reverse
+
+Note that writing ``m :: [a] -> [a]`` requires the use of the
+:extension:`InstanceSigs` extension.
+
+Similarly, :extension:`ScopedTypeVariables` is not required for type variables
+from the top of the class or instance declaration to scope over associated type
+families, which only requires the :extension:`TypeFamilies` extension. For
+instance, the following will be accepted without explicitly enabling
+:extension:`ScopedTypeVariables`: ::
+
+ class E a where
+ type T a
+
+ instance E [a] where
+ type T [a] = a
+See :ref:`scoping-class-params` for further information.
=====================================
testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
=====================================
@@ -1,6 +1,5 @@
T16326_Fail8.hs:7:10: error:
- Illegal class instance: ‘forall a -> C (Blah a)’
- Class instances must be of the form
- context => C ty_1 ... ty_n
- where ‘C’ is a class
+ Illegal visible, dependent quantification in the type of a term
+ (GHC does not yet support this)
+ In an instance declaration
=====================================
testsuite/tests/dependent/should_fail/T18271.hs
=====================================
@@ -0,0 +1,7 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module T18271 where
+
+class C a
+deriving instance forall a -> C (Maybe a)
=====================================
testsuite/tests/dependent/should_fail/T18271.stderr
=====================================
@@ -0,0 +1,5 @@
+
+T18271.hs:7:19: error:
+ Illegal visible, dependent quantification in the type of a term
+ (GHC does not yet support this)
+ In a deriving declaration
=====================================
testsuite/tests/dependent/should_fail/all.T
=====================================
@@ -65,3 +65,4 @@ test('T14880-2', normal, compile_fail, [''])
test('T15076', normal, compile_fail, [''])
test('T15076b', normal, compile_fail, [''])
test('T17687', normal, compile_fail, [''])
+test('T18271', normal, compile_fail, [''])
=====================================
testsuite/tests/deriving/should_compile/T15831.hs
=====================================
@@ -13,21 +13,21 @@ newtype Age = MkAge Int
deriving Ord
via Const Int (Any :: k)
deriving Read
- via (forall k. Const Int (Any :: k))
+ via forall k. Const Int (Any :: k)
deriving Show
via Const Int a
deriving Enum
via Const Int (a :: k)
deriving Bounded
- via (forall a. Const Int a)
+ via forall a. Const Int a
deriving Num
- via (forall k (a :: k). Const Int a)
+ via forall k (a :: k). Const Int a
newtype Age2 = MkAge2 Int
-deriving via Const Int Any instance Eq Age2
-deriving via Const Int (Any :: k) instance Ord Age2
-deriving via (forall k. Const Int (Any :: k)) instance Read Age2
-deriving via Const Int a instance Show Age2
-deriving via Const Int (a :: k) instance Enum Age2
-deriving via (forall a. Const Int a) instance Bounded Age2
-deriving via (forall k (a :: k). Const Int a) instance Num Age2
+deriving via Const Int Any instance Eq Age2
+deriving via Const Int (Any :: k) instance Ord Age2
+deriving via forall k. Const Int (Any :: k) instance Read Age2
+deriving via Const Int a instance Show Age2
+deriving via Const Int (a :: k) instance Enum Age2
+deriving via forall a. Const Int a instance Bounded Age2
+deriving via forall k (a :: k). Const Int a instance Num Age2
=====================================
testsuite/tests/deriving/should_compile/deriving-via-standalone.hs
=====================================
@@ -37,6 +37,6 @@ data X1 a
data X2 a
data X3 a
-deriving via (forall a. T a) instance Z a (X1 b)
-deriving via (T a) instance forall b. Z a (X2 b)
-deriving via (forall a. T a) instance forall b. Z a (X3 b)
+deriving via forall a. T a instance Z a (X1 b)
+deriving via T a instance forall b. Z a (X2 b)
+deriving via forall a. T a instance forall b. Z a (X3 b)
=====================================
testsuite/tests/deriving/should_fail/deriving-via-fail.hs
=====================================
@@ -12,4 +12,4 @@ newtype Foo2 a b = Foo2 (a -> b)
deriving Category
via fooo
-data Foo3 deriving Eq via (forall a. a)
+data Foo3 deriving Eq via forall a. a
=====================================
testsuite/tests/deriving/should_fail/deriving-via-fail4.hs
=====================================
@@ -14,4 +14,4 @@ newtype F1 = F1 Int
deriving Eq via Char
newtype F2 a = MkF2 a
- deriving (C a) via (forall a. a)
+ deriving (C a) via forall a. a
=====================================
testsuite/tests/parser/should_fail/T3811c.stderr
=====================================
@@ -1,6 +1,7 @@
T3811c.hs:6:10: error:
- Illegal class instance: ‘!Show D’
- Class instances must be of the form
- context => C ty_1 ... ty_n
+ Illegal head of an instance declaration: ‘!Show D’
+ Instance heads must be of the form
+ C ty_1 ... ty_n
where ‘C’ is a class
+ In an instance declaration
=====================================
testsuite/tests/rename/should_fail/T16114.stderr
=====================================
@@ -1,6 +1,4 @@
-T16114.hs:4:10: error:
- Illegal class instance: ‘Eq a => Eq a => Eq (T a)’
- Class instances must be of the form
- context => C ty_1 ... ty_n
- where ‘C’ is a class
+T16114.hs:4:18: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
=====================================
testsuite/tests/rename/should_fail/T18240a.hs
=====================================
@@ -0,0 +1,29 @@
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+module T18240a where
+
+import Data.Proxy
+
+class C a where
+ m :: Proxy a
+
+instance (forall a. C [a]) where
+ m = Proxy @[a]
+
+instance (Eq a => C [a]) where
+ m = Proxy @[a]
+
+instance (forall a. C (Either a b)) where
+ m = Proxy @(Either a b)
+
+instance forall a. (forall b. C (Either a b)) where
+ m = Proxy @(Either a b)
+
+instance Eq a => (Eq b => C (Either a b)) where
+ m = Proxy @(Either a b)
+
+-- Some other nonsensical instance types
+
+instance 42
+instance Int -> Int
=====================================
testsuite/tests/rename/should_fail/T18240a.stderr
=====================================
@@ -0,0 +1,40 @@
+
+T18240a.hs:11:11: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
+
+T18240a.hs:12:15: error: Not in scope: type variable ‘a’
+
+T18240a.hs:14:11: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
+
+T18240a.hs:17:11: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
+
+T18240a.hs:18:22: error: Not in scope: type variable ‘a’
+
+T18240a.hs:20:21: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
+
+T18240a.hs:21:24: error: Not in scope: type variable ‘b’
+
+T18240a.hs:23:19: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
+
+T18240a.hs:28:10: error:
+ Illegal head of an instance declaration: ‘42’
+ Instance heads must be of the form
+ C ty_1 ... ty_n
+ where ‘C’ is a class
+ In an instance declaration
+
+T18240a.hs:29:10: error:
+ Illegal head of an instance declaration: ‘Int -> Int’
+ Instance heads must be of the form
+ C ty_1 ... ty_n
+ where ‘C’ is a class
+ In an instance declaration
=====================================
testsuite/tests/rename/should_fail/T18240b.hs
=====================================
@@ -0,0 +1,29 @@
+{-# LANGUAGE DeriveAnyClass #-}
+{-# LANGUAGE DerivingVia #-}
+{-# LANGUAGE ExplicitForAll #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module T18240b where
+
+import Data.Proxy
+
+data T a b
+
+class W x y z
+instance W x y (T a b)
+
+newtype Foo a b = MkFoo (T a b)
+deriving via (forall x. T x y) instance W x y (Foo a b)
+deriving via forall x. forall y. T x y instance W x y (Foo a b)
+deriving via forall x. (forall y. T x y) instance W x y (Foo a b)
+
+class C1 x
+class C2 x y z
+
+data Bar = MkBar
+ deriving anyclass ( C1
+ , (forall x. C2 x y)
+ , forall x. forall y. C2 x y
+ , forall x. (forall y. C2 x y)
+ )
=====================================
testsuite/tests/rename/should_fail/T18240b.stderr
=====================================
@@ -0,0 +1,24 @@
+
+T18240b.hs:17:15: error:
+ ‘via’ type cannot contain nested ‘forall’s or contexts
+ In a deriving declaration
+
+T18240b.hs:18:24: error:
+ ‘via’ type cannot contain nested ‘forall’s or contexts
+ In a deriving declaration
+
+T18240b.hs:19:25: error:
+ ‘via’ type cannot contain nested ‘forall’s or contexts
+ In a deriving declaration
+
+T18240b.hs:26:24: error:
+ Derived class type cannot contain nested ‘forall’s or contexts
+ In the data type declaration for ‘Bar’
+
+T18240b.hs:27:33: error:
+ Derived class type cannot contain nested ‘forall’s or contexts
+ In the data type declaration for ‘Bar’
+
+T18240b.hs:28:34: error:
+ Derived class type cannot contain nested ‘forall’s or contexts
+ In the data type declaration for ‘Bar’
=====================================
testsuite/tests/rename/should_fail/T5951.stderr
=====================================
@@ -1,6 +1,4 @@
-T5951.hs:8:8: error:
- Illegal class instance: ‘A => B => C’
- Class instances must be of the form
- context => C ty_1 ... ty_n
- where ‘C’ is a class
+T5951.hs:9:8: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
=====================================
testsuite/tests/rename/should_fail/all.T
=====================================
@@ -154,3 +154,5 @@ test('T14548', normal, compile_fail, [''])
test('T16610', normal, compile_fail, [''])
test('T17593', normal, compile_fail, [''])
test('T18145', normal, compile_fail, [''])
+test('T18240a', normal, compile_fail, [''])
+test('T18240b', normal, compile_fail, [''])
=====================================
testsuite/tests/typecheck/should_fail/T16394.stderr
=====================================
@@ -1,5 +1,4 @@
-T16394.hs:6:10: error:
- Illegal class instance: ‘C a => C b => C (a, b)’
- Class instances must be of the form
- context => C ty_1 ... ty_n
- where ‘C’ is a class
+
+T16394.hs:6:17: error:
+ Instance head cannot contain nested ‘forall’s or contexts
+ In an instance declaration
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/15bfa78c6024bc2ca90bbbd15ea9f0ba84b14fe7
--
View it on GitLab: https://gitlab.haskell.org/ghc/ghc/-/commit/15bfa78c6024bc2ca90bbbd15ea9f0ba84b14fe7
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/20200611/f351afbb/attachment-0001.html>
More information about the ghc-commits
mailing list