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.

6 files changed, 202 insertions, 127 deletions

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 69f9d6de58..27d914e971 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 15775b8cf2..b8628b8b20 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
@@ -1010,22 +1013,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
@@ -1091,7 +1094,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')
 
@@ -1431,7 +1434,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
@@ -1841,15 +1844,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.
@@ -1883,7 +1885,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
@@ -1893,10 +1896,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)
 
@@ -2213,7 +2214,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
@@ -2232,10 +2233,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)
@@ -2273,41 +2272,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
 
 {-
 ************************************************************************