Reject nested foralls/contexts in instance types more consistentlywip/T18240

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 files changed, 581 insertions, 136 deletions

diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index ccf98857f4..ff67676f25 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -67,7 +67,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,
@@ -102,10 +102,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
 
 {-
 ************************************************************************
@@ -1338,10 +1338,10 @@ splitHsFunType (L _ (HsFunTy _ mult 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
@@ -1437,6 +1437,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@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:
 --
@@ -1454,26 +1474,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_tele =
-                                      HsForAllInvis { hsf_invis_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
@@ -1488,14 +1489,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@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_tele = HsForAllInvis { hsf_invis_bndrs = tvs' }
-               , hst_body = body' }
-      -> (tvs', body')
-    _ -> ([], lty)
+    HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }
+               , hst_body = body }
+      -> (Just tvs, body)
+    _ -> (Nothing, lty)
 
 -- | Decompose a type of the form @context => body@ into its constituent parts.
 --
@@ -1504,41 +1524,142 @@ 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@.
 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
+-----
+
+`deriving` clauses and standalone `deriving` declarations also permit bringing
+type variables into scope, either through explicit or implicit quantification.
+Unlike in the tops of instance declarations, however, one does not need to
+enable ScopedTypeVariables for this to take effect.
+
+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.
+-}
+
+{-
 ************************************************************************
 *                                                                      *
                 FieldOcc
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index cad85e2fe5..aeb94f5d10 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/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)
 
@@ -2184,18 +2230,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_tele = tele })
-             |  HsForAllVis{} <- tele
-             -> 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)" ]
-             |  HsForAllInvis{} <- tele
-             -> 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)
@@ -2204,12 +2242,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)
@@ -2239,6 +2271,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@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_tele = tele })
+      |  HsForAllVis{} <- tele
+         -- 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)" ])
+      |  HsForAllInvis{} <- tele
+      -> 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
diff --git a/docs/users_guide/8.12.1-notes.rst b/docs/users_guide/8.12.1-notes.rst
index deb29310ff..aa602b4f7c 100644
--- a/docs/users_guide/8.12.1-notes.rst
+++ b/docs/users_guide/8.12.1-notes.rst
@@ -150,6 +150,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)
+
 * A new language extension :extension:`QualifiedDo` is implemented, allowing
   to qualify a do block to control which operations to use for desugaring do
   syntax. ::
diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 8287e510dc..bbd146d6b4 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/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: ::
diff --git a/docs/users_guide/exts/instances.rst b/docs/users_guide/exts/instances.rst
index 3dd7969d97..14b2e39a27 100644
--- a/docs/users_guide/exts/instances.rst
+++ b/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
diff --git a/docs/users_guide/exts/scoped_type_variables.rst b/docs/users_guide/exts/scoped_type_variables.rst
index 002686ffd6..d80eb40d0d 100644
--- a/docs/users_guide/exts/scoped_type_variables.rst
+++ b/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.
diff --git a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr b/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
index 16c2aa617e..d7666cf84d 100644
--- a/testsuite/tests/dependent/should_fail/T16326_Fail8.stderr
+++ b/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
diff --git a/testsuite/tests/dependent/should_fail/T18271.hs b/testsuite/tests/dependent/should_fail/T18271.hs
new file mode 100644
index 0000000000..2441fa7318
--- /dev/null
+++ b/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)
diff --git a/testsuite/tests/dependent/should_fail/T18271.stderr b/testsuite/tests/dependent/should_fail/T18271.stderr
new file mode 100644
index 0000000000..0bc21f394d
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/dependent/should_fail/all.T b/testsuite/tests/dependent/should_fail/all.T
index d3d155f163..38c7f45d55 100644
--- a/testsuite/tests/dependent/should_fail/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/deriving/should_compile/T15831.hs b/testsuite/tests/deriving/should_compile/T15831.hs
index 309c8a8e3a..da157aa106 100644
--- a/testsuite/tests/deriving/should_compile/T15831.hs
+++ b/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
diff --git a/testsuite/tests/deriving/should_compile/deriving-via-standalone.hs b/testsuite/tests/deriving/should_compile/deriving-via-standalone.hs
index 26484a2df2..99da015bbd 100644
--- a/testsuite/tests/deriving/should_compile/deriving-via-standalone.hs
+++ b/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)
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail.hs b/testsuite/tests/deriving/should_fail/deriving-via-fail.hs
index 3fa8009638..0cb521de78 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail.hs
+++ 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
diff --git a/testsuite/tests/deriving/should_fail/deriving-via-fail4.hs b/testsuite/tests/deriving/should_fail/deriving-via-fail4.hs
index 1436d994c0..2e16abfa20 100644
--- a/testsuite/tests/deriving/should_fail/deriving-via-fail4.hs
+++ b/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
diff --git a/testsuite/tests/parser/should_fail/T3811c.stderr b/testsuite/tests/parser/should_fail/T3811c.stderr
index 52f081bbe6..6d662a9b16 100644
--- a/testsuite/tests/parser/should_fail/T3811c.stderr
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/T16114.stderr b/testsuite/tests/rename/should_fail/T16114.stderr
index aec0e3e3e0..adbaffc0ef 100644
--- a/testsuite/tests/rename/should_fail/T16114.stderr
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/T18240a.hs b/testsuite/tests/rename/should_fail/T18240a.hs
new file mode 100644
index 0000000000..cf3b8796d6
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/T18240a.stderr b/testsuite/tests/rename/should_fail/T18240a.stderr
new file mode 100644
index 0000000000..641bee5003
--- /dev/null
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/T18240b.hs b/testsuite/tests/rename/should_fail/T18240b.hs
new file mode 100644
index 0000000000..cbadf3d3e5
--- /dev/null
+++ b/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)
+                    )
diff --git a/testsuite/tests/rename/should_fail/T18240b.stderr b/testsuite/tests/rename/should_fail/T18240b.stderr
new file mode 100644
index 0000000000..330e5cc72f
--- /dev/null
+++ b/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’
diff --git a/testsuite/tests/rename/should_fail/T5951.stderr b/testsuite/tests/rename/should_fail/T5951.stderr
index b325493f35..f98fb501ed 100644
--- a/testsuite/tests/rename/should_fail/T5951.stderr
+++ b/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
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 27b359dec1..2647ac706b 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/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, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T16394.stderr b/testsuite/tests/typecheck/should_fail/T16394.stderr
index fff51a6e39..74e5c25ef5 100644
--- a/testsuite/tests/typecheck/should_fail/T16394.stderr
+++ b/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