Factor out HsPatSigType for pat sigs/RULE term sigs (#16762)

This implements chunks (2) and (3) of
https://gitlab.haskell.org/ghc/ghc/issues/16762#note_270170. Namely,
it introduces a dedicated `HsPatSigType` AST type, which represents
the types that can appear in pattern signatures and term-level `RULE`
binders. Previously, these were represented with `LHsSigWcType`.
Although `LHsSigWcType` is isomorphic to `HsPatSigType`, the intended
semantics of the two types are slightly different, as evidenced by
the fact that they have different code paths in the renamer and
typechecker.

See also the new `Note [Pattern signature binders and scoping]` in
`GHC.Hs.Types`.

17 files changed, 243 insertions, 109 deletions

diff --git a/compiler/GHC/Hs/Decls.hs b/compiler/GHC/Hs/Decls.hs
index f0ffd06307..8044b37cc4 100644
--- a/compiler/GHC/Hs/Decls.hs
+++ b/compiler/GHC/Hs/Decls.hs
@@ -2244,7 +2244,7 @@ type LRuleBndr pass = Located (RuleBndr pass)
 -- | Rule Binder
 data RuleBndr pass
   = RuleBndr (XCRuleBndr pass)  (Located (IdP pass))
-  | RuleBndrSig (XRuleBndrSig pass) (Located (IdP pass)) (LHsSigWcType pass)
+  | RuleBndrSig (XRuleBndrSig pass) (Located (IdP pass)) (HsPatSigType pass)
   | XRuleBndr !(XXRuleBndr pass)
         -- ^
         --  - 'ApiAnnotation.AnnKeywordId' : 'ApiAnnotation.AnnOpen',
@@ -2256,7 +2256,7 @@ type instance XCRuleBndr    (GhcPass _) = NoExtField
 type instance XRuleBndrSig  (GhcPass _) = NoExtField
 type instance XXRuleBndr    (GhcPass _) = NoExtCon
 
-collectRuleBndrSigTys :: [RuleBndr pass] -> [LHsSigWcType pass]
+collectRuleBndrSigTys :: [RuleBndr pass] -> [HsPatSigType pass]
 collectRuleBndrSigTys bndrs = [ty | RuleBndrSig _ _ ty <- bndrs]
 
 pprFullRuleName :: Located (SourceText, RuleName) -> SDoc
diff --git a/compiler/GHC/Hs/Extension.hs b/compiler/GHC/Hs/Extension.hs
index 0de2ac35a6..02106ab060 100644
--- a/compiler/GHC/Hs/Extension.hs
+++ b/compiler/GHC/Hs/Extension.hs
@@ -685,6 +685,11 @@ type family XXHsWildCardBndrs  x b
 
 -- -------------------------------------
 
+type family XHsPS x
+type family XXHsPatSigType x
+
+-- -------------------------------------
+
 type family XForAllTy        x
 type family XQualTy          x
 type family XTyVar           x
diff --git a/compiler/GHC/Hs/Instances.hs b/compiler/GHC/Hs/Instances.hs
index 6eca193bb8..f30e07a50e 100644
--- a/compiler/GHC/Hs/Instances.hs
+++ b/compiler/GHC/Hs/Instances.hs
@@ -386,6 +386,11 @@ deriving instance (Data thing) => Data (HsWildCardBndrs GhcPs thing)
 deriving instance (Data thing) => Data (HsWildCardBndrs GhcRn thing)
 deriving instance (Data thing) => Data (HsWildCardBndrs GhcTc thing)
 
+-- deriving instance (DataIdLR p p) => Data (HsPatSigType p)
+deriving instance Data (HsPatSigType GhcPs)
+deriving instance Data (HsPatSigType GhcRn)
+deriving instance Data (HsPatSigType GhcTc)
+
 -- deriving instance (DataIdLR p p) => Data (HsTyVarBndr p)
 deriving instance Data (HsTyVarBndr GhcPs)
 deriving instance Data (HsTyVarBndr GhcRn)
diff --git a/compiler/GHC/Hs/Pat.hs b/compiler/GHC/Hs/Pat.hs
index 50d3cf4aef..7b279ef3e1 100644
--- a/compiler/GHC/Hs/Pat.hs
+++ b/compiler/GHC/Hs/Pat.hs
@@ -240,7 +240,7 @@ data Pat p
   -- For details on above see note [Api annotations] in GHC.Parser.Annotation
   | SigPat          (XSigPat p)             -- After typechecker: Type
                     (LPat p)                -- Pattern with a type signature
-                    (LHsSigWcType (NoGhcTc p)) --  Signature can bind both
+                    (HsPatSigType (NoGhcTc p)) --  Signature can bind both
                                                --  kind and type vars
 
     -- ^ Pattern with a type signature
diff --git a/compiler/GHC/Hs/Types.hs b/compiler/GHC/Hs/Types.hs
index fd782c6348..f7a595d0f0 100644
--- a/compiler/GHC/Hs/Types.hs
+++ b/compiler/GHC/Hs/Types.hs
@@ -23,6 +23,7 @@ module GHC.Hs.Types (
         LHsQTyVars(..),
         HsImplicitBndrs(..),
         HsWildCardBndrs(..),
+        HsPatSigType(..), HsPSRn(..),
         LHsSigType, LHsSigWcType, LHsWcType,
         HsTupleSort(..),
         HsContext, LHsContext, noLHsContext,
@@ -47,7 +48,7 @@ module GHC.Hs.Types (
 
         mkAnonWildCardTy, pprAnonWildCard,
 
-        mkHsImplicitBndrs, mkHsWildCardBndrs, hsImplicitBody,
+        mkHsImplicitBndrs, mkHsWildCardBndrs, mkHsPatSigType, hsImplicitBody,
         mkEmptyImplicitBndrs, mkEmptyWildCardBndrs,
         mkHsQTvs, hsQTvExplicit, emptyLHsQTvs, isEmptyLHsQTvs,
         isHsKindedTyVar, hsTvbAllKinded, isLHsForAllTy,
@@ -59,7 +60,7 @@ module GHC.Hs.Types (
         splitLHsForAllTyInvis, splitLHsQualTy, splitLHsSigmaTyInvis,
         splitHsFunType, hsTyGetAppHead_maybe,
         mkHsOpTy, mkHsAppTy, mkHsAppTys, mkHsAppKindTy,
-        ignoreParens, hsSigType, hsSigWcType,
+        ignoreParens, hsSigType, hsSigWcType, hsPatSigType,
         hsLTyVarBndrToType, hsLTyVarBndrsToTypes,
         hsTyKindSig,
         hsConDetailsArgs,
@@ -184,6 +185,13 @@ is a bit complicated.  Here's how it works.
      f :: _a -> _
   The enclosing HsWildCardBndrs binds the wildcards _a and _.
 
+* HsSigPatType describes types that appear in pattern signatures and
+  the signatures of term-level binders in RULES. Like
+  HsWildCardBndrs/HsImplicitBndrs, they track the names of wildcard
+  variables and implicitly bound type variables. Unlike
+  HsImplicitBndrs, however, HsSigPatTypes do not obey the
+  forall-or-nothing rule. See Note [Pattern signature binders and scoping].
+
 * The explicit presence of these wrappers specifies, in the HsSyn,
   exactly where implicit quantification is allowed, and where
   wildcards are allowed.
@@ -225,13 +233,15 @@ Note carefully:
   Here _a is an ordinary forall'd binder, but (With NamedWildCards)
   _b is a named wildcard.  (See the comments in #10982)
 
-* Named wildcards are bound by the HsWildCardBndrs construct, which wraps
-  types that are allowed to have wildcards. Unnamed wildcards however are left
-  unchanged until typechecking, where we give them fresh wild tyavrs and
-  determine whether or not to emit hole constraints on each wildcard
-  (we don't if it's a visible type/kind argument or a type family pattern).
-  See related notes Note [Wildcards in visible kind application]
-  and Note [Wildcards in visible type application] in GHC.Tc.Gen.HsType
+* Named wildcards are bound by the HsWildCardBndrs (for types that obey the
+  forall-or-nothing rule) and HsPatSigType (for type signatures in patterns
+  and term-level binders in RULES), which wrap types that are allowed to have
+  wildcards. Unnamed wildcards, however are left unchanged until typechecking,
+  where we give them fresh wild tyvars and determine whether or not to emit
+  hole constraints on each wildcard (we don't if it's a visible type/kind
+  argument or a type family pattern). See related notes
+  Note [Wildcards in visible kind application] and
+  Note [Wildcards in visible type application] in GHC.Tc.Gen.HsType.
 
 * After type checking is done, we report what types the wildcards
   got unified with.
@@ -399,6 +409,33 @@ type instance XHsWC              GhcTc b = [Name]
 
 type instance XXHsWildCardBndrs  (GhcPass _) b = NoExtCon
 
+-- | Types that can appear in pattern signatures, as well as the signatures for
+-- term-level binders in RULES.
+-- See @Note [Pattern signature binders and scoping]@.
+--
+-- This is very similar to 'HsSigWcType', but with
+-- slightly different semantics: see @Note [HsType binders]@.
+-- See also @Note [The wildcard story for types]@.
+data HsPatSigType pass
+  = HsPS { hsps_ext  :: XHsPS pass   -- ^ After renamer: 'HsPSRn'
+         , hsps_body :: LHsType pass -- ^ Main payload (the type itself)
+    }
+  | XHsPatSigType !(XXHsPatSigType pass)
+
+-- | The extension field for 'HsPatSigType', which is only used in the
+-- renamer onwards. See @Note [Pattern signature binders and scoping]@.
+data HsPSRn = HsPSRn
+  { hsps_nwcs    :: [Name] -- ^ Wildcard names
+  , hsps_imp_tvs :: [Name] -- ^ Implicitly bound variable names
+  }
+  deriving Data
+
+type instance XHsPS GhcPs = NoExtField
+type instance XHsPS GhcRn = HsPSRn
+type instance XHsPS GhcTc = HsPSRn
+
+type instance XXHsPatSigType (GhcPass _) = NoExtCon
+
 -- | Located Haskell Signature Type
 type LHsSigType   pass = HsImplicitBndrs pass (LHsType pass)    -- Implicit only
 
@@ -419,6 +456,9 @@ hsSigType = hsImplicitBody
 hsSigWcType :: LHsSigWcType pass -> LHsType pass
 hsSigWcType sig_ty = hsib_body (hswc_body sig_ty)
 
+hsPatSigType :: HsPatSigType pass -> LHsType pass
+hsPatSigType = hsps_body
+
 dropWildCards :: LHsSigWcType pass -> LHsSigType pass
 -- Drop the wildcard part of a LHsSigWcType
 dropWildCards sig_ty = hswc_body sig_ty
@@ -441,6 +481,71 @@ we get
                                  , hst_body = blah }
 The implicit kind variable 'k' is bound by the HsIB;
 the explicitly forall'd tyvar 'a' is bound by the HsForAllTy
+
+Note [Pattern signature binders and scoping]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider the pattern signatures like those on `t` and `g` in:
+
+   f = let h = \(t :: (b, b) ->
+               \(g :: forall a. a -> b) ->
+               ...(t :: (Int,Int))...
+       in woggle
+
+* The `b` in t's pattern signature is implicitly bound and scopes over
+  the signature and the body of the lambda.  It stands for a type (any type);
+  indeed we subsequently discover that b=Int.
+  (See Note [TyVarTv] in GHC.Tc.Utils.TcMType for more on this point.)
+* The `b` in g's pattern signature is an /occurrence/ of the `b` bound by
+  t's pattern signature.
+* The `a` in `forall a` scopes only over the type `a -> b`, not over the body
+  of the lambda.
+* There is no forall-or-nothing rule for pattern signatures, which is why the
+  type `forall a. a -> b` is permitted in `g`'s pattern signature, even though
+  `b` is not explicitly bound.
+  See Note [forall-or-nothing rule] in GHC.Rename.HsType.
+
+Similar scoping rules apply to term variable binders in RULES, like in the
+following example:
+
+   {-# RULES "h" forall (t :: (b, b)) (g :: forall a. a -> b). h t g = ... #-}
+
+Just like in pattern signatures, the `b` in t's signature is implicitly bound
+and scopes over the remainder of the RULE. As a result, the `b` in g's
+signature is an occurrence. Moreover, the `a` in `forall a` scopes only over
+the type `a -> b`, and the forall-or-nothing rule does not apply.
+
+While quite similar, RULE term binder signatures behave slightly differently
+from pattern signatures in two ways:
+
+1. Unlike in pattern signatures, where type variables can stand for any type,
+   type variables in RULE term binder signatures are skolems.
+   See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType for
+   more on this point.
+
+   In this sense, type variables in pattern signatures are quite similar to
+   named wildcards, as both can refer to arbitrary types. The main difference
+   lies in error reporting: if a named wildcard `_a` in a pattern signature
+   stands for Int, then by default GHC will emit a warning stating as much.
+   Changing `_a` to `a`, on the other hand, will cause it not to be reported.
+2. In the `h` RULE above, only term variables are explicitly bound, so any free
+   type variables in the term variables' signatures are implicitly bound.
+   This is just like how the free type variables in pattern signatures are
+   implicitly bound. If a RULE explicitly binds both term and type variables,
+   however, then free type variables in term signatures are /not/ implicitly
+   bound. For example, this RULE would be ill scoped:
+
+     {-# RULES "h2" forall b. forall (t :: (b, c)) (g :: forall a. a -> b).
+                    h2 t g = ... #-}
+
+   This is because `b` and `c` occur free in the signature for `t`, but only
+   `b` was explicitly bound, leaving `c` out of scope. If the RULE had started
+   with `forall b c.`, then it would have been accepted.
+
+The types in pattern signatures and RULE term binder signatures are represented
+in the AST by HsSigPatType. From the renamer onward, the hsps_ext field (of
+type HsPSRn) tracks the names of named wildcards and implicitly bound type
+variables so that they can be brought into scope during renaming and
+typechecking.
 -}
 
 mkHsImplicitBndrs :: thing -> HsImplicitBndrs GhcPs thing
@@ -451,6 +556,10 @@ mkHsWildCardBndrs :: thing -> HsWildCardBndrs GhcPs thing
 mkHsWildCardBndrs x = HsWC { hswc_body = x
                            , hswc_ext  = noExtField }
 
+mkHsPatSigType :: LHsType GhcPs -> HsPatSigType GhcPs
+mkHsPatSigType x = HsPS { hsps_ext  = noExtField
+                        , hsps_body = x }
+
 -- Add empty binders.  This is a bit suspicious; what if
 -- the wrapped thing had free type variables?
 mkEmptyImplicitBndrs :: thing -> HsImplicitBndrs GhcRn thing
@@ -1408,6 +1517,10 @@ instance Outputable thing
        => Outputable (HsWildCardBndrs (GhcPass p) thing) where
     ppr (HsWC { hswc_body = ty }) = ppr ty
 
+instance OutputableBndrId p
+       => Outputable (HsPatSigType (GhcPass p)) where
+    ppr (HsPS { hsps_body = ty }) = ppr ty
+
 pprAnonWildCard :: SDoc
 pprAnonWildCard = char '_'
 
diff --git a/compiler/GHC/HsToCore/Quote.hs b/compiler/GHC/HsToCore/Quote.hs
index 166127f9d1..395f1adfb0 100644
--- a/compiler/GHC/HsToCore/Quote.hs
+++ b/compiler/GHC/HsToCore/Quote.hs
@@ -821,7 +821,7 @@ repRuleD (L loc (HsRule { rd_name = n
 ruleBndrNames :: LRuleBndr GhcRn -> [Name]
 ruleBndrNames (L _ (RuleBndr _ n))      = [unLoc n]
 ruleBndrNames (L _ (RuleBndrSig _ n sig))
-  | HsWC { hswc_body = HsIB { hsib_ext = vars }} <- sig
+  | HsPS { hsps_ext = HsPSRn { hsps_imp_tvs = vars }} <- sig
   = unLoc n : vars
 
 repRuleBndr :: LRuleBndr GhcRn -> MetaM (Core (M TH.RuleBndr))
@@ -830,7 +830,7 @@ repRuleBndr (L _ (RuleBndr _ n))
        ; rep2 ruleVarName [n'] }
 repRuleBndr (L _ (RuleBndrSig _ n sig))
   = do { MkC n'  <- lookupLBinder n
-       ; MkC ty' <- repLTy (hsSigWcType sig)
+       ; MkC ty' <- repLTy (hsPatSigType sig)
        ; rep2 typedRuleVarName [n', ty'] }
 
 repAnnD :: LAnnDecl GhcRn -> MetaM (SrcSpan, Core (M TH.Dec))
@@ -1935,7 +1935,7 @@ repP (NPat _ (L _ l) Nothing _) = do { a <- repOverloadedLiteral l
 repP (ViewPat _ e p) = do { e' <- repLE e; p' <- repLP p; repPview e' p' }
 repP p@(NPat _ _ (Just _) _) = notHandled "Negative overloaded patterns" (ppr p)
 repP (SigPat _ p t) = do { p' <- repLP p
-                         ; t' <- repLTy (hsSigWcType t)
+                         ; t' <- repLTy (hsPatSigType t)
                          ; repPsig p' t' }
 repP (SplicePat _ splice) = repSplice splice
 repP other = notHandled "Exotic pattern" (ppr other)
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index ddb29ce63d..6b469160e2 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -413,35 +413,9 @@ bar (x :: forall a. a -> a) = ... -- a is not in scope here
 --   ^ a is in scope here (pattern body)
 
 bax (x :: a) = ... -- a is in scope here
-Because of HsWC and HsIB pass on their scope to their children
-we must wrap the LHsType in pattern signatures in a
-Shielded explicitly, so that the HsWC/HsIB scope is not passed
-on the the LHsType
--}
-
-data Shielded a = SH Scope a -- Ignores its TScope, uses its own scope instead
-
-type family ProtectedSig a where
-  ProtectedSig GhcRn = HsWildCardBndrs GhcRn (HsImplicitBndrs
-                                                GhcRn
-                                                (Shielded (LHsType GhcRn)))
-  ProtectedSig GhcTc = NoExtField
-
-class ProtectSig a where
-  protectSig :: Scope -> LHsSigWcType (NoGhcTc a) -> ProtectedSig a
-
-instance (HasLoc a) => HasLoc (Shielded a) where
-  loc (SH _ a) = loc a
-
-instance (ToHie (TScoped a)) => ToHie (TScoped (Shielded a)) where
-  toHie (TS _ (SH sc a)) = toHie (TS (ResolvedScopes [sc]) a)
 
-instance ProtectSig GhcTc where
-  protectSig _ _ = noExtField
-
-instance ProtectSig GhcRn where
-  protectSig sc (HsWC a (HsIB b sig)) =
-    HsWC a (HsIB b (SH sc sig))
+This case in handled in the instance for HsPatSigType
+-}
 
 class HasLoc a where
   -- ^ defined so that HsImplicitBndrs and HsWildCardBndrs can
@@ -770,8 +744,6 @@ instance ( a ~ GhcPass p
          , ToHie (RContext (HsRecFields a (PScoped (LPat a))))
          , ToHie (LHsExpr a)
          , ToHie (TScoped (LHsSigWcType a))
-         , ProtectSig a
-         , ToHie (TScoped (ProtectedSig a))
          , HasType (LPat a)
          , Data (HsSplice a)
          , IsPass p
@@ -832,9 +804,12 @@ instance ( a ~ GhcPass p
       SigPat _ pat sig ->
         [ toHie $ PS rsp scope pscope pat
         , let cscope = mkLScope pat in
-            toHie $ TS (ResolvedScopes [cscope, scope, pscope])
-                       (protectSig @a cscope sig)
-              -- See Note [Scoping Rules for SigPat]
+            case ghcPass @p of
+              GhcPs -> pure []
+              GhcTc -> pure []
+              GhcRn ->
+                toHie $ TS (ResolvedScopes [cscope, scope, pscope])
+                        sig
         ]
       XPat e -> case ghcPass @p of
 #if __GLASGOW_HASKELL__ < 811
@@ -856,6 +831,13 @@ instance ( a ~ GhcPass p
             L spn $ HsRecField lbl (PS rsp scope fscope pat) pun
           scoped_fds = listScopes pscope fds
 
+instance ToHie (TScoped (HsPatSigType GhcRn)) where
+  toHie (TS sc (HsPS (HsPSRn wcs tvs) body@(L span _))) = concatM $
+      [ pure $ bindingsOnly $ map (C $ TyVarBind (mkScope span) sc) (wcs++tvs)
+      , toHie body
+      ]
+  -- See Note [Scoping Rules for SigPat]
+
 instance ( ToHie body
          , ToHie (LGRHS a body)
          , ToHie (RScoped (LHsLocalBinds a))
diff --git a/compiler/GHC/Parser/PostProcess.hs b/compiler/GHC/Parser/PostProcess.hs
index 94137f07ba..b9bff61599 100644
--- a/compiler/GHC/Parser/PostProcess.hs
+++ b/compiler/GHC/Parser/PostProcess.hs
@@ -874,7 +874,7 @@ mkRuleBndrs :: [LRuleTyTmVar] -> [LRuleBndr GhcPs]
 mkRuleBndrs = fmap (fmap cvt_one)
   where cvt_one (RuleTyTmVar v Nothing)    = RuleBndr    noExtField v
         cvt_one (RuleTyTmVar v (Just sig)) =
-          RuleBndrSig noExtField v (mkLHsSigWcType sig)
+          RuleBndrSig noExtField v (mkHsPatSigType sig)
 
 -- turns RuleTyTmVars into HsTyVarBndrs - this is more interesting
 mkRuleTyVarBndrs :: [LRuleTyTmVar] -> [LHsTyVarBndr GhcPs]
@@ -2033,7 +2033,7 @@ instance DisambECP (PatBuilder GhcPs) where
   mkHsWildCardPV l = return $ L l (PatBuilderPat (WildPat noExtField))
   mkHsTySigPV l b sig = do
     p <- checkLPat b
-    return $ L l (PatBuilderPat (SigPat noExtField p (mkLHsSigWcType sig)))
+    return $ L l (PatBuilderPat (SigPat noExtField p (mkHsPatSigType sig)))
   mkHsExplicitListPV l xs = do
     ps <- traverse checkLPat xs
     return (L l (PatBuilderPat (ListPat noExtField ps)))
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index fe7fb78b08..a2566220b6 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -955,7 +955,7 @@ renameSig _ (IdSig _ x)
 renameSig ctxt sig@(TypeSig _ vs ty)
   = do  { new_vs <- mapM (lookupSigOccRn ctxt sig) vs
         ; let doc = TypeSigCtx (ppr_sig_bndrs vs)
-        ; (new_ty, fvs) <- rnHsSigWcType BindUnlessForall doc ty
+        ; (new_ty, fvs) <- rnHsSigWcType doc ty
         ; return (TypeSig noExtField new_vs new_ty, fvs) }
 
 renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 6ec473134d..65d119ab12 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -316,7 +316,7 @@ rnExpr (RecordUpd { rupd_expr = expr, rupd_flds = rbinds })
                  , fvExpr `plusFV` fvRbinds) }
 
 rnExpr (ExprWithTySig _ expr pty)
-  = do  { (pty', fvTy)    <- rnHsSigWcType BindUnlessForall ExprWithTySigCtx pty
+  = do  { (pty', fvTy)    <- rnHsSigWcType ExprWithTySigCtx pty
         ; (expr', fvExpr) <- bindSigTyVarsFV (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 537b2a47f0..f3727221a0 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -13,7 +13,7 @@ module GHC.Rename.HsType (
         rnHsType, rnLHsType, rnLHsTypes, rnContext,
         rnHsKind, rnLHsKind, rnLHsTypeArgs,
         rnHsSigType, rnHsWcType,
-        HsSigWcTypeScoping(..), rnHsSigWcType, rnHsSigWcTypeScoped,
+        HsSigWcTypeScoping(..), rnHsSigWcType, rnHsPatSigType,
         newTyVarNameRn,
         rnConDeclFields,
         rnLTyVar,
@@ -71,11 +71,11 @@ import Control.Monad      ( unless, when )
 
 {-
 These type renamers are in a separate module, rather than in (say) GHC.Rename.Module,
-to break several loop.
+to break several loops.
 
 *********************************************************
 *                                                       *
-           HsSigWcType (i.e with wildcards)
+    HsSigWcType and HsPatSigType (i.e with wildcards)
 *                                                       *
 *********************************************************
 -}
@@ -85,46 +85,77 @@ data HsSigWcTypeScoping
     -- ^ Always bind any free tyvars of the given type, regardless of whether we
     -- have a forall at the top.
     --
-    -- For pattern type sigs and rules we /do/ want to bring those type
+    -- For pattern type sigs, we /do/ want to bring those type
     -- variables into scope, even if there's a forall at the top which usually
     -- stops that happening, e.g:
     --
-    -- > \ (x :: forall a. a-> b) -> e
+    -- > \ (x :: forall a. a -> b) -> e
     --
     -- Here we do bring 'b' into scope.
+    --
+    -- RULES can also use 'AlwaysBind', such as in the following example:
+    --
+    -- > {-# RULES \"f\" forall (x :: forall a. a -> b). f x = ... b ... #-}
+    --
+    -- This only applies to RULES that do not explicitly bind their type
+    -- variables. If a RULE explicitly quantifies its type variables, then
+    -- 'NeverBind' is used instead. See also
+    -- @Note [Pattern signature binders and scoping]@ in "GHC.Hs.Types".
   | BindUnlessForall
-    -- ^ Unless there's forall at the top, do the same thing as 'AlwaysBind'
+    -- ^ Unless there's forall at the top, do the same thing as 'AlwaysBind'.
+    -- This is only ever used in places where the \"@forall@-or-nothing\" rule
+    -- is in effect. See @Note [forall-or-nothing rule]@.
   | NeverBind
-    -- ^ Never bind any free tyvars
-
-rnHsSigWcType :: HsSigWcTypeScoping -> HsDocContext -> LHsSigWcType GhcPs
+    -- ^ Never bind any free tyvars. This is used for RULES that have both
+    -- explicit type and term variable binders, e.g.:
+    --
+    -- > {-# RULES \"const\" forall a. forall (x :: a) y. const x y = x #-}
+    --
+    -- The presence of the type variable binder @forall a.@ implies that the
+    -- free variables in the types of the term variable binders @x@ and @y@
+    -- are /not/ bound. In the example above, there are no such free variables,
+    -- but if the user had written @(y :: b)@ instead of @y@ in the term
+    -- variable binders, then @b@ would be rejected for being out of scope.
+    -- See also @Note [Pattern signature binders and scoping]@ in
+    -- "GHC.Hs.Types".
+
+rnHsSigWcType :: HsDocContext -> LHsSigWcType GhcPs
               -> RnM (LHsSigWcType GhcRn, FreeVars)
-rnHsSigWcType scoping doc sig_ty
-  = rn_hs_sig_wc_type scoping doc sig_ty $ \sig_ty' ->
-    return (sig_ty', emptyFVs)
-
-rnHsSigWcTypeScoped :: HsSigWcTypeScoping
-                    -> HsDocContext -> LHsSigWcType GhcPs
-                    -> (LHsSigWcType GhcRn -> RnM (a, FreeVars))
-                    -> RnM (a, FreeVars)
+rnHsSigWcType doc (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
+  = rn_hs_sig_wc_type BindUnlessForall doc hs_ty $ \nwcs imp_tvs body ->
+    let ib_ty = HsIB { hsib_ext = imp_tvs, hsib_body = body  }
+        wc_ty = HsWC { hswc_ext = nwcs,    hswc_body = ib_ty } in
+    pure (wc_ty, emptyFVs)
+
+rnHsPatSigType :: HsSigWcTypeScoping
+               -> HsDocContext -> HsPatSigType GhcPs
+               -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
+               -> RnM (a, FreeVars)
 -- Used for
---   - Signatures on binders in a RULE
---   - Pattern type signatures
+--   - Pattern type signatures, which are only allowed with ScopedTypeVariables
+--   - Signatures on binders in a RULE, which are allowed even if
+--     ScopedTypeVariables isn't enabled
 -- Wildcards are allowed
--- type signatures on binders only allowed with ScopedTypeVariables
-rnHsSigWcTypeScoped scoping ctx sig_ty thing_inside
+--
+-- See Note [Pattern signature binders and scoping] in GHC.Hs.Types
+rnHsPatSigType scoping ctx sig_ty thing_inside
   = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
-       ; checkErr ty_sig_okay (unexpectedTypeSigErr sig_ty)
-       ; rn_hs_sig_wc_type scoping ctx sig_ty thing_inside
-       }
-
-rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext -> LHsSigWcType GhcPs
-                  -> (LHsSigWcType GhcRn -> RnM (a, FreeVars))
+       ; checkErr ty_sig_okay (unexpectedPatSigTypeErr sig_ty)
+       ; rn_hs_sig_wc_type scoping ctx (hsPatSigType sig_ty) $
+         \nwcs imp_tvs body ->
+    do { let sig_names = HsPSRn { hsps_nwcs = nwcs, hsps_imp_tvs = imp_tvs }
+             sig_ty'   = HsPS { hsps_ext = sig_names, hsps_body = body }
+       ; thing_inside sig_ty'
+       } }
+
+-- The workhorse for rnHsSigWcType and rnHsPatSigType.
+rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext -> LHsType GhcPs
+                  -> ([Name]    -- Wildcard names
+                      -> [Name] -- Implicitly bound type variable names
+                      -> LHsType GhcRn
+                      -> RnM (a, FreeVars))
                   -> RnM (a, FreeVars)
--- rn_hs_sig_wc_type is used for source-language type signatures
-rn_hs_sig_wc_type scoping ctxt
-                  (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
-                  thing_inside
+rn_hs_sig_wc_type scoping ctxt hs_ty thing_inside
   = do { free_vars <- extractFilteredRdrTyVarsDups hs_ty
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
@@ -134,10 +165,7 @@ rn_hs_sig_wc_type scoping ctxt
                NeverBind        -> []
        ; rnImplicitBndrs implicit_bndrs $ \ vars ->
     do { (wcs, hs_ty', fvs1) <- rnWcBody ctxt nwc_rdrs hs_ty
-       ; let sig_ty' = HsWC { hswc_ext = wcs, hswc_body = ib_ty' }
-             ib_ty'  = HsIB { hsib_ext = vars
-                            , hsib_body = hs_ty' }
-       ; (res, fvs2) <- thing_inside sig_ty'
+       ; (res, fvs2) <- thing_inside wcs vars hs_ty'
        ; return (res, fvs1 `plusFV` fvs2) } }
 
 rnHsWcType :: HsDocContext -> LHsWcType GhcPs -> RnM (LHsWcType GhcRn, FreeVars)
@@ -321,8 +349,9 @@ rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
 -- therefore an indication that the user is trying to be fastidious, so
 -- we don't implicitly bind any variables.
 
--- | See note Note [forall-or-nothing rule]. This tiny little function is used
--- (rather than its small body inlined) to indicate we implementing that rule.
+-- | See Note [forall-or-nothing rule]. This tiny little function is used
+-- (rather than its small body inlined) to indicate that we are implementing
+-- that rule.
 forAllOrNothing :: Bool
                 -- ^ True <=> explicit forall
                 -- E.g.  f :: forall a. a->b
@@ -1396,8 +1425,8 @@ ppr_opfix (op, fixity) = pp_op <+> brackets (ppr fixity)
 *                                                      *
 ***************************************************** -}
 
-unexpectedTypeSigErr :: LHsSigWcType GhcPs -> SDoc
-unexpectedTypeSigErr ty
+unexpectedPatSigTypeErr :: HsPatSigType GhcPs -> SDoc
+unexpectedPatSigTypeErr ty
   = hang (text "Illegal type signature:" <+> quotes (ppr ty))
        2 (text "Type signatures are only allowed in patterns with ScopedTypeVariables")
 
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index a4ca8a5165..2a09849e52 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -957,7 +957,7 @@ rnSrcDerivDecl (DerivDecl _ ty mds overlap)
        ; unless standalone_deriv_ok (addErr standaloneDerivErr)
        ; (mds', ty', fvs)
            <- rnLDerivStrategy DerivDeclCtx mds $
-              rnHsSigWcType BindUnlessForall DerivDeclCtx ty
+              rnHsSigWcType DerivDeclCtx ty
        ; warnNoDerivStrat mds' loc
        ; return (DerivDecl noExtField ty' mds' overlap, fvs) }
   where
@@ -1028,7 +1028,7 @@ bindRuleTmVars doc tyvs vars names thing_inside
 
     go ((L l (RuleBndrSig _ (L loc _) bsig)) : vars)
        (n : ns) thing_inside
-      = rnHsSigWcTypeScoped bind_free_tvs doc bsig $ \ bsig' ->
+      = rnHsPatSigType bind_free_tvs doc bsig $ \ bsig' ->
         go vars ns $ \ vars' ->
         thing_inside (L l (RuleBndrSig noExtField (L loc n) bsig') : vars')
 
diff --git a/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 1e2bf09f45..09e2ea8cbe 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -218,9 +218,6 @@ matchNameMaker ctxt = LamMk report_unused
                       ThPatQuote            -> False
                       _                     -> True
 
-rnHsSigCps :: LHsSigWcType GhcPs -> CpsRn (LHsSigWcType GhcRn)
-rnHsSigCps sig = CpsRn (rnHsSigWcTypeScoped AlwaysBind PatCtx sig)
-
 newPatLName :: NameMaker -> Located RdrName -> CpsRn (Located Name)
 newPatLName name_maker rdr_name@(L loc _)
   = do { name <- newPatName name_maker rdr_name
@@ -410,9 +407,12 @@ rnPatAndThen mk (SigPat x pat sig)
   -- f ((Just (x :: a) :: Maybe a)
   -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~^       `a' is first bound here
   -- ~~~~~~~~~~~~~~~^                   the same `a' then used here
-  = do { sig' <- rnHsSigCps sig
+  = do { sig' <- rnHsPatSigTypeAndThen sig
        ; pat' <- rnLPatAndThen mk pat
        ; return (SigPat x pat' sig' ) }
+  where
+    rnHsPatSigTypeAndThen :: HsPatSigType GhcPs -> CpsRn (HsPatSigType GhcRn)
+    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx sig)
 
 rnPatAndThen mk (LitPat x lit)
   | HsString src s <- lit
diff --git a/compiler/GHC/Tc/Gen/HsType.hs b/compiler/GHC/Tc/Gen/HsType.hs
index 9342c367b3..cd48e5416f 100644
--- a/compiler/GHC/Tc/Gen/HsType.hs
+++ b/compiler/GHC/Tc/Gen/HsType.hs
@@ -3338,7 +3338,7 @@ Result works fine, but it may eventually bite us.
 ********************************************************************* -}
 
 tcHsPatSigType :: UserTypeCtxt
-               -> LHsSigWcType GhcRn          -- The type signature
+               -> HsPatSigType GhcRn          -- The type signature
                -> TcM ( [(Name, TcTyVar)]     -- Wildcards
                       , [(Name, TcTyVar)]     -- The new bit of type environment, binding
                                               -- the scoped type variables
@@ -3346,13 +3346,13 @@ tcHsPatSigType :: UserTypeCtxt
 -- Used for type-checking type signatures in
 -- (a) patterns           e.g  f (x::Int) = e
 -- (b) RULE forall bndrs  e.g. forall (x::Int). f x = x
+-- See Note [Pattern signature binders and scoping] in GHC.Hs.Types
 --
 -- This may emit constraints
 -- See Note [Recipe for checking a signature]
-tcHsPatSigType ctxt sig_ty
-  | HsWC { hswc_ext = sig_wcs,   hswc_body = ib_ty } <- sig_ty
-  , HsIB { hsib_ext = sig_ns
-         , hsib_body = hs_ty } <- ib_ty
+tcHsPatSigType ctxt
+  (HsPS { hsps_ext  = HsPSRn { hsps_nwcs = sig_wcs, hsps_imp_tvs = sig_ns }
+        , hsps_body = hs_ty })
   = addSigCtxt ctxt hs_ty $
     do { sig_tkv_prs <- mapM new_implicit_tv sig_ns
        ; (wcs, sig_ty)
@@ -3385,12 +3385,12 @@ tcHsPatSigType ctxt sig_ty
            ; tv   <- case ctxt of
                        RuleSigCtxt {} -> newSkolemTyVar name kind
                        _              -> newPatSigTyVar name kind
-                       -- See Note [Pattern signature binders]
+                       -- See Note [Typechecking pattern signature binders]
              -- NB: tv's Name may be fresh (in the case of newPatSigTyVar)
            ; return (name, tv) }
 
-{- Note [Pattern signature binders]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+{- Note [Typechecking pattern signature binders]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 See also Note [Type variables in the type environment] in GHC.Tc.Utils.
 Consider
 
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index 2f7d2e7721..bd9afd766f 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -690,7 +690,7 @@ because they won't be in scope when we do the desugaring
 -}
 
 tcPatSig :: Bool                    -- True <=> pattern binding
-         -> LHsSigWcType GhcRn
+         -> HsPatSigType GhcRn
          -> ExpSigmaType
          -> TcM (TcType,            -- The type to use for "inside" the signature
                  [(Name,TcTyVar)],  -- The new bit of type environment, binding
diff --git a/compiler/GHC/Tc/Gen/Rule.hs b/compiler/GHC/Tc/Gen/Rule.hs
index 708218abe5..3ed75ac49b 100644
--- a/compiler/GHC/Tc/Gen/Rule.hs
+++ b/compiler/GHC/Tc/Gen/Rule.hs
@@ -230,7 +230,7 @@ tcRuleTmBndrs (L _ (RuleBndrSig _ (L _ name) rn_ty) : rule_bndrs)
   = do  { let ctxt = RuleSigCtxt name
         ; (_ , tvs, id_ty) <- tcHsPatSigType ctxt rn_ty
         ; let id  = mkLocalId name id_ty
-                    -- See Note [Pattern signature binders] in GHC.Tc.Gen.HsType
+                    -- See Note [Typechecking pattern signature binders] in GHC.Tc.Gen.HsType
 
               -- The type variables scope over subsequent bindings; yuk
         ; (tyvars, tmvars) <- tcExtendNameTyVarEnv tvs $
diff --git a/compiler/GHC/ThToHs.hs b/compiler/GHC/ThToHs.hs
index b0d797885b..e1d1c97410 100644
--- a/compiler/GHC/ThToHs.hs
+++ b/compiler/GHC/ThToHs.hs
@@ -830,7 +830,7 @@ cvtRuleBndr (RuleVar n)
 cvtRuleBndr (TypedRuleVar n ty)
   = do { n'  <- vNameL n
        ; ty' <- cvtType ty
-       ; return $ noLoc $ Hs.RuleBndrSig noExtField n' $ mkLHsSigWcType ty' }
+       ; return $ noLoc $ Hs.RuleBndrSig noExtField n' $ mkHsPatSigType ty' }
 
 ---------------------------------------------------
 --              Declarations
@@ -1307,7 +1307,7 @@ cvtp (ListP ps)        = do { ps' <- cvtPats ps
                             ; return
                                    $ ListPat noExtField ps'}
 cvtp (SigP p t)        = do { p' <- cvtPat p; t' <- cvtType t
-                            ; return $ SigPat noExtField p' (mkLHsSigWcType t') }
+                            ; return $ SigPat noExtField p' (mkHsPatSigType t') }
 cvtp (ViewP e p)       = do { e' <- cvtl e; p' <- cvtPat p
                             ; return $ ViewPat noExtField e' p'}