Use mutable update to defer out-of-scope errorswip/T17812

Previously, we let-bound an identifier to use to carry
the erroring evidence for an out-of-scope variable. But
this failed for levity-polymorphic out-of-scope variables,
leading to a panic (#17812). The new plan is to use
a mutable update to just write the erroring expression directly
where it needs to go.

Close #17812.

Test case: typecheck/should_compile/T17812

21 files changed, 143 insertions, 84 deletions

diff --git a/compiler/GHC/Data/IOEnv.hs b/compiler/GHC/Data/IOEnv.hs
index 439f101ecc..850d111818 100644
--- a/compiler/GHC/Data/IOEnv.hs
+++ b/compiler/GHC/Data/IOEnv.hs
@@ -29,7 +29,7 @@ module GHC.Data.IOEnv (
         tryM, tryAllM, tryMostM, fixM,
 
         -- I/O operations
-        IORef, newMutVar, readMutVar, writeMutVar, updMutVar,
+        IORef, newMutVar, readMutVar, writeMutVar, updMutVar, updMutVarM,
         atomicUpdMutVar, atomicUpdMutVar'
   ) where
 
@@ -193,6 +193,12 @@ readMutVar var = liftIO (readIORef var)
 updMutVar :: IORef a -> (a -> a) -> IOEnv env ()
 updMutVar var upd = liftIO (modifyIORef var upd)
 
+updMutVarM :: IORef a -> (a -> IOEnv env a) -> IOEnv env ()
+updMutVarM ref upd
+  = do { contents     <- liftIO $ readIORef ref
+       ; new_contents <- upd contents
+       ; liftIO $ writeIORef ref new_contents }
+
 -- | Atomically update the reference.  Does not force the evaluation of the
 -- new variable contents.  For strict update, use 'atomicUpdMutVar''.
 atomicUpdMutVar :: IORef a -> (a -> (a, b)) -> IOEnv env b
diff --git a/compiler/GHC/Hs/Expr.hs b/compiler/GHC/Hs/Expr.hs
index ef8934b831..78b07e54a3 100644
--- a/compiler/GHC/Hs/Expr.hs
+++ b/compiler/GHC/Hs/Expr.hs
@@ -38,7 +38,6 @@ import GHC.Hs.Binds
 -- others:
 import GHC.Tc.Types.Evidence
 import GHC.Core
-import GHC.Types.Id( Id )
 import GHC.Types.Name
 import GHC.Types.Name.Set
 import GHC.Types.Basic
@@ -252,8 +251,10 @@ data HsExpr p
                              -- Turned from HsVar to HsUnboundVar by the
                              --   renamer, when it finds an out-of-scope
                              --   variable or hole.
-                             -- The (XUnboundVar p) field becomes Id
-                             --   after typechecking
+                             -- The (XUnboundVar p) field becomes an HoleExprRef
+                             --   after typechecking; this is where the
+                             --   erroring expression will be written after
+                             --   solving. See Note [Holes] in GHC.Tc.Types.Constraint.
 
   | HsConLikeOut (XConLikeOut p)
                  ConLike     -- ^ After typechecker only; must be different
@@ -608,7 +609,11 @@ type instance XApp           (GhcPass _) = NoExtField
 
 type instance XUnboundVar    GhcPs = NoExtField
 type instance XUnboundVar    GhcRn = NoExtField
-type instance XUnboundVar    GhcTc = Id
+type instance XUnboundVar    GhcTc = HoleExprRef
+  -- We really don't need the whole HoleExprRef; just the IORef EvTerm
+  -- would be enough. But then deriving a Data instance becomes impossible.
+  -- Much, much easier just to define HoleExprRef with a Data instance and
+  -- store the whole structure.
 
 type instance XAppTypeE      GhcPs = NoExtField
 type instance XAppTypeE      GhcRn = NoExtField
diff --git a/compiler/GHC/HsToCore/Binds.hs b/compiler/GHC/HsToCore/Binds.hs
index 10534c782b..e828202a61 100644
--- a/compiler/GHC/HsToCore/Binds.hs
+++ b/compiler/GHC/HsToCore/Binds.hs
@@ -18,7 +18,7 @@ lower levels it is preserved with @let@/@letrec@s).
 
 module GHC.HsToCore.Binds
    ( dsTopLHsBinds, dsLHsBinds, decomposeRuleLhs, dsSpec
-   , dsHsWrapper, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds, dsMkUserRule
+   , dsHsWrapper, dsEvTerm, dsTcEvBinds, dsTcEvBinds_s, dsEvBinds, dsMkUserRule
    )
 where
 
diff --git a/compiler/GHC/HsToCore/Coverage.hs b/compiler/GHC/HsToCore/Coverage.hs
index cdc68599ba..db0d72bc9d 100644
--- a/compiler/GHC/HsToCore/Coverage.hs
+++ b/compiler/GHC/HsToCore/Coverage.hs
@@ -511,7 +511,7 @@ addBinTickLHsExpr boxLabel (L pos e0)
 
 addTickHsExpr :: HsExpr GhcTc -> TM (HsExpr GhcTc)
 addTickHsExpr e@(HsVar _ (L _ id))  = do freeVar id; return e
-addTickHsExpr e@(HsUnboundVar id _) = do freeVar id; return e
+addTickHsExpr e@(HsUnboundVar {})   = return e
 addTickHsExpr e@(HsRecFld _ (Ambiguous id _))   = do freeVar id; return e
 addTickHsExpr e@(HsRecFld _ (Unambiguous id _)) = do freeVar id; return e
 addTickHsExpr e@(HsConLikeOut _ con)
diff --git a/compiler/GHC/HsToCore/Expr.hs b/compiler/GHC/HsToCore/Expr.hs
index c7eeaec586..c9e5aec28e 100644
--- a/compiler/GHC/HsToCore/Expr.hs
+++ b/compiler/GHC/HsToCore/Expr.hs
@@ -268,7 +268,8 @@ dsExpr :: HsExpr GhcTc -> DsM CoreExpr
 dsExpr (HsVar    _ (L _ id))           = dsHsVar id
 dsExpr (HsRecFld _ (Unambiguous id _)) = dsHsVar id
 dsExpr (HsRecFld _ (Ambiguous   id _)) = dsHsVar id
-dsExpr (HsUnboundVar id _)             = dsHsVar id
+dsExpr (HsUnboundVar (HER ref _ _) _)  = dsEvTerm =<< readMutVar ref
+        -- See Note [Holes] in GHC.Tc.Types.Constraint
 
 dsExpr (HsPar _ e)            = dsLExpr e
 dsExpr (ExprWithTySig _ e _)  = dsLExpr e
diff --git a/compiler/GHC/Iface/Ext/Ast.hs b/compiler/GHC/Iface/Ext/Ast.hs
index 3917998c3e..4bd9ed381d 100644
--- a/compiler/GHC/Iface/Ext/Ast.hs
+++ b/compiler/GHC/Iface/Ext/Ast.hs
@@ -165,7 +165,7 @@ For subtrees in the AST that may contain symbols, the procedure is fairly
 straightforward.  If you are extending the GHC AST, you will need to provide a
 `ToHie` instance for any new types you may have introduced in the AST.
 
-Here are is an extract from the `ToHie` instance for (LHsExpr (GhcPass p)):
+Here is an extract from the `ToHie` instance for (LHsExpr (GhcPass p)):
 
   toHie e@(L mspan oexpr) = concatM $ getTypeNode e : case oexpr of
       HsVar _ (L _ var) ->
@@ -725,6 +725,7 @@ instance HiePass p => HasType (Located (HsExpr (GhcPass p))) where
       HieTc ->
         -- Some expression forms have their type immediately available
         let tyOpt = case e' of
+              HsUnboundVar (HER _ ty _) _ -> Just ty
               HsLit _ l -> Just (hsLitType l)
               HsOverLit _ o -> Just (overLitType o)
 
@@ -764,7 +765,6 @@ instance HiePass p => HasType (Located (HsExpr (GhcPass p))) where
           skipDesugaring :: HsExpr GhcTc -> Bool
           skipDesugaring e = case e of
             HsVar{}             -> False
-            HsUnboundVar{}      -> False
             HsConLikeOut{}      -> False
             HsRecFld{}          -> False
             HsOverLabel{}       -> False
@@ -791,7 +791,6 @@ class ( IsPass p
       , Data (HsTupArg (GhcPass p))
       , Data (IPBind (GhcPass p))
       , ToHie (Context (Located (IdGhcP p)))
-      , ToHie (Context (Located (XUnboundVar (GhcPass p))))
       , ToHie (RFContext (Located (AmbiguousFieldOcc (GhcPass p))))
       , ToHie (RFContext (Located (FieldOcc (GhcPass p))))
       , ToHie (TScoped (LHsWcType (GhcPass (NoGhcTcPass p))))
@@ -1053,8 +1052,7 @@ instance HiePass p => ToHie (Located (HsExpr (GhcPass p))) where
         [ toHie $ C Use (L mspan var)
              -- Patch up var location since typechecker removes it
         ]
-      HsUnboundVar var _ ->
-        [ toHie $ C Use (L mspan var) ]
+      HsUnboundVar _ _ -> []  -- there is an unbound name here, but that causes trouble
       HsConLikeOut _ con ->
         [ toHie $ C Use $ L mspan $ conLikeName con
         ]
diff --git a/compiler/GHC/Tc/Errors.hs b/compiler/GHC/Tc/Errors.hs
index e7d7ff6c2b..4f7c9dfea2 100644
--- a/compiler/GHC/Tc/Errors.hs
+++ b/compiler/GHC/Tc/Errors.hs
@@ -953,17 +953,18 @@ mkErrorTerm dflags ty err = evDelayedError ty err_fs
     err_msg = pprLocErrMsg err
     err_fs  = mkFastString $ showSDoc dflags $
               err_msg $$ text "(deferred type error)"
+
 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Hole -> TcM ()
-maybeAddDeferredHoleBinding ctxt err (Hole { hole_sort = ExprHole ev_id })
+maybeAddDeferredHoleBinding ctxt err (Hole { hole_sort = ExprHole (HER ref ref_ty _) })
 -- Only add bindings for holes in expressions
 -- not for holes in partial type signatures
 -- cf. addDeferredBinding
   | deferringAnyBindings ctxt
   = do { dflags <- getDynFlags
-       ; let err_tm = mkErrorTerm dflags (idType ev_id) err
-           -- NB: idType ev_id, not hole_ty. hole_ty might be rewritten.
+       ; let err_tm = mkErrorTerm dflags ref_ty err
+           -- NB: ref_ty, not hole_ty. hole_ty might be rewritten.
            -- See Note [Holes] in GHC.Tc.Types.Constraint
-       ; addTcEvBind (cec_binds ctxt) $ mkWantedEvBind ev_id err_tm }
+       ; writeMutVar ref err_tm }
   | otherwise
   = return ()
 maybeAddDeferredHoleBinding _ _ (Hole { hole_sort = TypeHole })
diff --git a/compiler/GHC/Tc/Gen/Expr.hs b/compiler/GHC/Tc/Gen/Expr.hs
index 15ca20b738..0a8e1925c2 100644
--- a/compiler/GHC/Tc/Gen/Expr.hs
+++ b/compiler/GHC/Tc/Gen/Expr.hs
@@ -197,15 +197,12 @@ tcExpr e@(HsRecFld {})      res_ty = tcApp e res_ty
 --
 -- Some of these started life as a true expression hole "_".
 -- Others might simply be variables that accidentally have no binding site
-tcExpr e@(HsUnboundVar _ occ) res_ty
-  = do { ty <- newOpenFlexiTyVarTy  -- Allow Int# etc (#12531)
-       ; name <- newSysName occ
-       ; let ev = mkLocalId name Many ty
-       ; emitNewExprHole occ ev ty
+tcExpr (HsUnboundVar _ occ) res_ty
+  = do { ty <- expTypeToType res_ty    -- Allow Int# etc (#12531)
+       ; her <- emitNewExprHole occ ty
        ; tcEmitBindingUsage bottomUE   -- Holes fit any usage environment
                                        -- (#18491)
-       ; tcWrapResultO (UnboundOccurrenceOf occ) e
-                       (HsUnboundVar ev occ) ty res_ty }
+       ; return (HsUnboundVar her occ) }
 
 tcExpr e@(HsLit x lit) res_ty
   = do { let lit_ty = hsLitType lit
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 6f58b6bf35..f9b54c0598 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -263,11 +263,11 @@ data Hole
 
 
 -- | Used to indicate which sort of hole we have.
-data HoleSort = ExprHole Id
+data HoleSort = ExprHole HoleExprRef
                  -- ^ Either an out-of-scope variable or a "true" hole in an
                  -- expression (TypedHoles).
-                 -- The 'Id' is where to store "evidence": this evidence
-                 -- will be an erroring expression for -fdefer-type-errors.
+                 -- The HoleExprRef says where to write the
+                 -- the erroring expression for -fdefer-type-errors.
               | TypeHole
                  -- ^ A hole in a type (PartialTypeSignatures)
               | ConstraintHole
@@ -277,17 +277,17 @@ data HoleSort = ExprHole Id
                  -- Note [Do not simplify ConstraintHoles] in GHC.Tc.Solver.
 
 instance Outputable Hole where
-  ppr (Hole { hole_sort = ExprHole id
+  ppr (Hole { hole_sort = ExprHole ref
             , hole_occ  = occ
             , hole_ty   = ty })
-    = parens $ (braces $ ppr occ <> colon <> ppr id) <+> dcolon <+> ppr ty
+    = parens $ (braces $ ppr occ <> colon <> ppr ref) <+> dcolon <+> ppr ty
   ppr (Hole { hole_sort = _other
             , hole_occ  = occ
             , hole_ty   = ty })
     = braces $ ppr occ <> colon <> ppr ty
 
 instance Outputable HoleSort where
-  ppr (ExprHole id)  = text "ExprHole:" <> ppr id
+  ppr (ExprHole ref) = text "ExprHole:" <+> ppr ref
   ppr TypeHole       = text "TypeHole"
   ppr ConstraintHole = text "CosntraintHole"
 
@@ -364,14 +364,20 @@ reported with all the other errors in GHC.Tc.Errors.
 For expression holes, the user has the option of deferring errors until runtime
 with -fdefer-type-errors. In this case, the hole actually has evidence: this
 evidence is an erroring expression that prints an error and crashes at runtime.
-The ExprHole variant of holes stores the Id that will be bound to this evidence;
-during constraint generation, this Id was inserted into the expression output
-by the type checker.
+The ExprHole variant of holes stores an IORef EvTerm that will contain this evidence;
+during constraint generation, this IORef was stored in the HsUnboundVar extension
+field by the type checker. The desugarer simply dereferences to get the CoreExpr.
 
-You might think that the type of the stored Id is the same as the type of the
+Prior to fixing #17812, we used to invent an Id to hold the erroring
+expression, and then bind it during type-checking. But this does not support
+levity-polymorphic out-of-scope identifiers. See
+typecheck/should_compile/T17812. We thus use the mutable-CoreExpr approach
+described above.
+
+You might think that the type in the HoleExprRef is the same as the type of the
 hole. However, because the hole type (hole_ty) is rewritten with respect to
 givens, this might not be the case. That is, the hole_ty is always (~) to the
-type of the Id, but they might not be `eqType`. We need the type of the generated
+type of the HoleExprRef, but they might not be `eqType`. We need the type of the generated
 evidence to match what is expected in the context of the hole, and so we must
 store these types separately.
 
diff --git a/compiler/GHC/Tc/Types/Evidence.hs b/compiler/GHC/Tc/Types/Evidence.hs
index 602d06608c..c75760853b 100644
--- a/compiler/GHC/Tc/Types/Evidence.hs
+++ b/compiler/GHC/Tc/Types/Evidence.hs
@@ -33,6 +33,9 @@ module GHC.Tc.Types.Evidence (
   EvCallStack(..),
   EvTypeable(..),
 
+  -- * HoleExprRef
+  HoleExprRef(..),
+
   -- * TcCoercion
   TcCoercion, TcCoercionR, TcCoercionN, TcCoercionP, CoercionHole,
   TcMCoercion, TcMCoercionN, TcMCoercionR,
@@ -658,6 +661,29 @@ data EvCallStack
   deriving Data.Data
 
 {-
+************************************************************************
+*                                                                      *
+         Evidence for holes
+*                                                                      *
+************************************************************************
+-}
+
+-- | Where to store evidence for expression holes
+-- See Note [Holes] in GHC.Tc.Types.Constraint
+data HoleExprRef = HER (IORef EvTerm)   -- ^ where to write the erroring expression
+                       TcType           -- ^ expected type of that expression
+                       Unique           -- ^ for debug output only
+
+instance Outputable HoleExprRef where
+  ppr (HER _ _ u) = ppr u
+
+instance Data.Data HoleExprRef where
+  -- Placeholder; we can't traverse into HoleExprRef
+  toConstr _   = abstractConstr "HoleExprRef"
+  gunfold _ _  = error "gunfold"
+  dataTypeOf _ = Data.mkNoRepType "HoleExprRef"
+
+{-
 Note [Typeable evidence terms]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 The EvTypeable data type looks isomorphic to Type, but the EvTerms
diff --git a/compiler/GHC/Tc/Types/Origin.hs b/compiler/GHC/Tc/Types/Origin.hs
index b47d4319dd..0ce4b238d4 100644
--- a/compiler/GHC/Tc/Types/Origin.hs
+++ b/compiler/GHC/Tc/Types/Origin.hs
@@ -432,7 +432,6 @@ data CtOrigin
   | ExprHoleOrigin OccName   -- from an expression hole
   | TypeHoleOrigin OccName   -- from a type hole (partial type signature)
   | PatCheckOrigin      -- normalisation of a type during pattern-match checking
-  | UnboundOccurrenceOf OccName
   | ListOrigin          -- An overloaded list
   | BracketOrigin       -- An overloaded quotation bracket
   | StaticOrigin        -- A static form
@@ -479,7 +478,7 @@ lexprCtOrigin (L _ e) = exprCtOrigin e
 
 exprCtOrigin :: HsExpr GhcRn -> CtOrigin
 exprCtOrigin (HsVar _ (L _ name)) = OccurrenceOf name
-exprCtOrigin (HsUnboundVar _ uv)  = UnboundOccurrenceOf uv
+exprCtOrigin (HsUnboundVar {})    = Shouldn'tHappenOrigin "unbound variable"
 exprCtOrigin (HsConLikeOut {})    = panic "exprCtOrigin HsConLikeOut"
 exprCtOrigin (HsRecFld _ f)       = OccurrenceOfRecSel (rdrNameAmbiguousFieldOcc f)
 exprCtOrigin (HsOverLabel _ _ l)  = OverLabelOrigin l
@@ -571,9 +570,6 @@ pprCtOrigin (KindEqOrigin t1 Nothing _ _)
   = hang (ctoHerald <+> text "a kind equality when matching")
        2 (ppr t1)
 
-pprCtOrigin (UnboundOccurrenceOf name)
-  = ctoHerald <+> text "an undeclared identifier" <+> quotes (ppr name)
-
 pprCtOrigin (DerivOriginDC dc n _)
   = hang (ctoHerald <+> text "the" <+> speakNth n
           <+> text "field of" <+> quotes (ppr dc))
diff --git a/compiler/GHC/Tc/Utils/TcMType.hs b/compiler/GHC/Tc/Utils/TcMType.hs
index 075c14a987..8d14d9201d 100644
--- a/compiler/GHC/Tc/Utils/TcMType.hs
+++ b/compiler/GHC/Tc/Utils/TcMType.hs
@@ -275,16 +275,21 @@ emitWantedEvVars :: CtOrigin -> [TcPredType] -> TcM [EvVar]
 emitWantedEvVars orig = mapM (emitWantedEvVar orig)
 
 -- | Emit a new wanted expression hole
-emitNewExprHole :: OccName   -- of the hole
-                -> Id        -- of the evidence
-                -> Type -> TcM ()
-emitNewExprHole occ ev_id ty
-  = do { loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
-       ; let hole = Hole { hole_sort = ExprHole ev_id
-                         , hole_occ  = getOccName ev_id
+emitNewExprHole :: OccName         -- of the hole
+                -> Type -> TcM HoleExprRef
+emitNewExprHole occ ty
+  = do { u <- newUnique
+       ; ref <- newTcRef (pprPanic "unfilled unbound-variable evidence" (ppr u))
+       ; let her = HER ref ty u
+
+       ; loc <- getCtLocM (ExprHoleOrigin occ) (Just TypeLevel)
+
+       ; let hole = Hole { hole_sort = ExprHole her
+                         , hole_occ  = occ
                          , hole_ty   = ty
                          , hole_loc  = loc }
-       ; emitHole hole }
+       ; emitHole hole
+       ; return her }
 
 newDict :: Class -> [TcType] -> TcM DictId
 newDict cls tys
@@ -2139,8 +2144,6 @@ zonkHole :: Hole -> TcM Hole
 zonkHole hole@(Hole { hole_ty = ty })
   = do { ty' <- zonkTcType ty
        ; return (hole { hole_ty = ty' }) }
-  -- No need to zonk the Id in any ExprHole because we never look at it
-  -- until after the final zonk and desugaring
 
 {- Note [zonkCt behaviour]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Utils/Zonk.hs b/compiler/GHC/Tc/Utils/Zonk.hs
index a1ca04b487..e233673b79 100644
--- a/compiler/GHC/Tc/Utils/Zonk.hs
+++ b/compiler/GHC/Tc/Utils/Zonk.hs
@@ -1,6 +1,7 @@
 {-# LANGUAGE CPP              #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE TypeFamilies     #-}
+{-# LANGUAGE TypeApplications #-}
 
 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 
@@ -731,8 +732,15 @@ zonkExpr env (HsVar x (L l id))
   = ASSERT2( isNothing (isDataConId_maybe id), ppr id )
     return (HsVar x (L l (zonkIdOcc env id)))
 
-zonkExpr env (HsUnboundVar v occ)
-  = return (HsUnboundVar (zonkIdOcc env v) occ)
+zonkExpr env (HsUnboundVar her occ)
+  = do her' <- zonk_her her
+       return (HsUnboundVar her' occ)
+  where
+    zonk_her :: HoleExprRef -> TcM HoleExprRef
+    zonk_her (HER ref ty u)
+      = do updMutVarM ref (zonkEvTerm env)
+           ty'  <- zonkTcTypeToTypeX env ty
+           return (HER ref ty' u)
 
 zonkExpr env (HsRecFld _ (Ambiguous v occ))
   = return (HsRecFld noExtField (Ambiguous (zonkIdOcc env v) occ))
diff --git a/testsuite/tests/ghci/scripts/T10249.stderr b/testsuite/tests/ghci/scripts/T10249.stderr
index b15f205ebb..b7e3e07a89 100644
--- a/testsuite/tests/ghci/scripts/T10249.stderr
+++ b/testsuite/tests/ghci/scripts/T10249.stderr
@@ -1,8 +1,8 @@
 
 <interactive>:1:1: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of it :: t
+    • Found hole: _ :: p
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of it :: p
                at <interactive>:1:1
     • In an equation for ‘it’: it = _
-    • Relevant bindings include it :: t (bound at <interactive>:1:1)
+    • Relevant bindings include it :: p (bound at <interactive>:1:1)
diff --git a/testsuite/tests/ghci/should_run/T15007.stderr b/testsuite/tests/ghci/should_run/T15007.stderr
index e6a98b0bcb..4a54f43e89 100644
--- a/testsuite/tests/ghci/should_run/T15007.stderr
+++ b/testsuite/tests/ghci/should_run/T15007.stderr
@@ -1,8 +1,8 @@
 
 <interactive>:3:1: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of it :: t
+    • Found hole: _ :: p
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of it :: p
                at <interactive>:3:1
     • In an equation for ‘it’: it = _
-    • Relevant bindings include it :: t (bound at <interactive>:3:1)
+    • Relevant bindings include it :: p (bound at <interactive>:3:1)
diff --git a/testsuite/tests/typecheck/should_compile/T17812.hs b/testsuite/tests/typecheck/should_compile/T17812.hs
new file mode 100644
index 0000000000..fcd8a5bc1e
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17812.hs
@@ -0,0 +1,8 @@
+{-# LANGUAGE RankNTypes, PolyKinds, KindSignatures #-}
+{-# OPTIONS_GHC -fdefer-out-of-scope-variables #-}
+
+module T17812 where
+import GHC.Types
+
+bad :: forall (r :: RuntimeRep) a (b :: TYPE r). a -> b
+bad x = outOfScope
diff --git a/testsuite/tests/typecheck/should_compile/T17812.stderr b/testsuite/tests/typecheck/should_compile/T17812.stderr
new file mode 100644
index 0000000000..83e812e589
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T17812.stderr
@@ -0,0 +1,3 @@
+
+T17812.hs:8:9: warning: [-Wdeferred-out-of-scope-variables (in -Wdefault)]
+    Variable not in scope: outOfScope
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 3fc36839d8..d60e56fcaa 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -730,6 +730,7 @@ test('T18920', normal, compile, [''])
 test('T18939_Compile', normal, compile, [''])
 test('T15942', normal, compile, [''])
 test('ClassDefaultInHsBoot', [extra_files(['ClassDefaultInHsBootA1.hs','ClassDefaultInHsBootA2.hs','ClassDefaultInHsBootA2.hs-boot','ClassDefaultInHsBootA3.hs'])], multimod_compile, ['ClassDefaultInHsBoot', '-v0'])
+test('T17812', normal, compile, [''])
 test('T17186', normal, compile, [''])
 test('CbvOverlap', normal, compile, [''])
 test('InstanceGivenOverlap', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_compile/holes.stderr b/testsuite/tests/typecheck/should_compile/holes.stderr
index a4f106ab82..ddaae57d07 100644
--- a/testsuite/tests/typecheck/should_compile/holes.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes.stderr
@@ -1,12 +1,12 @@
 
 holes.hs:3:5: warning: [-Wtyped-holes (in -Wdefault)]
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of f :: t
+    • Found hole: _ :: p
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of f :: p
                at holes.hs:3:1-5
     • In an equation for ‘f’: f = _
-    • Relevant bindings include f :: t (bound at holes.hs:3:1)
-      Valid hole fits include f :: forall {t}. t
+    • Relevant bindings include f :: p (bound at holes.hs:3:1)
+      Valid hole fits include f :: forall {p}. p
 
 holes.hs:6:7: warning: [-Wtyped-holes (in -Wdefault)]
     • Found hole: _ :: Char
@@ -15,7 +15,7 @@ holes.hs:6:7: warning: [-Wtyped-holes (in -Wdefault)]
         x :: Int (bound at holes.hs:6:3)
         g :: Int -> Char (bound at holes.hs:6:1)
       Valid hole fits include
-        f :: forall {t}. t
+        f :: forall {p}. p
         maxBound :: forall a. Bounded a => a
         minBound :: forall a. Bounded a => a
 
@@ -27,7 +27,7 @@ holes.hs:8:5: warning: [-Wtyped-holes (in -Wdefault)]
     • Relevant bindings include h :: [Char] (bound at holes.hs:8:1)
       Valid hole fits include
         h :: [Char]
-        f :: forall {t}. t
+        f :: forall {p}. p
         [] :: forall a. [a]
         mempty :: forall a. Monoid a => a
 
@@ -45,7 +45,7 @@ holes.hs:11:15: warning: [-Wtyped-holes (in -Wdefault)]
         z :: [a] -> [a]
         g :: Int -> Char
         h :: [Char]
-        f :: forall {t}. t
+        f :: forall {p}. p
         otherwise :: Bool
         False :: Bool
         True :: Bool
diff --git a/testsuite/tests/typecheck/should_compile/holes3.stderr b/testsuite/tests/typecheck/should_compile/holes3.stderr
index 2210fc5dea..52cf8db18f 100644
--- a/testsuite/tests/typecheck/should_compile/holes3.stderr
+++ b/testsuite/tests/typecheck/should_compile/holes3.stderr
@@ -1,12 +1,12 @@
 
 holes3.hs:3:5: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of f :: t
+    • Found hole: _ :: p
+      Where: ‘p’ is a rigid type variable bound by
+               the inferred type of f :: p
                at holes3.hs:3:1-5
     • In an equation for ‘f’: f = _
-    • Relevant bindings include f :: t (bound at holes3.hs:3:1)
-      Valid hole fits include f :: forall {t}. t
+    • Relevant bindings include f :: p (bound at holes3.hs:3:1)
+      Valid hole fits include f :: forall {p}. p
 
 holes3.hs:6:7: error:
     • Found hole: _gr :: Char
@@ -16,7 +16,7 @@ holes3.hs:6:7: error:
         x :: Int (bound at holes3.hs:6:3)
         g :: Int -> Char (bound at holes3.hs:6:1)
       Valid hole fits include
-        f :: forall {t}. t
+        f :: forall {p}. p
         maxBound :: forall a. Bounded a => a
         minBound :: forall a. Bounded a => a
 
@@ -29,7 +29,7 @@ holes3.hs:8:5: error:
     • Relevant bindings include h :: [Char] (bound at holes3.hs:8:1)
       Valid hole fits include
         h :: [Char]
-        f :: forall {t}. t
+        f :: forall {p}. p
         [] :: forall a. [a]
         mempty :: forall a. Monoid a => a
 
@@ -48,7 +48,7 @@ holes3.hs:11:15: error:
         z :: [a] -> [a]
         g :: Int -> Char
         h :: [Char]
-        f :: forall {t}. t
+        f :: forall {p}. p
         otherwise :: Bool
         False :: Bool
         True :: Bool
diff --git a/testsuite/tests/typecheck/should_fail/T12177.stderr b/testsuite/tests/typecheck/should_fail/T12177.stderr
index 16056e3e27..4ca175b5de 100644
--- a/testsuite/tests/typecheck/should_fail/T12177.stderr
+++ b/testsuite/tests/typecheck/should_fail/T12177.stderr
@@ -1,20 +1,20 @@
 
 T12177.hs:3:19: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of bar :: p -> p1 -> t
+    • Found hole: _ :: p2
+      Where: ‘p2’ is a rigid type variable bound by
+               the inferred type of bar :: p -> p1 -> p2
                at T12177.hs:3:1-19
     • In the expression: \ x -> _
       In the expression: \ x -> \ x -> _
       In an equation for ‘bar’: bar = \ x -> \ x -> _
     • Relevant bindings include
         x :: p1 (bound at T12177.hs:3:14)
-        bar :: p -> p1 -> t (bound at T12177.hs:3:1)
+        bar :: p -> p1 -> p2 (bound at T12177.hs:3:1)
 
 T12177.hs:5:37: error:
-    • Found hole: _ :: t
-      Where: ‘t’ is a rigid type variable bound by
-               the inferred type of baz :: p -> p1 -> p2 -> p3 -> p4 -> t
+    • Found hole: _ :: p5
+      Where: ‘p5’ is a rigid type variable bound by
+               the inferred type of baz :: p -> p1 -> p2 -> p3 -> p4 -> p5
                at T12177.hs:5:1-37
     • In the expression: \ z -> _
       In the expression: \ x -> \ z -> _
@@ -23,4 +23,4 @@ T12177.hs:5:37: error:
         z :: p4 (bound at T12177.hs:5:32)
         x :: p3 (bound at T12177.hs:5:26)
         y :: p1 (bound at T12177.hs:5:14)
-        baz :: p -> p1 -> p2 -> p3 -> p4 -> t (bound at T12177.hs:5:1)
+        baz :: p -> p1 -> p2 -> p3 -> p4 -> p5 (bound at T12177.hs:5:1)