Extension shuffling (#23291)wip/sand-witch/modern-STV-extension-shuffling

Where introduced 4 new extensions:
  - PatternSignatures
  - ExtendedForAllScope
  - MethodTypeVariables
  - ImplicitForAll

Tasks of ScopedTypeVariables extension were distributed between
PatternSignatures, ExtendedForAllScope and MethodTypeVariables according
to the proposal. Now ScopedTypeVaribles only implies these three exntesions.

Extension ImplicitForAll saves current behavior. NoImplicitForAll
disables implicit bounding of type variables in many contexts.

Was introduced one new warning option: -Wpattern-signature-binds
It warns when pattern signature binds into scope new type variable. For
example:

  f (a :: t) = ...

39 files changed, 439 insertions, 86 deletions

diff --git a/compiler/GHC/Driver/DynFlags.hs b/compiler/GHC/Driver/DynFlags.hs
index 01aa518452..34e702e5ba 100644
--- a/compiler/GHC/Driver/DynFlags.hs
+++ b/compiler/GHC/Driver/DynFlags.hs
@@ -1351,8 +1351,9 @@ languageExtensions (Just Haskell98)
            -- turning it off breaks code, so we're keeping it on for
            -- backwards compatibility.  Cabal uses -XHaskell98 by
            -- default unless you specify another language.
-       LangExt.DeepSubsumption
+       LangExt.DeepSubsumption,
        -- Non-standard but enabled for backwards compatability (see GHC proposal #511)
+       LangExt.ImplicitForAll
       ]
 
 languageExtensions (Just Haskell2010)
@@ -1369,7 +1370,8 @@ languageExtensions (Just Haskell2010)
        LangExt.DoAndIfThenElse,
        LangExt.FieldSelectors,
        LangExt.RelaxedPolyRec,
-       LangExt.DeepSubsumption ]
+       LangExt.DeepSubsumption,
+       LangExt.ImplicitForAll]
 
 languageExtensions (Just GHC2021)
     = [LangExt.ImplicitPrelude,
@@ -1383,6 +1385,7 @@ languageExtensions (Just GHC2021)
        LangExt.DoAndIfThenElse,
        LangExt.FieldSelectors,
        LangExt.RelaxedPolyRec,
+       LangExt.ImplicitForAll,
        -- Now the new extensions (not in Haskell2010)
        LangExt.BangPatterns,
        LangExt.BinaryLiterals,
@@ -1415,12 +1418,15 @@ languageExtensions (Just GHC2021)
        LangExt.RankNTypes,
        LangExt.ScopedTypeVariables,
        LangExt.TypeAbstractions,     -- implied by ScopedTypeVariables according to GHC Proposal #448 "Modern Scoped Type Variables"
+       LangExt.TypeSynonymInstances, -- implied by ScopedTypeVariables according to ^
+       LangExt.PatternSignatures,    -- implied by ScopedTypeVariables according to ^
+       LangExt.MethodTypeVariables,  -- implied by ScopedTypeVariables according to ^
+       LangExt.ExtendedForAllScope,  -- implied by ScopedTypeVariables according to ^
        LangExt.StandaloneDeriving,
        LangExt.StandaloneKindSignatures,
        LangExt.TupleSections,
        LangExt.TypeApplications,
-       LangExt.TypeOperators,
-       LangExt.TypeSynonymInstances]
+       LangExt.TypeOperators]
 
 
 ways :: DynFlags -> Ways
diff --git a/compiler/GHC/Driver/Flags.hs b/compiler/GHC/Driver/Flags.hs
index 759c137eb5..8d33c63c95 100644
--- a/compiler/GHC/Driver/Flags.hs
+++ b/compiler/GHC/Driver/Flags.hs
@@ -637,6 +637,7 @@ data WarningFlag =
    | Opt_WarnLoopySuperclassSolve                    -- Since 9.6
    | Opt_WarnTermVariableCapture                     -- Since 9.8
    | Opt_WarnMissingRoleAnnotations                  -- Since 9.8
+   | Opt_WarnPatternSignatureBinds                   -- Since 9.8
    deriving (Eq, Ord, Show, Enum)
 
 -- | Return the names of a WarningFlag
@@ -744,6 +745,7 @@ warnFlagNames wflag = case wflag of
   Opt_WarnLoopySuperclassSolve                    -> "loopy-superclass-solve" :| []
   Opt_WarnTypeEqualityRequiresOperators           -> "type-equality-requires-operators" :| []
   Opt_WarnMissingRoleAnnotations                  -> "missing-role-annotations" :| []
+  Opt_WarnPatternSignatureBinds                   -> "pattern-signature-binds" :| []
 
 -- -----------------------------------------------------------------------------
 -- Standard sets of warning options
diff --git a/compiler/GHC/Driver/Session.hs b/compiler/GHC/Driver/Session.hs
index dd5bb6b7cb..8199755765 100644
--- a/compiler/GHC/Driver/Session.hs
+++ b/compiler/GHC/Driver/Session.hs
@@ -2250,7 +2250,8 @@ wWarningFlagsDeps = mconcat [
   warnSpec    Opt_WarnTypeEqualityOutOfScope,
   warnSpec    Opt_WarnTypeEqualityRequiresOperators,
   warnSpec    Opt_WarnTermVariableCapture,
-  warnSpec    Opt_WarnMissingRoleAnnotations
+  warnSpec    Opt_WarnMissingRoleAnnotations,
+  warnSpec    Opt_WarnPatternSignatureBinds
  ]
 
 warningGroupsDeps :: [(Deprecation, FlagSpec WarningGroup)]
@@ -2663,8 +2664,10 @@ xFlagsDeps = [
   flagSpec "ParallelListComp"                 LangExt.ParallelListComp,
   flagSpec "PartialTypeSignatures"            LangExt.PartialTypeSignatures,
   flagSpec "PatternGuards"                    LangExt.PatternGuards,
-  depFlagSpec' "PatternSignatures"            LangExt.ScopedTypeVariables
-    (deprecatedForExtension "ScopedTypeVariables"),
+  flagSpec "PatternSignatures"                LangExt.PatternSignatures,
+  flagSpec "MethodTypeVariables"              LangExt.MethodTypeVariables,
+  flagSpec "ExtendedForAllScope"              LangExt.ExtendedForAllScope,
+  flagSpec "ImplicitForAll"                   LangExt.ImplicitForAll,
   flagSpec "PatternSynonyms"                  LangExt.PatternSynonyms,
   flagSpec "PolyKinds"                        LangExt.PolyKinds,
   flagSpec "PolymorphicComponents"            LangExt.RankNTypes,
@@ -2757,6 +2760,9 @@ impliedXFlags
 
     -- In accordance with GHC Proposal #448 "Modern Scoped Type Variables"
     , (LangExt.ScopedTypeVariables,       turnOn, LangExt.TypeAbstractions)
+    , (LangExt.ScopedTypeVariables,       turnOn, LangExt.PatternSignatures)
+    , (LangExt.ScopedTypeVariables,       turnOn, LangExt.MethodTypeVariables)
+    , (LangExt.ScopedTypeVariables,       turnOn, LangExt.ExtendedForAllScope)
 
     , (LangExt.RebindableSyntax, turnOff, LangExt.ImplicitPrelude)      -- NB: turn off!
 
diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index eb3a955269..3b99b14aae 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -819,9 +819,9 @@ enabled. For example, the following will be rejected:
   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/.
+declarations. Namely, if MethodTypeVariables (impied by 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
@@ -841,20 +841,20 @@ 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`.
+bound and the `b` is implicitly bound. Moreover, MethodTypeVariables
+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.
+don't have the same strange interaction with MethodTypeVariables.
 
 Just as we forbid nested `forall`s and contexts in normal instance
 declarations, we also forbid them in SPECIALISE instance pragmas (#18455).
-Unlike normal instance declarations, ScopedTypeVariables don't have any impact
-on SPECIALISE instance pragmas, but we use the same validity checks for
-SPECIALISE instance pragmas anyway to be consistent.
+Unlike normal instance declarations, MethodTypeVariables
+don't have any impact on SPECIALISE instance pragmas, but we use the same
+validity checks for SPECIALISE instance pragmas anyway to be consistent.
 
 -----
 -- Wrinkle: Derived instances
@@ -863,7 +863,7 @@ SPECIALISE instance pragmas anyway to be consistent.
 `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.
+enable MethodTypeVariables 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`:
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index 73af997a2e..80736c0a34 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -519,7 +519,7 @@ rnBind sig_fn bind@(FunBind { fun_id = name
        -- invariant: no free vars here when it's a FunBind
   = do  { let plain_name = unLoc name
 
-        ; (matches', rhs_fvs) <- bindSigTyVarsFV (sig_fn plain_name) $
+        ; (matches', rhs_fvs) <- bindSigTyVarsFVExtended (sig_fn plain_name) $
                                 -- bindSigTyVars tests for LangExt.ScopedTyVars
                                  rnMatchGroup (mkPrefixFunRhs name)
                                               rnLExpr matches
@@ -726,7 +726,7 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
         ; unless pattern_synonym_ok (addErr TcRnIllegalPatternSynonymDecl)
         ; let scoped_tvs = sig_fn name
 
-        ; ((pat', details'), fvs1) <- bindSigTyVarsFV scoped_tvs $
+        ; ((pat', details'), fvs1) <- bindSigTyVarsFVExtended scoped_tvs $
                                       rnPat PatSyn pat $ \pat' ->
          -- We check the 'RdrName's instead of the 'Name's
          -- so that the binding locations are reported
@@ -763,7 +763,7 @@ rnPatSynBind sig_fn bind@(PSB { psb_id = L l name
             Unidirectional -> return (Unidirectional, emptyFVs)
             ImplicitBidirectional -> return (ImplicitBidirectional, emptyFVs)
             ExplicitBidirectional mg ->
-                do { (mg', fvs) <- bindSigTyVarsFV scoped_tvs $
+                do { (mg', fvs) <- bindSigTyVarsFVExtended scoped_tvs $
                                    rnMatchGroup (mkPrefixFunRhs (L l name))
                                                 rnLExpr mg
                    ; return (ExplicitBidirectional mg', fvs) }
@@ -920,7 +920,8 @@ rnMethodBinds is_cls_decl cls ktv_names binds sigs
        -- Rename the bindings RHSs.  Again there's an issue about whether the
        -- type variables from the class/instance head are in scope.
        -- Answer no in Haskell 2010, but yes if you have -XScopedTypeVariables
-       ; (binds'', bind_fvs) <- bindSigTyVarsFV ktv_names $
+       -- or -XMethodTypeVariables
+       ; (binds'', bind_fvs) <- bindSigTyVarsFVMethod ktv_names $
               do { binds_w_dus <- mapBagM (rnLBind (mkScopedTvFn other_sigs')) binds'
                  ; let bind_fvs = foldr (\(_,_,fv1) fv2 -> fv1 `plusFV` fv2)
                                            emptyFVs binds_w_dus
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 2afc0f0fa6..184b5f8550 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -521,7 +521,7 @@ rnExpr (HsRecSel x _) = dataConCantHappen x
 
 rnExpr (ExprWithTySig _ expr pty)
   = do  { (pty', fvTy)    <- rnHsSigWcType ExprWithTySigCtx pty
-        ; (expr', fvExpr) <- bindSigTyVarsFV (hsWcScopedTvs pty') $
+        ; (expr', fvExpr) <- bindSigTyVarsFVExtended (hsWcScopedTvs pty') $
                              rnLExpr expr
         ; return (ExprWithTySig noExtField expr' pty', fvExpr `plusFV` fvTy) }
 
diff --git a/compiler/GHC/Rename/HsType.hs b/compiler/GHC/Rename/HsType.hs
index 049bbe2c22..7ab390615a 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -31,7 +31,8 @@ module GHC.Rename.HsType (
         -- Binding related stuff
         bindHsOuterTyVarBndrs, bindHsForAllTelescope,
         bindLHsTyVarBndr, bindLHsTyVarBndrs, WarnUnusedForalls(..),
-        rnImplicitTvOccs, bindSigTyVarsFV, bindHsQTyVars,
+        rnImplicitTvOccs, bindSigTyVarsFVExtended, bindSigTyVarsFVMethod,
+        bindHsQTyVars,
         FreeKiTyVars, filterInScopeM,
         extractHsTyRdrTyVars, extractHsTyRdrTyVarsKindVars,
         extractHsTysRdrTyVars, extractRdrKindSigVars,
@@ -150,14 +151,14 @@ rnHsPatSigType :: HsPatSigTypeScoping
                -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
                -> RnM (a, FreeVars)
 -- Used for
---   - Pattern type signatures, which are only allowed with ScopedTypeVariables
+--   - Pattern type signatures, which are only allowed with PatternSignatures
 --   - Signatures on binders in a RULE, which are allowed even if
---     ScopedTypeVariables isn't enabled
+--     PatternSignatures isn't enabled
 -- Wildcards are allowed
 --
 -- See Note [Pattern signature binders and scoping] in GHC.Hs.Type
 rnHsPatSigType scoping ctx sig_ty thing_inside
-  = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
+  = do { ty_sig_okay <- xoptM LangExt.PatternSignatures
        ; checkErr ty_sig_okay (unexpectedPatSigTypeErr sig_ty)
        ; free_vars <- filterInScopeM (extractHsTyRdrTyVars pat_sig_ty)
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
@@ -165,6 +166,9 @@ rnHsPatSigType scoping ctx sig_ty thing_inside
              implicit_bndrs = case scoping of
                AlwaysBind -> tv_rdrs
                NeverBind  -> []
+       ; let i_bndrs = nubN implicit_bndrs in
+          unless (null i_bndrs) $
+            addDiagnostic (TcRnPatternSignatureBinds i_bndrs)
        ; rnImplicitTvOccs Nothing implicit_bndrs $ \ imp_tvs ->
     do { (nwcs, pat_sig_ty', fvs1) <- rnWcBody ctx nwc_rdrs pat_sig_ty
        ; let sig_names = HsPSRn { hsps_nwcs = nwcs, hsps_imp_tvs = imp_tvs }
@@ -386,6 +390,10 @@ rnImplicitTvOccs :: Maybe assoc
                  -> RnM (a, FreeVars)
 rnImplicitTvOccs mb_assoc implicit_vs_with_dups thing_inside
   = do { let implicit_vs = nubN implicit_vs_with_dups
+       ; unlessXOptM LangExt.ImplicitForAll $
+         unless (null implicit_vs) $
+         addErr (TcRnImplicitForAll implicit_vs)
+
        ; mapM_ warn_term_var_capture implicit_vs
 
        ; traceRn "rnImplicitTvOccs" $
@@ -900,18 +908,27 @@ notInKinds _ _ = return ()
 *                                                      *
 ***************************************************** -}
 
-bindSigTyVarsFV :: [Name]
-                -> RnM (a, FreeVars)
-                -> RnM (a, FreeVars)
+bindSigTyVarsFVExtended, bindSigTyVarsFVMethod :: [Name]
+                                               -> RnM (a, FreeVars)
+                                               -> RnM (a, FreeVars)
 -- Used just before renaming the defn of a function
 -- with a separate type signature, to bring its tyvars into scope
--- With no -XScopedTypeVariables, this is a no-op
-bindSigTyVarsFV tvs thing_inside
-  = do  { scoped_tyvars <- xoptM LangExt.ScopedTypeVariables
-        ; if not scoped_tyvars then
-                thing_inside
-          else
-                bindLocalNamesFV tvs thing_inside }
+-- With no -XExtendedForAllScope/-XMethodTypeVariables, this is a no-op
+(bindSigTyVarsFVExtended, bindSigTyVarsFVMethod)
+  = ( bindSigTyVarsFVIfEnabled LangExt.ExtendedForAllScope
+    , bindSigTyVarsFVIfEnabled LangExt.MethodTypeVariables
+    )
+  where
+    bindSigTyVarsFVIfEnabled :: LangExt.Extension
+                             -> [Name]
+                             -> RnM (a, FreeVars)
+                             -> RnM (a, FreeVars)
+    bindSigTyVarsFVIfEnabled lang_ext tvs thing_inside
+      = do  { can_tyvars_be_in_scope <- xoptM lang_ext
+            ; if not can_tyvars_be_in_scope then
+                    thing_inside
+              else
+                    bindLocalNamesFV tvs thing_inside }
 
 ---------------
 bindHsQTyVars :: forall a b.
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index 319dececdd..69e312a6e3 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -198,7 +198,7 @@ rnSrcDecls group@(HsGroup { hs_valds   = val_decls,
 
    -- (H) Rename Everything else
 
-   (rn_rule_decls,    src_fvs2) <- setXOptM LangExt.ScopedTypeVariables $
+   (rn_rule_decls,    src_fvs2) <- setXOptM LangExt.PatternSignatures $
                                    rnList rnHsRuleDecls rule_decls ;
                            -- Inside RULES, scoped type variables are on
    (rn_foreign_decls, src_fvs3) <- rnList rnHsForeignDecl foreign_decls ;
diff --git a/compiler/GHC/Tc/Deriv.hs b/compiler/GHC/Tc/Deriv.hs
index 4d7bf81f6c..b5cb247d02 100644
--- a/compiler/GHC/Tc/Deriv.hs
+++ b/compiler/GHC/Tc/Deriv.hs
@@ -273,7 +273,9 @@ renameDeriv inst_infos bagBinds
     setXOptM LangExt.EmptyCase $
     -- Derived decls (for empty types) can have
     --    case x of {}
-    setXOptM LangExt.ScopedTypeVariables $
+    setXOptM LangExt.MethodTypeVariables $
+    setXOptM LangExt.PatternSignatures $
+    setXOptM LangExt.ExtendedForAllScope $
     setXOptM LangExt.KindSignatures $
     -- Derived decls (for newtype-deriving) can use ScopedTypeVariables &
     -- KindSignatures
diff --git a/compiler/GHC/Tc/Deriv/Generate.hs b/compiler/GHC/Tc/Deriv/Generate.hs
index 9a76c82b8f..b8678e4344 100644
--- a/compiler/GHC/Tc/Deriv/Generate.hs
+++ b/compiler/GHC/Tc/Deriv/Generate.hs
@@ -1875,9 +1875,9 @@ of the method. For example, recall:
                   join
 
 In the example above, it is imperative that the `a` in the instance signature
-for `join` scope over the body of `join` by way of ScopedTypeVariables.
-This might sound obvious, but note that in gen_Newtype_binds, which is
-responsible for generating the code above, the type in `join`'s instance
+for `join` scope over the body of `join` by way of ExtendedForallScope (implied
+by ScopedTypeVariables). This might sound obvious, but note that in gen_Newtype_binds,
+which is responsible for generating the code above, the type in `join`'s instance
 signature is given as a Core type, whereas gen_Newtype_binds will eventually
 produce HsBinds (i.e., source Haskell) that is renamed and typechecked. We
 must ensure that `a` is in scope over the body of `join` during renaming
diff --git a/compiler/GHC/Tc/Errors/Ppr.hs b/compiler/GHC/Tc/Errors/Ppr.hs
index a9b1084914..fe5b9c91c2 100644
--- a/compiler/GHC/Tc/Errors/Ppr.hs
+++ b/compiler/GHC/Tc/Errors/Ppr.hs
@@ -1726,9 +1726,7 @@ instance Diagnostic TcRnMessage where
              nest 4 (text "in the section:" <+> quotes (ppr section))]
 
     TcRnUnexpectedPatSigType ty
-      -> mkSimpleDecorated $
-           hang (text "Illegal type signature:" <+> quotes (ppr ty))
-              2 (text "Type signatures are only allowed in patterns with ScopedTypeVariables")
+      -> mkSimpleDecorated $ text "Illegal type signature:" <+> quotes (ppr ty)
 
     TcRnIllegalKindSignature ty
       -> mkSimpleDecorated $ text "Illegal kind signature:" <+> quotes (ppr ty)
@@ -1882,6 +1880,14 @@ instance Diagnostic TcRnMessage where
     TcRnNonCanonicalDefinition reason inst_ty
       -> mkSimpleDecorated $
          pprNonCanonicalDefinition inst_ty reason
+    TcRnImplicitForAll fvars -> mkSimpleDecorated $
+      text "Unbound type variable" <> plural fvars <> text ":"
+      <+> pprQuotedList fvars
+
+    TcRnPatternSignatureBinds fvars -> mkSimpleDecorated $
+      sep  [text "Type variable binding" <> plural fvars
+           , text "in pattern signature:" <+> pprQuotedList fvars
+           ]
     TcRnUnexpectedDeclarationSplice {}
       -> mkSimpleDecorated $
          text "Declaration splices are not permitted" <+>
@@ -2542,6 +2548,10 @@ instance Diagnostic TcRnMessage where
       -> WarningWithFlag Opt_WarnNonCanonicalMonadInstances
     TcRnUnexpectedDeclarationSplice {}
       -> ErrorWithoutFlag
+    TcRnImplicitForAll{}
+      -> ErrorWithoutFlag
+    TcRnPatternSignatureBinds{}
+      -> WarningWithFlag Opt_WarnPatternSignatureBinds
     TcRnImplicitImportOfPrelude {}
       -> WarningWithFlag Opt_WarnImplicitPrelude
     TcRnMissingMain {}
@@ -3151,7 +3161,7 @@ instance Diagnostic TcRnMessage where
     TcRnSectionPrecedenceError{}
       -> noHints
     TcRnUnexpectedPatSigType{}
-      -> [suggestExtension LangExt.ScopedTypeVariables]
+      -> [suggestExtension LangExt.PatternSignatures]
     TcRnIllegalKindSignature{}
       -> [suggestExtension LangExt.KindSignatures]
     TcRnUnusedQuantifiedTypeVar{}
@@ -3221,6 +3231,10 @@ instance Diagnostic TcRnMessage where
       -> noHints
     TcRnNonCanonicalDefinition reason _
       -> suggestNonCanonicalDefinition reason
+    TcRnImplicitForAll{}
+      -> [suggestExtension LangExt.ImplicitForAll]
+    TcRnPatternSignatureBinds{}
+      -> noHints
     TcRnUnexpectedDeclarationSplice {}
       -> noHints
     TcRnImplicitImportOfPrelude {}
diff --git a/compiler/GHC/Tc/Errors/Types.hs b/compiler/GHC/Tc/Errors/Types.hs
index 41fa0515ee..33e7bc9c53 100644
--- a/compiler/GHC/Tc/Errors/Types.hs
+++ b/compiler/GHC/Tc/Errors/Types.hs
@@ -2332,7 +2332,7 @@ data TcRnMessage where
     -> TcRnMessage
 
   {-| TcRnUnexpectedPatSigType is an error occurring when there is
-      a type signature in a pattern without -XScopedTypeVariables extension
+      a type signature in a pattern without -XPatternSignatures extension
 
       Examples:
         f (a :: Bool) = ...
@@ -4180,6 +4180,31 @@ data TcRnMessage where
   -}
   TcRnMissingRoleAnnotation :: Name -> [Role] -> TcRnMessage
 
+  {-| TcRnImplicitForAll is an error thrown when a user uses
+      type variables not bound by a forall without
+      enabling the ImplicitForAll extension.
+
+     Example(s):
+
+       id :: a -> a
+       id x = x
+
+     Test case: rename/should_fail/RnNoImplicitForAll
+  -}
+  TcRnImplicitForAll :: [LocatedN RdrName] -> TcRnMessage
+
+  {-| TcRnPatternSignatureBinds is a warning thrown when a user binds
+      type variables in a pattern signature. This is only performed with
+      -Wpattern-signature-binds
+
+     Example(s):
+
+       id (x :: b) = x
+
+     Test case: rename/should_fail/WPatternSigBinds
+  -}
+  TcRnPatternSignatureBinds :: [LocatedN RdrName] -> TcRnMessage
+
   deriving Generic
 
 -- | Things forbidden in @type data@ declarations.
diff --git a/compiler/GHC/Types/Error/Codes.hs b/compiler/GHC/Types/Error/Codes.hs
index 25f78f9fbd..0a6e85a6bd 100644
--- a/compiler/GHC/Types/Error/Codes.hs
+++ b/compiler/GHC/Types/Error/Codes.hs
@@ -600,6 +600,8 @@ type family GhcDiagnosticCode c = n | n -> c where
   GhcDiagnosticCode "TcRnBindingNameConflict"                       = 10498
   GhcDiagnosticCode "NonCanonicalMonoid"                            = 50928
   GhcDiagnosticCode "NonCanonicalMonad"                             = 22705
+  GhcDiagnosticCode "TcRnImplicitForAll"                            = 78543
+  GhcDiagnosticCode "TcRnPatternSignatureBinds"                     = 65467
   GhcDiagnosticCode "TcRnUnexpectedDeclarationSplice"               = 17599
   GhcDiagnosticCode "TcRnImplicitImportOfPrelude"                   = 20540
   GhcDiagnosticCode "TcRnMissingMain"                               = 67120
diff --git a/docs/users_guide/expected-undocumented-flags.txt b/docs/users_guide/expected-undocumented-flags.txt
index 6fa3f2f27d..2d820ace20 100644
--- a/docs/users_guide/expected-undocumented-flags.txt
+++ b/docs/users_guide/expected-undocumented-flags.txt
@@ -14,7 +14,6 @@
 -XMonomorphismRestriction
 -XParallelArrays
 -XPatternGuards
--XPatternSignatures
 -XPolymorphicComponents
 -XRecordPuns
 -XRelaxedLayout
diff --git a/docs/users_guide/exts/explicit_forall.rst b/docs/users_guide/exts/explicit_forall.rst
index 5a6212ee4b..50e797f85d 100644
--- a/docs/users_guide/exts/explicit_forall.rst
+++ b/docs/users_guide/exts/explicit_forall.rst
@@ -114,7 +114,7 @@ The ``forall``-or-nothing rule takes effect in the following places:
 
 Notes:
 
-- :ref:`pattern-type-sigs` are a notable example of a place where
+- :extension:`PatternSignatures` are a notable example of a place where
   types do *not* obey the ``forall``-or-nothing rule. For example, GHC will
   accept the following: ::
 
diff --git a/docs/users_guide/exts/gadt.rst b/docs/users_guide/exts/gadt.rst
index 89ecf8473d..0382479104 100644
--- a/docs/users_guide/exts/gadt.rst
+++ b/docs/users_guide/exts/gadt.rst
@@ -194,7 +194,7 @@ also sets :extension:`GADTSyntax` and :extension:`MonoLocalBinds`.
 
    In the function clause for ``g``, GHC first checks ``MkF``, the outermost
    pattern, followed by the inner ``Nothing`` pattern. This outside-in order
-   can interact somewhat counterintuitively with :ref:`pattern-type-sigs`.
+   can interact somewhat counterintuitively with :extension:`PatternSignatures`.
    Consider the following variation of ``g``: ::
 
        g2 :: F a a -> a
diff --git a/docs/users_guide/exts/implicit_forall.rst b/docs/users_guide/exts/implicit_forall.rst
new file mode 100644
index 0000000000..de9f77e45d
--- /dev/null
+++ b/docs/users_guide/exts/implicit_forall.rst
@@ -0,0 +1,76 @@
+Implicit ForAll
+===============
+
+.. extension:: ImplicitForAll
+    :shortdesc: Implicitly bind free type variables.
+
+    :since: 9.8.1
+
+    :status: Included in :extension:`GHC2021`
+
+    If a type signature does not have an explicit ``forall`` at the top, add an implicit one
+    that binds all the type variables mentioned in the signature that are not already in scope.
+
+
+:extension:`ImplicitForAll` creates an implicit ``forall`` in:
+
+- Type signatures for variable declarations, methods, and foreign imports and exports::
+
+    let f :: a -> a; f = ... in ...
+    -- becomes
+    let f :: forall a. a -> a; f = ... in ...
+
+- Kind signatures::
+
+    type T :: k -> Type
+    -- becomes
+    type T :: forall k. k -> Type
+
+- GADT constructor declarations::
+
+    MkG :: a -> Maybe b -> G (Either Int b)
+    -- becomes
+    MkG :: forall a b. a -> Maybe b -> G (Either Int b)
+
+- Pattern synonym signatures::
+
+    pattern P :: a -> Maybe a
+    -- becomes
+    pattern P :: forall a. a -> Maybe a
+
+- Type annotations in expressions and ``SPECIALISE`` pragmas::
+
+    Right True :: Either a Bool
+    -- becomes
+    Right True :: forall a. Either a Bool
+
+- Types in a ``deriving`` clause::
+
+    data T deriving (C a)
+    -- becomes
+    data T deriving (forall a. C a)
+
+- Instance heads, including standalone ``deriving`` instances::
+
+    instance Show a => Show (Maybe a)
+    -- becomes
+    instance forall a. Show a => Show (Maybe a)
+
+- Type and data family instances, as well as closed ``type family`` equations::
+
+    type instance F (Maybe a) = Int
+    -- becomes
+    type instance forall a. F (Maybe a) = Int
+
+- ``RULES`` pragmas::
+
+    {-# RULES "name" forall (x :: Maybe a). foo x = 5 #-}
+    -- becomes
+    {-# RULES "name" forall a. forall (x :: Maybe a). foo x = 5 #-}
+
+:extension:`ImplicitForAll` also allows binding type variables in pattern
+signatures, but there is still no explicit analogue::
+
+    f (a :: t) = ...
+    -- would be like
+    f @t (a :: t) = ...
diff --git a/docs/users_guide/exts/scoped_type_variables.rst b/docs/users_guide/exts/scoped_type_variables.rst
index ee6a77f32a..15972c9d08 100644
--- a/docs/users_guide/exts/scoped_type_variables.rst
+++ b/docs/users_guide/exts/scoped_type_variables.rst
@@ -6,9 +6,13 @@ Lexically scoped type variables
 ===============================
 
 .. extension:: ScopedTypeVariables
-    :shortdesc: Enable lexically-scoped type variables.
+    :shortdesc: Enable lexically-scoped type variables everywhere.
 
-    :implies: :extension:`ExplicitForAll`
+    :implies: :extension:`ExplicitForAll`,
+      :extension:`PatternSignatures`,
+      :extension:`ExtendedForAllScope`,
+      :extension:`MethodTypeVariables`,
+      :extension:`TypeAbstractions`
 
     :since: 6.8.1
 
@@ -26,7 +30,7 @@ Lexically scoped type variables
     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`.
+    Explicit ``forall`` is not always required -- see :ref:`pattern signature equivalent <pattern-equiv-form>` for the example in this section, or :extension:`PatternSignatures`.
 
 GHC supports *lexically scoped type variables*, without which some type
 signatures are simply impossible to write. For example: ::
@@ -48,7 +52,7 @@ possible to do so.
 
 .. _pattern-equiv-form:
 
-An equivalent form for that example, avoiding explicit ``forall`` uses :ref:`pattern-type-sigs`: ::
+An equivalent form for that example, avoiding explicit ``forall`` uses :extension:`PatternSignatures`: ::
 
     f :: [a] -> [a]
     f (xs :: [aa]) = xs ++ ys
@@ -84,9 +88,9 @@ A *lexically scoped type variable* can be bound by:
 
 -  An expression type signature (:ref:`exp-type-sigs`)
 
--  A pattern type signature (:ref:`pattern-type-sigs`)
+-  A pattern type signature (:extension:`PatternSignatures`)
 
--  Class and instance declarations (:ref:`cls-inst-scoped-tyvars`)
+-  Class and instance declarations (:extension:`MethodTypeVariables`)
 
 In Haskell, a programmer-written type signature is implicitly quantified
 over its free type variables (`Section
@@ -100,14 +104,31 @@ scope is *not* universally quantified. For example, if type variable
       (e :: b -> b)     means     (e :: forall b. b->b)
       (e :: a -> b)     means     (e :: forall b. a->b)
 
+Extended ForAll Scope
+=====================
+
+.. extension:: ExtendedForAllScope
+    :shortdesc: Enable lexically-scoped type variables in function bindings,
+                pattern synonyms and expression type signatures.
+
+    :since: 9.8.1
+
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Enable lexical scoping of type variables explicitly introduced with
+    a ``forall`` in function bindings, pattern synonyms and expression type signatures.
+
 .. _decl-type-sigs:
 
 Declaration type signatures
 ---------------------------
 
-A declaration type signature that has *explicit* quantification (using
-``forall``) brings into scope the explicitly-quantified type variables,
-in the definition of the named function. For example: ::
+When :extension:`ExtendedForAllScope` is enabled, a declaration type signature
+that has *explicit* quantification (using ``forall``) brings into scope the
+explicitly-quantified type variables, in the definition of the named function.
+For example: ::
 
       f :: forall a. [a] -> [a]
       f (x:xs) = xs ++ [ x :: a ]
@@ -171,9 +192,9 @@ This only happens if:
 Expression type signatures
 --------------------------
 
-An expression type signature that has *explicit* quantification (using
-``forall``) brings into scope the explicitly-quantified type variables,
-in the annotated expression. For example: ::
+When :extension:`ExtendedForAllScope` is enabled, an expression type signature
+that has *explicit* quantification (using ``forall``) brings into scope the
+explicitly-quantified type variables, in the annotated expression. For example: ::
 
     f = runST ( (op >>= \(x :: STRef s Int) -> g x) :: forall s. ST s Bool )
 
@@ -181,13 +202,22 @@ Here, the type signature ``forall s. ST s Bool`` brings the type
 variable ``s`` into scope, in the annotated expression
 ``(op >>= \(x :: STRef s Int) -> g x)``.
 
-.. _pattern-type-sigs:
+Pattern Signatures
+==================
 
-Pattern type signatures
------------------------
+.. extension:: PatternSignatures
+    :shortdesc: Allow type signatures in patterns.
 
-A type signature may occur in any pattern; this is a *pattern type
-signature*. For example: ::
+    :since: 9.8.1
+
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Allow type signatures and type variable bindings in patterns.
+
+When :extension:`PatternSignatures` is enabled, a type signature may occur
+in any pattern; this is a *pattern type signature*. For example: ::
 
     -- f and g assume that 'a' is already in scope
     f = \(x::Int, y::a) -> x
@@ -259,12 +289,22 @@ they are both legal whether or not ``a`` is already in scope.
 They differ in that *if* ``a`` is already in scope, the signature constrains
 the pattern, rather than the pattern binding the variable.
 
-.. _cls-inst-scoped-tyvars:
+Method Type Variables
+=====================
+
+.. extension:: MethodTypeVariables
+    :shortdesc: Enable lexically-scoped type variables in class and instance declarations.
+
+    :since: 9.8.1
 
-Class and instance declarations
--------------------------------
+    :implied by: :extension:`ScopedTypeVariables`
+
+    :status: Included in :extension:`GHC2021`
+
+    Enable lexical scoping of type variables explicitly introduced with
+    ``forall`` in class and instance declarations.
 
-:extension:`ScopedTypeVariables` allow the type variables bound by the top of a
+:extension:`MethodTypeVariables` 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``
@@ -286,11 +326,11 @@ declaration; see :ref:`explicit-foralls`). For example: ::
       instance forall b. C b => C [b] where
         op xs = reverse (head (xs :: [[b]]))
 
-While :extension:`ScopedTypeVariables` is required for type variables from the
+While :extension:`MethodTypeVariables` 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`: ::
+explicitly enabling :extension:`MethodTypeVariables`: ::
 
       class D a where
         m :: [a] -> a
@@ -302,11 +342,11 @@ explicitly enabling :extension:`ScopedTypeVariables`: ::
 Note that writing ``m :: [a] -> [a]`` requires the use of the
 :extension:`InstanceSigs` extension.
 
-Similarly, :extension:`ScopedTypeVariables` is not required for type variables
+Similarly, :extension:`MethodTypeVariables` 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`: ::
+:extension:`MethodTypeVariables`: ::
 
       class E a where
         type T a
diff --git a/docs/users_guide/exts/type_abstractions.rst b/docs/users_guide/exts/type_abstractions.rst
index ca8761f405..7b109e4fad 100644
--- a/docs/users_guide/exts/type_abstractions.rst
+++ b/docs/users_guide/exts/type_abstractions.rst
@@ -6,6 +6,8 @@ Type abstractions
 
     :since: 9.8.1
 
+    :implied by: :extension:`ScopedTypeVariables`
+
     :status: Partially implemented
 
     Allow the use of type abstraction syntax.
diff --git a/docs/users_guide/exts/type_signatures.rst b/docs/users_guide/exts/type_signatures.rst
index 9d0fcdc5bb..67b1f904df 100644
--- a/docs/users_guide/exts/type_signatures.rst
+++ b/docs/users_guide/exts/type_signatures.rst
@@ -7,6 +7,7 @@ Type signatures
     :maxdepth: 1
 
     explicit_forall
+    implicit_forall
     ambiguous_types
     kind_signatures
     scoped_type_variables
diff --git a/docs/users_guide/using-warnings.rst b/docs/users_guide/using-warnings.rst
index 922a9638c0..9d0ab1f667 100644
--- a/docs/users_guide/using-warnings.rst
+++ b/docs/users_guide/using-warnings.rst
@@ -2415,6 +2415,28 @@ of ``-W(no-)*``.
     In other words the type-class role cannot be accidentally left
     representational or phantom, which could affected the code correctness.
 
+.. ghc-flag:: -Wpattern-signature-binds
+    :shortdesc: warn when pattern signature binds new type variable
+    :type: dynamic
+
+    :since: 9.8.1
+
+    Added in accordance with `GHC Proposal #448
+    <https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0448-type-variable-scoping.rst>`__.
+
+    Type variable bindings in pattern signatures violate the Lexical Scoping Principle: depending
+    on the context, type variables in the pattern signatures can be either occurrences or bindings.
+
+    For example: ::
+
+       f (x :: a) = ... -- binding of ‘a’
+
+       g :: forall a . ...
+       g (x :: a) = ... -- occurrence of ‘a’
+
+    When :ghc-flag:`-Wpattern-signature-binds` is enabled, GHC warns agains type variable bindings
+    in pattern signatures.
+
 
 If you're feeling really paranoid, the :ghc-flag:`-dcore-lint` option is a good choice.
 It turns on heavyweight intra-pass sanity-checking within GHC. (It checks GHC's
diff --git a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
index e3bd35cbbb..b12e5deb58 100644
--- a/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
+++ b/libraries/ghc-boot-th/GHC/LanguageExtensions/Type.hs
@@ -153,6 +153,10 @@ data Extension
    | OverloadedRecordUpdate
    | TypeAbstractions
    | ExtendedLiterals
+   | PatternSignatures
+   | ExtendedForAllScope
+   | MethodTypeVariables
+   | ImplicitForAll
    deriving (Eq, Enum, Show, Generic, Bounded)
 -- 'Ord' and 'Bounded' are provided for GHC API users (see discussions
 -- in https://gitlab.haskell.org/ghc/ghc/merge_requests/2707 and
diff --git a/testsuite/tests/driver/T4437.hs b/testsuite/tests/driver/T4437.hs
index 142c348fca..5c81cf0525 100644
--- a/testsuite/tests/driver/T4437.hs
+++ b/testsuite/tests/driver/T4437.hs
@@ -38,7 +38,10 @@ check title expected got
 expectedGhcOnlyExtensions :: [String]
 expectedGhcOnlyExtensions =
     [ "TypeAbstractions",
-      "ExtendedLiterals"
+      "ExtendedLiterals",
+      "MethodTypeVariables",
+      "ExtendedForAllScope",
+      "ImplicitForAll"
     ]
 
 expectedCabalOnlyExtensions :: [String]
diff --git a/testsuite/tests/rename/should_fail/RnNoImplicitForAll.hs b/testsuite/tests/rename/should_fail/RnNoImplicitForAll.hs
new file mode 100644
index 0000000000..03147242d8
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/RnNoImplicitForAll.hs
@@ -0,0 +1,36 @@
+{-# LANGUAGE NoImplicitForAll, GADTs, DeriveAnyClass #-}
+
+module RnNoImplicitForAll where
+
+import GHC.Types
+
+f :: a -> a
+f = undefined
+
+type T :: k -> Type
+data T k
+
+data G a where
+  MkG :: a -> Maybe b -> G (Either Int b)
+
+rightTrue = Right True :: Either a Bool
+
+munit :: forall m a . Monad m => m a
+munit = pure undefined
+{-# SPECIALISE munit :: IO a #-}
+
+class C a b
+
+data TD deriving (C a)
+
+instance Show a => Show (Maybe a)
+
+type family F a
+
+type instance F (Maybe a) = Int
+
+{-# RULES "name" forall (x :: Maybe a). foo x = 5 #-}
+
+foo x = 5
+
+id (a :: t) = t
diff --git a/testsuite/tests/rename/should_fail/RnNoImplicitForAll.stderr b/testsuite/tests/rename/should_fail/RnNoImplicitForAll.stderr
new file mode 100644
index 0000000000..ff3918ded3
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/RnNoImplicitForAll.stderr
@@ -0,0 +1,40 @@
+
+RnNoImplicitForAll.hs:7:1: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:10:11: error: [GHC-78543]
+    Unbound type variable: ‘k’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:14:3: error: [GHC-78543]
+    Unbound type variables: ‘a’, ‘b’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:16:13: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:20:25: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:24:19: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:26:10: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:30:1: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:32:11: error: [GHC-78543]
+    Unbound type variable: ‘a’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
+
+RnNoImplicitForAll.hs:36:5: error: [GHC-78543]
+    Unbound type variable: ‘t’
+    Suggested fix: Perhaps you intended to use ImplicitForAll
diff --git a/testsuite/tests/rename/should_fail/T11663.stderr b/testsuite/tests/rename/should_fail/T11663.stderr
index 4602d1992a..ae0e512dbe 100644
--- a/testsuite/tests/rename/should_fail/T11663.stderr
+++ b/testsuite/tests/rename/should_fail/T11663.stderr
@@ -1,20 +1,16 @@
 
 T11663.hs:6:12: error: [GHC-74097]
     Illegal type signature: ‘Int’
-      Type signatures are only allowed in patterns with ScopedTypeVariables
-    Suggested fix: Perhaps you intended to use ScopedTypeVariables
+    Suggested fix: Perhaps you intended to use PatternSignatures
 
 T11663.hs:7:9: error: [GHC-74097]
     Illegal type signature: ‘Int’
-      Type signatures are only allowed in patterns with ScopedTypeVariables
-    Suggested fix: Perhaps you intended to use ScopedTypeVariables
+    Suggested fix: Perhaps you intended to use PatternSignatures
 
 T11663.hs:8:22: error: [GHC-74097]
     Illegal type signature: ‘Int’
-      Type signatures are only allowed in patterns with ScopedTypeVariables
-    Suggested fix: Perhaps you intended to use ScopedTypeVariables
+    Suggested fix: Perhaps you intended to use PatternSignatures
 
 T11663.hs:9:32: error: [GHC-74097]
     Illegal type signature: ‘Int’
-      Type signatures are only allowed in patterns with ScopedTypeVariables
-    Suggested fix: Perhaps you intended to use ScopedTypeVariables
+    Suggested fix: Perhaps you intended to use PatternSignatures
diff --git a/testsuite/tests/rename/should_fail/WPatternSigBinds.hs b/testsuite/tests/rename/should_fail/WPatternSigBinds.hs
new file mode 100644
index 0000000000..b3bdd68675
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/WPatternSigBinds.hs
@@ -0,0 +1,8 @@
+{-# OPTIONS_GHC -Wpattern-signature-binds -Werror #-}
+module WPatternSigBinds where
+
+f (x :: a) = x
+
+g (x :: a) (y :: b) = x
+
+h (x :: a) (y :: b c d) = x
diff --git a/testsuite/tests/rename/should_fail/WPatternSigBinds.stderr b/testsuite/tests/rename/should_fail/WPatternSigBinds.stderr
new file mode 100644
index 0000000000..f859316889
--- /dev/null
+++ b/testsuite/tests/rename/should_fail/WPatternSigBinds.stderr
@@ -0,0 +1,15 @@
+
+WPatternSigBinds.hs:4:4: error: [GHC-65467] [-Wpattern-signature-binds, Werror=pattern-signature-binds]
+    Type variable binding in pattern signature: ‘a’
+
+WPatternSigBinds.hs:6:4: error: [GHC-65467] [-Wpattern-signature-binds, Werror=pattern-signature-binds]
+    Type variable binding in pattern signature: ‘a’
+
+WPatternSigBinds.hs:6:13: error: [GHC-65467] [-Wpattern-signature-binds, Werror=pattern-signature-binds]
+    Type variable binding in pattern signature: ‘b’
+
+WPatternSigBinds.hs:8:4: error: [GHC-65467] [-Wpattern-signature-binds, Werror=pattern-signature-binds]
+    Type variable binding in pattern signature: ‘a’
+
+WPatternSigBinds.hs:8:13: error: [GHC-65467] [-Wpattern-signature-binds, Werror=pattern-signature-binds]
+    Type variable bindings in pattern signature: ‘b’, ‘c’, ‘d’
diff --git a/testsuite/tests/rename/should_fail/all.T b/testsuite/tests/rename/should_fail/all.T
index 883476aac5..b2cc4cd56c 100644
--- a/testsuite/tests/rename/should_fail/all.T
+++ b/testsuite/tests/rename/should_fail/all.T
@@ -198,3 +198,5 @@ test('RnUnexpectedStandaloneDeriving', normal, compile_fail, [''])
 test('RnStupidThetaInGadt', normal, compile_fail, [''])
 test('PackageImportsDisabled', normal, compile_fail, [''])
 test('ImportLookupIllegal', normal, compile_fail, [''])
+test('RnNoImplicitForAll', normal, compile_fail, [''])
+test('WPatternSigBinds', normal, compile_fail, [''])
diff --git a/testsuite/tests/showIface/DocsInHiFile1.stdout b/testsuite/tests/showIface/DocsInHiFile1.stdout
index b74854d941..d46dfa240b 100644
--- a/testsuite/tests/showIface/DocsInHiFile1.stdout
+++ b/testsuite/tests/showIface/DocsInHiFile1.stdout
@@ -144,5 +144,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/DocsInHiFileTH.stdout b/testsuite/tests/showIface/DocsInHiFileTH.stdout
index 57ec74c37d..1179d04ae8 100644
--- a/testsuite/tests/showIface/DocsInHiFileTH.stdout
+++ b/testsuite/tests/showIface/DocsInHiFileTH.stdout
@@ -287,5 +287,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/HaddockIssue849.stdout b/testsuite/tests/showIface/HaddockIssue849.stdout
index 3bd32adbcc..a4f7dc5278 100644
--- a/testsuite/tests/showIface/HaddockIssue849.stdout
+++ b/testsuite/tests/showIface/HaddockIssue849.stdout
@@ -67,5 +67,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/HaddockOpts.stdout b/testsuite/tests/showIface/HaddockOpts.stdout
index 8af1142afe..3feab090c5 100644
--- a/testsuite/tests/showIface/HaddockOpts.stdout
+++ b/testsuite/tests/showIface/HaddockOpts.stdout
@@ -59,5 +59,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/LanguageExts.stdout b/testsuite/tests/showIface/LanguageExts.stdout
index 1e0a2a89be..6fafc2a6f7 100644
--- a/testsuite/tests/showIface/LanguageExts.stdout
+++ b/testsuite/tests/showIface/LanguageExts.stdout
@@ -22,5 +22,6 @@ docs:
          StarIsType
          CUSKs
          FieldSelectors
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/MagicHashInHaddocks.stdout b/testsuite/tests/showIface/MagicHashInHaddocks.stdout
index 2eb7eee959..d7450bff6b 100644
--- a/testsuite/tests/showIface/MagicHashInHaddocks.stdout
+++ b/testsuite/tests/showIface/MagicHashInHaddocks.stdout
@@ -69,5 +69,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/NoExportList.stdout b/testsuite/tests/showIface/NoExportList.stdout
index 669774d8e4..5d7e7bd6b1 100644
--- a/testsuite/tests/showIface/NoExportList.stdout
+++ b/testsuite/tests/showIface/NoExportList.stdout
@@ -95,5 +95,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/PragmaDocs.stdout b/testsuite/tests/showIface/PragmaDocs.stdout
index b2a9c929c6..0eff820a69 100644
--- a/testsuite/tests/showIface/PragmaDocs.stdout
+++ b/testsuite/tests/showIface/PragmaDocs.stdout
@@ -69,5 +69,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/showIface/ReExports.stdout b/testsuite/tests/showIface/ReExports.stdout
index f0c1ab2c9f..f695a8da2d 100644
--- a/testsuite/tests/showIface/ReExports.stdout
+++ b/testsuite/tests/showIface/ReExports.stdout
@@ -66,5 +66,9 @@ docs:
          StandaloneKindSignatures
          FieldSelectors
          TypeAbstractions
+         PatternSignatures
+         ExtendedForAllScope
+         MethodTypeVariables
+         ImplicitForAll
 extensible fields:
 
diff --git a/testsuite/tests/typecheck/should_fail/PatSynExistential.stderr b/testsuite/tests/typecheck/should_fail/PatSynExistential.stderr
index 326974dc55..fe75d0bc24 100644
--- a/testsuite/tests/typecheck/should_fail/PatSynExistential.stderr
+++ b/testsuite/tests/typecheck/should_fail/PatSynExistential.stderr
@@ -1,4 +1,5 @@
-PatSynExistential.hs:6:1: [GHC-33973]
-     The result type of the signature for ‘P’, namely ‘x -> Maybe x’
+
+PatSynExistential.hs:6:1: error: [GHC-33973]
+    • The result type of the signature for ‘P’, namely ‘x -> Maybe x’
         mentions existential type variable ‘x’
-     In the declaration for pattern synonym ‘P’
+    • In the declaration for pattern synonym ‘P’