Clean up the inferred type variable restriction

This patch primarily:

* Documents `checkInferredVars` (previously called
  `check_inferred_vars`) more carefully. This is the
  function which throws an error message if a user quantifies an
  inferred type variable in a place where specificity cannot be
  observed. See `Note [Unobservably inferred type variables]` in
  `GHC.Rename.HsType`.

  Note that I now invoke `checkInferredVars` _alongside_
  `rnHsSigType`, `rnHsWcSigType`, etc. rather than doing so _inside_
  of these functions. This results in slightly more call sites for
  `checkInferredVars`, but it makes it much easier to enumerate the
  spots where the inferred type variable restriction comes into
  effect.
* Removes the inferred type variable restriction for default method
  type signatures, per the discussion in #18432. As a result, this
  patch fixes #18432.

Along the way, I performed some various cleanup:

* I moved `no_nested_foralls_contexts_err` into `GHC.Rename.Utils`
  (under the new name `noNestedForallsContextsErr`), since it now
  needs to be invoked from multiple modules. I also added a helper
  function `addNoNestedForallsContextsErr` that throws the error
  message after producing it, as this is a common idiom.
* In order to ensure that users cannot sneak inferred type variables
  into `SPECIALISE instance` pragmas by way of nested `forall`s, I
  now invoke `addNoNestedForallsContextsErr` when renaming
  `SPECIALISE instance` pragmas, much like when we rename normal
  instance declarations. (This probably should have originally been
  done as a part of the fix for #18240, but this task was somehow
  overlooked.) As a result, this patch fixes #18455 as a side effect.

(cherry picked from commit 502605f7ae9907a6b0b9823e8f055ae390c57b1d)

14 files changed, 232 insertions, 128 deletions

diff --git a/compiler/GHC/Hs/Type.hs b/compiler/GHC/Hs/Type.hs
index 6ed5566054..5de051d047 100644
--- a/compiler/GHC/Hs/Type.hs
+++ b/compiler/GHC/Hs/Type.hs
@@ -1628,6 +1628,12 @@ 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.
 
+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.
+
 -----
 -- Wrinkle: Derived instances
 -----
diff --git a/compiler/GHC/Rename/Bind.hs b/compiler/GHC/Rename/Bind.hs
index bb4a3c1b76..da4213acee 100644
--- a/compiler/GHC/Rename/Bind.hs
+++ b/compiler/GHC/Rename/Bind.hs
@@ -43,7 +43,8 @@ import GHC.Rename.Fixity
 import GHC.Rename.Utils ( HsDocContext(..), mapFvRn, extendTyVarEnvFVRn
                         , checkDupRdrNames, warnUnusedLocalBinds
                         , checkUnusedRecordWildcard
-                        , checkDupAndShadowedNames, bindLocalNamesFV )
+                        , checkDupAndShadowedNames, bindLocalNamesFV
+                        , addNoNestedForallsContextsErr, checkInferredVars )
 import GHC.Driver.Session
 import GHC.Unit.Module
 import GHC.Types.Name
@@ -955,7 +956,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 doc Nothing ty
+        ; (new_ty, fvs) <- rnHsSigWcType doc ty
         ; return (TypeSig noExtField new_vs new_ty, fvs) }
 
 renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
@@ -963,20 +964,25 @@ renameSig ctxt sig@(ClassOpSig _ is_deflt vs ty)
         ; when (is_deflt && not defaultSigs_on) $
           addErr (defaultSigErr sig)
         ; new_v <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel inf_msg ty
+        ; (new_ty, fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (ClassOpSig noExtField is_deflt new_v new_ty, fvs) }
   where
     (v1:_) = vs
     ty_ctxt = GenericCtx (text "a class method signature for"
                           <+> quotes (ppr v1))
-    inf_msg = if is_deflt
-      then Just (text "A default type signature cannot contain inferred type variables")
-      else Nothing
 
 renameSig _ (SpecInstSig _ src ty)
-  = do  { (new_ty, fvs) <- rnHsSigType SpecInstSigCtx TypeLevel inf_msg ty
+  = do  { checkInferredVars doc inf_msg ty
+        ; (new_ty, fvs) <- rnHsSigType doc TypeLevel 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).
+        ; addNoNestedForallsContextsErr doc (text "SPECIALISE instance type")
+            (getLHsInstDeclHead new_ty)
         ; return (SpecInstSig noExtField src new_ty,fvs) }
   where
+    doc = SpecInstSigCtx
     inf_msg = Just (text "Inferred type variables are not allowed")
 
 -- {-# SPECIALISE #-} pragmas can refer to imported Ids
@@ -993,7 +999,7 @@ renameSig ctxt sig@(SpecSig _ v tys inl)
     ty_ctxt = GenericCtx (text "a SPECIALISE signature for"
                           <+> quotes (ppr v))
     do_one (tys,fvs) ty
-      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel Nothing ty
+      = do { (new_ty, fvs_ty) <- rnHsSigType ty_ctxt TypeLevel ty
            ; return ( new_ty:tys, fvs_ty `plusFV` fvs) }
 
 renameSig ctxt sig@(InlineSig _ v s)
@@ -1010,7 +1016,7 @@ renameSig ctxt sig@(MinimalSig _ s (L l bf))
 
 renameSig ctxt sig@(PatSynSig _ vs ty)
   = do  { new_vs <- mapM (lookupSigOccRn ctxt sig) vs
-        ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel Nothing ty
+        ; (ty', fvs) <- rnHsSigType ty_ctxt TypeLevel ty
         ; return (PatSynSig noExtField new_vs ty', fvs) }
   where
     ty_ctxt = GenericCtx (text "a pattern synonym signature for"
diff --git a/compiler/GHC/Rename/Expr.hs b/compiler/GHC/Rename/Expr.hs
index 6814752963..e91f6fa4ff 100644
--- a/compiler/GHC/Rename/Expr.hs
+++ b/compiler/GHC/Rename/Expr.hs
@@ -317,7 +317,7 @@ rnExpr (RecordUpd { rupd_expr = expr, rupd_flds = rbinds })
                  , fvExpr `plusFV` fvRbinds) }
 
 rnExpr (ExprWithTySig _ expr pty)
-  = do  { (pty', fvTy)    <- rnHsSigWcType ExprWithTySigCtx Nothing 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 0def086cb5..e7ba37c2b6 100644
--- a/compiler/GHC/Rename/HsType.hs
+++ b/compiler/GHC/Rename/HsType.hs
@@ -39,7 +39,6 @@ import GHC.Prelude
 
 import {-# SOURCE #-} GHC.Rename.Splice( rnSpliceType )
 
-import GHC.Core.Type
 import GHC.Driver.Session
 import GHC.Hs
 import GHC.Rename.Doc    ( rnLHsDoc, rnMbLHsDoc )
@@ -68,7 +67,7 @@ import GHC.Data.FastString
 import GHC.Data.Maybe
 import qualified GHC.LanguageExtensions as LangExt
 
-import Data.List          ( nubBy, partition, find )
+import Data.List          ( nubBy, partition )
 import Control.Monad      ( unless, when )
 
 #include "HsVersions.h"
@@ -124,19 +123,16 @@ data HsSigWcTypeScoping
     -- "GHC.Hs.Type".
 
 rnHsSigWcType :: HsDocContext
-              -> Maybe SDoc
-              -- ^ The error msg if the signature is not allowed to contain
-              --   manually written inferred variables.
               -> LHsSigWcType GhcPs
               -> RnM (LHsSigWcType GhcRn, FreeVars)
-rnHsSigWcType doc inf_err (HsWC { hswc_body = HsIB { hsib_body = hs_ty }})
-  = rn_hs_sig_wc_type BindUnlessForall doc inf_err hs_ty $ \nwcs imp_tvs body ->
+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 -> Maybe SDoc
+               -> HsDocContext
                -> HsPatSigType GhcPs
                -> (HsPatSigType GhcRn -> RnM (a, FreeVars))
                -> RnM (a, FreeVars)
@@ -147,10 +143,10 @@ rnHsPatSigType :: HsSigWcTypeScoping
 -- Wildcards are allowed
 --
 -- See Note [Pattern signature binders and scoping] in GHC.Hs.Type
-rnHsPatSigType scoping ctx inf_err sig_ty thing_inside
+rnHsPatSigType scoping ctx sig_ty thing_inside
   = do { ty_sig_okay <- xoptM LangExt.ScopedTypeVariables
        ; checkErr ty_sig_okay (unexpectedPatSigTypeErr sig_ty)
-       ; rn_hs_sig_wc_type scoping ctx inf_err (hsPatSigType 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 }
@@ -158,16 +154,15 @@ rnHsPatSigType scoping ctx inf_err sig_ty thing_inside
        } }
 
 -- The workhorse for rnHsSigWcType and rnHsPatSigType.
-rn_hs_sig_wc_type :: HsSigWcTypeScoping -> HsDocContext -> Maybe SDoc
+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 scoping ctxt inf_err hs_ty thing_inside
-  = do { check_inferred_vars ctxt inf_err hs_ty
-       ; free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
+rn_hs_sig_wc_type scoping ctxt hs_ty thing_inside
+  = do { free_vars <- filterInScopeM (extractHsTyRdrTyVars hs_ty)
        ; (nwc_rdrs', tv_rdrs) <- partition_nwcs free_vars
        ; let nwc_rdrs = nubL nwc_rdrs'
        ; implicit_bndrs <- case scoping of
@@ -318,17 +313,13 @@ of the HsWildCardBndrs structure, and we are done.
 
 rnHsSigType :: HsDocContext
             -> TypeOrKind
-            -> Maybe SDoc
-            -- ^ The error msg if the signature is not allowed to contain
-            --   manually written inferred variables.
             -> LHsSigType GhcPs
             -> RnM (LHsSigType GhcRn, FreeVars)
 -- Used for source-language type signatures
 -- that cannot have wildcards
-rnHsSigType ctx level inf_err (HsIB { hsib_body = hs_ty })
+rnHsSigType ctx level (HsIB { hsib_body = hs_ty })
   = do { traceRn "rnHsSigType" (ppr hs_ty)
        ; rdr_env <- getLocalRdrEnv
-       ; check_inferred_vars ctx inf_err hs_ty
        ; vars0 <- forAllOrNothing (isLHsForAllTy hs_ty)
            $ filterInScope rdr_env
            $ extractHsTyRdrTyVars hs_ty
@@ -415,26 +406,6 @@ type signature, since the type signature implicitly carries their binding
 sites. This is less precise, but more accurate.
 -}
 
-check_inferred_vars :: HsDocContext
-                    -> Maybe SDoc
-                    -- ^ The error msg if the signature is not allowed to contain
-                    --   manually written inferred variables.
-                    -> LHsType GhcPs
-                    -> RnM ()
-check_inferred_vars _    Nothing    _  = return ()
-check_inferred_vars ctxt (Just msg) ty =
-  let bndrs = forallty_bndrs ty
-  in case find ((==) InferredSpec . hsTyVarBndrFlag) bndrs of
-    Nothing -> return ()
-    Just _  -> addErr $ withHsDocContext ctxt msg
-  where
-    forallty_bndrs :: LHsType GhcPs -> [HsTyVarBndr Specificity GhcPs]
-    forallty_bndrs (L _ ty) = case ty of
-      HsParTy _ ty' -> forallty_bndrs ty'
-      HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}
-                    -> map unLoc tvs
-      _             -> []
-
 {- ******************************************************
 *                                                       *
            LHsType and HsType
diff --git a/compiler/GHC/Rename/Module.hs b/compiler/GHC/Rename/Module.hs
index f41a000e80..4cdae93a7f 100644
--- a/compiler/GHC/Rename/Module.hs
+++ b/compiler/GHC/Rename/Module.hs
@@ -34,7 +34,8 @@ import GHC.Rename.Utils ( HsDocContext(..), mapFvRn, bindLocalNames
                         , checkDupRdrNames, bindLocalNamesFV
                         , checkShadowedRdrNames, warnUnusedTypePatterns
                         , extendTyVarEnvFVRn, newLocalBndrsRn
-                        , withHsDocContext )
+                        , withHsDocContext, noNestedForallsContextsErr
+                        , addNoNestedForallsContextsErr, checkInferredVars )
 import GHC.Rename.Unbound ( mkUnboundName, notInScopeErr )
 import GHC.Rename.Names
 import GHC.Rename.Doc   ( rnHsDoc, rnMbLHsDoc )
@@ -65,7 +66,6 @@ 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
 
@@ -371,7 +371,7 @@ rnHsForeignDecl :: ForeignDecl GhcPs -> RnM (ForeignDecl GhcRn, FreeVars)
 rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
   = do { topEnv :: HscEnv <- getTopEnv
        ; name' <- lookupLocatedTopBndrRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
 
         -- Mark any PackageTarget style imports as coming from the current package
        ; let unitId = homeUnit $ hsc_dflags topEnv
@@ -383,7 +383,7 @@ rnHsForeignDecl (ForeignImport { fd_name = name, fd_sig_ty = ty, fd_fi = spec })
 
 rnHsForeignDecl (ForeignExport { fd_name = name, fd_sig_ty = ty, fd_fe = spec })
   = do { name' <- lookupLocatedOccRn name
-       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType (ForeignDeclCtx name) TypeLevel ty
        ; return (ForeignExport { fd_e_ext = noExtField
                                , fd_name = name', fd_sig_ty = ty'
                                , fd_fe = spec }
@@ -602,13 +602,14 @@ 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 ctxt TypeLevel inf_err inst_ty
+  = do { checkInferredVars ctxt inf_err inst_ty
+       ; (inst_ty', inst_fvs) <- rnHsSigType ctxt TypeLevel inst_ty
        ; let (ktv_names, _, head_ty') = splitLHsInstDeclTy inst_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)...
-             mb_nested_msg = no_nested_foralls_contexts_err
+             mb_nested_msg = noNestedForallsContextsErr
                                (text "Instance head") head_ty'
              -- ...then check if the instance head is actually headed by a
              -- class type constructor...
@@ -628,17 +629,10 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
          -- 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>"))
+       ; cls <- case (mb_nested_msg, eith_cls) of
+           (Nothing,   Right cls) -> pure cls
+           (Just err1, _)         -> bail_out err1
+           (_,         Left err2) -> bail_out err2
 
           -- Rename the bindings
           -- The typechecker (not the renamer) checks that all
@@ -680,6 +674,15 @@ rnClsInstDecl (ClsInstDecl { cid_poly_ty = inst_ty, cid_binds = mbinds
     ctxt    = GenericCtx $ text "an instance declaration"
     inf_err = Just (text "Inferred type variables are not allowed")
 
+    -- 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).
+    bail_out (l, err_msg) = do
+      addErrAt l $ withHsDocContext ctxt err_msg
+      pure $ mkUnboundName (mkTcOccFS (fsLit "<class>"))
+
 rnFamInstEqn :: HsDocContext
              -> AssocTyFamInfo
              -> FreeKiTyVars
@@ -1073,22 +1076,22 @@ rnSrcDerivDecl :: DerivDecl GhcPs -> RnM (DerivDecl GhcRn, FreeVars)
 rnSrcDerivDecl (DerivDecl _ ty mds overlap)
   = do { standalone_deriv_ok <- xoptM LangExt.StandaloneDeriving
        ; unless standalone_deriv_ok (addErr standaloneDerivErr)
-       ; (mds', ty', fvs)
-           <- rnLDerivStrategy ctxt mds $ rnHsSigWcType ctxt inf_err ty
+       ; checkInferredVars ctxt inf_err nowc_ty
+       ; (mds', ty', fvs) <- rnLDerivStrategy ctxt mds $ rnHsSigWcType ctxt 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
+       ; addNoNestedForallsContextsErr ctxt
+           (text "Standalone-derived instance head")
+           (getLHsInstDeclHead $ dropWildCards ty')
        ; 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
+    loc = getLoc $ hsib_body nowc_ty
+    nowc_ty = dropWildCards ty
 
 standaloneDerivErr :: SDoc
 standaloneDerivErr
@@ -1154,7 +1157,7 @@ bindRuleTmVars doc tyvs vars names thing_inside
 
     go ((L l (RuleBndrSig _ (L loc _) bsig)) : vars)
        (n : ns) thing_inside
-      = rnHsPatSigType bind_free_tvs doc Nothing bsig $ \ bsig' ->
+      = rnHsPatSigType bind_free_tvs doc bsig $ \ bsig' ->
         go vars ns $ \ vars' ->
         thing_inside (L l (RuleBndrSig noExtField (L loc n) bsig') : vars')
 
@@ -1494,7 +1497,7 @@ rnStandaloneKindSignature tc_names (StandaloneKindSig _ v ki)
         ; unless standalone_ki_sig_ok $ addErr standaloneKiSigErr
         ; new_v <- lookupSigCtxtOccRn (TopSigCtxt tc_names) (text "standalone kind signature") v
         ; let doc = StandaloneKindSigCtx (ppr v)
-        ; (new_ki, fvs) <- rnHsSigType doc KindLevel Nothing ki
+        ; (new_ki, fvs) <- rnHsSigType doc KindLevel ki
         ; return (StandaloneKindSig noExtField new_v new_ki, fvs)
         }
   where
@@ -1904,15 +1907,14 @@ rnLHsDerivingClause doc
     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
+      checkInferredVars doc inf_err pred_ty
+      ret@(pred_ty', _) <- rnHsSigType doc TypeLevel 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
+      addNoNestedForallsContextsErr doc (text "Derived class type")
+        (getLHsInstDeclHead pred_ty')
       pure ret
 
 rnLDerivStrategy :: forall a.
@@ -1946,7 +1948,8 @@ rnLDerivStrategy doc mds thing_inside
         AnyclassStrategy -> boring_case AnyclassStrategy
         NewtypeStrategy  -> boring_case NewtypeStrategy
         ViaStrategy via_ty ->
-          do (via_ty', fvs1) <- rnHsSigType doc TypeLevel inf_err via_ty
+          do checkInferredVars doc inf_err via_ty
+             (via_ty', fvs1) <- rnHsSigType doc TypeLevel via_ty
              let HsIB { hsib_ext  = via_imp_tvs
                       , hsib_body = via_body } = via_ty'
                  (via_exp_tv_bndrs, via_rho) = splitLHsForAllTyInvis_KP via_body
@@ -1956,10 +1959,8 @@ rnLDerivStrategy doc mds thing_inside
              -- `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
+             addNoNestedForallsContextsErr doc
+               (quotes (text "via") <+> text "type") via_rho
              (thing, fvs2) <- extendTyVarEnvFVRn via_tvs thing_inside
              pure (ViaStrategy via_ty', thing, fvs1 `plusFV` fvs2)
 
@@ -2265,7 +2266,7 @@ rnConDecl (XConDecl (ConDeclGADTPrefixPs { con_gp_names = names, con_gp_ty = ty
        ; mb_doc'   <- rnMbLHsDoc mb_doc
 
        ; let ctxt = ConDeclCtx new_names
-       ; (ty', fvs) <- rnHsSigType ctxt TypeLevel Nothing ty
+       ; (ty', fvs) <- rnHsSigType ctxt TypeLevel ty
        ; linearTypes <- xopt LangExt.LinearTypes <$> getDynFlags
 
          -- Now that operator precedence has been resolved, we can split the
@@ -2284,10 +2285,8 @@ 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.
-       ; whenIsJust (no_nested_foralls_contexts_err
-                       (text "GADT constructor type signature")
-                       res_ty) $ \(l, err_msg) ->
-           addErrAt l $ withHsDocContext ctxt err_msg
+       ; addNoNestedForallsContextsErr ctxt
+           (text "GADT constructor type signature") res_ty
 
        ; traceRn "rnConDecl (ConDeclGADTPrefixPs)"
            (ppr names $$ ppr implicit_tkvs $$ ppr explicit_tkvs)
@@ -2325,41 +2324,6 @@ 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/compiler/GHC/Rename/Pat.hs b/compiler/GHC/Rename/Pat.hs
index 06619cd142..09e2ea8cbe 100644
--- a/compiler/GHC/Rename/Pat.hs
+++ b/compiler/GHC/Rename/Pat.hs
@@ -412,7 +412,7 @@ rnPatAndThen mk (SigPat x pat sig)
        ; return (SigPat x pat' sig' ) }
   where
     rnHsPatSigTypeAndThen :: HsPatSigType GhcPs -> CpsRn (HsPatSigType GhcRn)
-    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx Nothing sig)
+    rnHsPatSigTypeAndThen sig = CpsRn (rnHsPatSigType AlwaysBind PatCtx sig)
 
 rnPatAndThen mk (LitPat x lit)
   | HsString src s <- lit
diff --git a/compiler/GHC/Rename/Utils.hs b/compiler/GHC/Rename/Utils.hs
index f76939493f..301aa4e081 100644
--- a/compiler/GHC/Rename/Utils.hs
+++ b/compiler/GHC/Rename/Utils.hs
@@ -26,8 +26,10 @@ module GHC.Rename.Utils (
 
         bindLocalNames, bindLocalNamesFV,
 
-        addNameClashErrRn, extendTyVarEnvFVRn
+        addNameClashErrRn, extendTyVarEnvFVRn,
 
+        checkInferredVars,
+        noNestedForallsContextsErr, addNoNestedForallsContextsErr
 )
 
 where
@@ -35,6 +37,7 @@ where
 
 import GHC.Prelude
 
+import GHC.Core.Type
 import GHC.Hs
 import GHC.Types.Name.Reader
 import GHC.Driver.Types
@@ -49,6 +52,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Misc
 import GHC.Types.Basic  ( TopLevelFlag(..) )
 import GHC.Data.List.SetOps ( removeDups )
+import GHC.Data.Maybe ( whenIsJust )
 import GHC.Driver.Session
 import GHC.Data.FastString
 import Control.Monad
@@ -176,6 +180,136 @@ checkShadowedOccs (global_env,local_env) get_loc_occ ns
                              || xopt LangExt.RecordWildCards dflags) }
     is_shadowed_gre _other = return True
 
+-------------------------------------
+-- | Throw an error message if a user attempts to quantify an inferred type
+-- variable in a place where specificity cannot be observed. For example,
+-- @forall {a}. [a] -> [a]@ would be rejected to the inferred type variable
+-- @{a}@, but @forall a. [a] -> [a]@ would be accepted.
+-- See @Note [Unobservably inferred type variables]@.
+checkInferredVars :: HsDocContext
+                  -> Maybe SDoc
+                  -- ^ The error msg if the signature is not allowed to contain
+                  --   manually written inferred variables.
+                  -> LHsSigType GhcPs
+                  -> RnM ()
+checkInferredVars _    Nothing    _  = return ()
+checkInferredVars ctxt (Just msg) ty =
+  let bndrs = forallty_bndrs (hsSigType ty)
+  in case find ((==) InferredSpec . hsTyVarBndrFlag) bndrs of
+    Nothing -> return ()
+    Just _  -> addErr $ withHsDocContext ctxt msg
+  where
+    forallty_bndrs :: LHsType GhcPs -> [HsTyVarBndr Specificity GhcPs]
+    forallty_bndrs (L _ ty) = case ty of
+      HsParTy _ ty' -> forallty_bndrs ty'
+      HsForAllTy { hst_tele = HsForAllInvis { hsf_invis_bndrs = tvs }}
+                    -> map unLoc tvs
+      _             -> []
+
+{-
+Note [Unobservably inferred type variables]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+While GHC's parser allows the use of inferred type variables
+(e.g., `forall {a}. <...>`) just about anywhere that type variable binders can
+appear, there are some situations where the distinction between inferred and
+specified type variables cannot be observed. For example, consider this
+instance declaration:
+
+  instance forall {a}. Eq (T a) where ...
+
+Making {a} inferred is pointless, as there is no way for user code to
+"apply" an instance declaration in a way where the inferred/specified
+distinction would make a difference. (Notably, there is no opportunity
+for visible type application of an instance declaration.) Anyone who
+writes such code is likely confused, so in an attempt to be helpful,
+we emit an error message if a user writes code like this. The
+checkInferredVars function is responsible for implementing this
+restriction.
+
+It turns out to be somewhat cumbersome to enforce this restriction in
+certain cases.  Specifically:
+
+* Quantified constraints. In the type `f :: (forall {a}. C a) => Proxy Int`,
+  there is no way to observe that {a} is inferred. Nevertheless, actually
+  rejecting this code would be tricky, as we would need to reject
+  `forall {a}. <...>` as a constraint but *accept* other uses of
+  `forall {a}. <...>` as a type (e.g., `g :: (forall {a}. a -> a) -> b -> b`).
+  This is quite tedious to do in practice, so we don't bother.
+
+* Default method type signatures (#18432). These are tricky because inferred
+  type variables can appear nested, e.g.,
+
+    class C a where
+      m         :: forall b. a -> b -> forall c.   c -> c
+      default m :: forall b. a -> b -> forall {c}. c -> c
+      m _ _ = id
+
+  Robustly checking for nested, inferred type variables ends up being a pain,
+  so we don't try to do this.
+
+For now, we simply allow inferred quantifiers to be specified here,
+even though doing so is pointless. All we lose is a warning.
+
+Aside from the places where we already use checkInferredVars, most of
+the other places where inferred vars don't make sense are in any case
+already prohibited from having foralls /at all/.  For example:
+
+  instance forall a. forall {b}. Eq (Either a b) where ...
+
+Here the nested `forall {b}` is already prohibited. (See
+Note [No nested foralls or contexts in instance types] in GHC.Hs.Type).
+-}
+
+-- | Examines a non-outermost type for @forall@s or contexts, which are assumed
+-- to be nested. For example, in the following declaration:
+--
+-- @
+-- instance forall a. forall b. C (Either a b)
+-- @
+--
+-- The outermost @forall a@ is fine, but the nested @forall b@ is not. We
+-- invoke 'noNestedForallsContextsErr' on the type @forall b. C (Either a b)@
+-- to catch the nested @forall@ and create a suitable error message.
+-- 'noNestedForallsContextsErr' returns @'Just' err_msg@ if such a @forall@ or
+-- context is found, and returns @Nothing@ otherwise.
+--
+-- This is currently used in the following 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' in
+--   "GHC.Rename.Module" and 'renameSig' in "GHC.Rename.Bind").
+--   See @Note [No nested foralls or contexts in instance types]@ in
+--   "GHC.Hs.Type".
+noNestedForallsContextsErr :: SDoc -> LHsType GhcRn -> Maybe (SrcSpan, SDoc)
+noNestedForallsContextsErr 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"
+
+-- | A common way to invoke 'noNestedForallsContextsErr'.
+addNoNestedForallsContextsErr :: HsDocContext -> SDoc -> LHsType GhcRn -> RnM ()
+addNoNestedForallsContextsErr ctxt what lty =
+  whenIsJust (noNestedForallsContextsErr what lty) $ \(l, err_msg) ->
+    addErrAt l $ withHsDocContext ctxt err_msg
 
 {-
 ************************************************************************
diff --git a/testsuite/tests/quantified-constraints/T18432.hs b/testsuite/tests/quantified-constraints/T18432.hs
new file mode 100644
index 0000000000..ba50727420
--- /dev/null
+++ b/testsuite/tests/quantified-constraints/T18432.hs
@@ -0,0 +1,10 @@
+{-# LANGUAGE QuantifiedConstraints #-}
+module Bug where
+
+import Data.Proxy
+
+class C a where
+  m :: Proxy a
+
+f :: (forall {a}. C a) => Proxy Int
+f = m
diff --git a/testsuite/tests/quantified-constraints/all.T b/testsuite/tests/quantified-constraints/all.T
index da3a6fecec..9bcc30b1a9 100644
--- a/testsuite/tests/quantified-constraints/all.T
+++ b/testsuite/tests/quantified-constraints/all.T
@@ -29,3 +29,4 @@ test('T17267c', normal, compile_fail, [''])
 test('T17267d', normal, compile_and_run, [''])
 test('T17267e', normal, compile_fail, [''])
 test('T17458', normal, compile_fail, [''])
+test('T18432', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs b/testsuite/tests/typecheck/should_compile/ExplicitSpecificity4.hs
index 4d615631b6..4d615631b6 100644
--- a/testsuite/tests/typecheck/should_fail/ExplicitSpecificity4.hs
+++ b/testsuite/tests/typecheck/should_compile/ExplicitSpecificity4.hs
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index d720891df5..51977768c7 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -712,6 +712,7 @@ test('T18129', expect_broken(18129), compile, [''])
 test('T18185', normal, compile, [''])
 test('ExplicitSpecificityA1', normal, compile, [''])
 test('ExplicitSpecificityA2', normal, compile, [''])
+test('ExplicitSpecificity4', normal, compile, [''])
 test('T17775-viewpats-a', normal, compile, [''])
 test('T17775-viewpats-b', normal, compile_fail, [''])
 test('T17775-viewpats-c', normal, compile_fail, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T18455.hs b/testsuite/tests/typecheck/should_fail/T18455.hs
new file mode 100644
index 0000000000..ad151ae9a7
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18455.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+module T18455 where
+
+class C a
+
+instance C (Either a b) where
+  {-# SPECIALISE instance forall a. forall b. C (Either a b) #-}
diff --git a/testsuite/tests/typecheck/should_fail/T18455.stderr b/testsuite/tests/typecheck/should_fail/T18455.stderr
new file mode 100644
index 0000000000..15d02d1902
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T18455.stderr
@@ -0,0 +1,4 @@
+
+T18455.hs:7:37: error:
+    SPECIALISE instance type cannot contain nested ‘forall’s or contexts
+    In a SPECIALISE instance pragma
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index c9b785554e..7b4d6d1899 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -568,7 +568,6 @@ test('T18127a', normal, compile_fail, [''])
 test('ExplicitSpecificity1', normal, compile_fail, [''])
 test('ExplicitSpecificity2', normal, compile_fail, [''])
 test('ExplicitSpecificity3', normal, compile_fail, [''])
-test('ExplicitSpecificity4', normal, compile_fail, [''])
 test('ExplicitSpecificity5', normal, compile_fail, [''])
 test('ExplicitSpecificity6', normal, compile_fail, [''])
 test('ExplicitSpecificity7', normal, compile_fail, [''])
@@ -578,3 +577,4 @@ test('ExplicitSpecificity10', normal, compile_fail, [''])
 test('T18357', normal, compile_fail, [''])
 test('T18357a', normal, compile_fail, [''])
 test('T18357b', normal, compile_fail, [''])
+test('T18455', normal, compile_fail, [''])