Treat out-of-scope variables as holes

This patch implements the idea in Trac #10569.

* An out-of-scope variable is treated as a typed expression
  hole.

* That is, we don't report it in the type checker, not the
  renamer, and we when we do report it, we give its type.

* Moreover, we can defer the error to runtime with
  -fdefer-typed-holes

In implementation terms:

* The renamer turns an unbound variable into a HsUnboundVar

* The type checker emits a Hole constraint for a
  HsUnboundVar, and turns it back into a HsVar

It was a bit painful to implement because a whole raft of
error messages change slightly.  But there was absolutely
nothing hard in principle.

Holes are reported with a bunch of possibly-useful context,
notably the "relevant bindings".  I found that this was
distracting clutter in the very common case of a mis-typed
variable that is only accidentally not in scope, so I've
arranged to print the context information only for true holes,
that is ones starting with an underscore.

Unbound data constructors use in patterns, like
  f (D x) = x
are still reportd by the renamer, and abort compilation
before type checking.

13 files changed, 314 insertions, 196 deletions

diff --git a/compiler/deSugar/Coverage.hs b/compiler/deSugar/Coverage.hs
index b44e9d8fa4..f5a9290e48 100644
--- a/compiler/deSugar/Coverage.hs
+++ b/compiler/deSugar/Coverage.hs
@@ -461,16 +461,15 @@ addBinTickLHsExpr boxLabel (L pos e0)
 -- Decoarate an HsExpr with ticks
 
 addTickHsExpr :: HsExpr Id -> TM (HsExpr Id)
-addTickHsExpr e@(HsVar id) = do freeVar id; return e
-addTickHsExpr e@(HsIPVar _) = return e
-addTickHsExpr e@(HsOverLit _) = return e
-addTickHsExpr e@(HsLit _) = return e
-addTickHsExpr (HsLam matchgroup) =
-        liftM HsLam (addTickMatchGroup True matchgroup)
-addTickHsExpr (HsLamCase ty mgs) =
-        liftM (HsLamCase ty) (addTickMatchGroup True mgs)
-addTickHsExpr (HsApp e1 e2) =
-        liftM2 HsApp (addTickLHsExprNever e1) (addTickLHsExpr e2)
+addTickHsExpr e@(HsVar id)       = do freeVar id; return e
+addTickHsExpr (HsUnboundVar {})  = panic "addTickHsExpr.HsUnboundVar"
+addTickHsExpr e@(HsIPVar _)      = return e
+addTickHsExpr e@(HsOverLit _)    = return e
+addTickHsExpr e@(HsLit _)        = return e
+addTickHsExpr (HsLam matchgroup) = liftM HsLam (addTickMatchGroup True matchgroup)
+addTickHsExpr (HsLamCase ty mgs) = liftM (HsLamCase ty) (addTickMatchGroup True mgs)
+addTickHsExpr (HsApp e1 e2)      = liftM2 HsApp (addTickLHsExprNever e1) (addTickLHsExpr e2)
+
 addTickHsExpr (OpApp e1 e2 fix e3) =
         liftM4 OpApp
                 (addTickLHsExpr e1)
@@ -599,7 +598,6 @@ addTickHsExpr (HsWrap w e) =
                 (addTickHsExpr e)       -- explicitly no tick on inside
 
 addTickHsExpr e@(HsType _) = return e
-addTickHsExpr (HsUnboundVar {}) = panic "addTickHsExpr.HsUnboundVar"
 
 -- Others dhould never happen in expression content.
 addTickHsExpr e  = pprPanic "addTickHsExpr" (ppr e)
diff --git a/compiler/deSugar/DsExpr.hs b/compiler/deSugar/DsExpr.hs
index 66f1758a03..a6cb98d372 100644
--- a/compiler/deSugar/DsExpr.hs
+++ b/compiler/deSugar/DsExpr.hs
@@ -191,6 +191,7 @@ dsExpr :: HsExpr Id -> DsM CoreExpr
 dsExpr (HsPar e)              = dsLExpr e
 dsExpr (ExprWithTySigOut e _) = dsLExpr e
 dsExpr (HsVar var)            = return (varToCoreExpr var)   -- See Note [Desugaring vars]
+dsExpr (HsUnboundVar {})      = panic "dsExpr: HsUnboundVar" -- Typechecker eliminates them
 dsExpr (HsIPVar _)            = panic "dsExpr: HsIPVar"
 dsExpr (HsLit lit)            = dsLit lit
 dsExpr (HsOverLit lit)        = dsOverLit lit
@@ -216,7 +217,6 @@ dsExpr (HsLamCase arg matches)
 dsExpr (HsApp fun arg)
   = mkCoreAppDs <$> dsLExpr fun <*>  dsLExpr arg
 
-dsExpr (HsUnboundVar _) = panic "dsExpr: HsUnboundVar"
 
 {-
 Note [Desugaring vars]
diff --git a/compiler/hsSyn/HsExpr.hs b/compiler/hsSyn/HsExpr.hs
index 16205d7322..c81707dbc2 100644
--- a/compiler/hsSyn/HsExpr.hs
+++ b/compiler/hsSyn/HsExpr.hs
@@ -27,7 +27,6 @@ import HsBinds
 import TcEvidence
 import CoreSyn
 import Var
-import RdrName
 import Name
 import BasicTypes
 import DataCon
@@ -127,11 +126,18 @@ is Less Cool because
 
 -- | A Haskell expression.
 data HsExpr id
-  = HsVar     id                        -- ^ Variable
-  | HsIPVar   HsIPName                  -- ^ Implicit parameter
-  | HsOverLit (HsOverLit id)            -- ^ Overloaded literals
+  = HsVar     id             -- ^ Variable
 
-  | HsLit     HsLit                     -- ^ Simple (non-overloaded) literals
+  | HsUnboundVar OccName     -- ^ Unbound variable; also used for "holes" _, or _x.
+                             -- Turned from HsVar to HsUnboundVar by the renamer, when
+                             --   it finds an out-of-scope variable
+                             -- Turned into HsVar by type checker, to support deferred
+                             --   type errors.  (The HsUnboundVar only has an OccName.)
+
+  | HsIPVar   HsIPName       -- ^ Implicit parameter
+  | HsOverLit (HsOverLit id) -- ^ Overloaded literals
+
+  | HsLit     HsLit          -- ^ Simple (non-overloaded) literals
 
   | HsLam     (MatchGroup id (LHsExpr id)) -- ^ Lambda abstraction. Currently always a single match
        --
@@ -492,7 +498,7 @@ data HsExpr id
 
   |  HsWrap     HsWrapper    -- TRANSLATION
                 (HsExpr id)
-  |  HsUnboundVar RdrName
+
   deriving (Typeable)
 deriving instance (DataId id) => Data (HsExpr id)
 
@@ -582,11 +588,12 @@ ppr_lexpr :: OutputableBndr id => LHsExpr id -> SDoc
 ppr_lexpr e = ppr_expr (unLoc e)
 
 ppr_expr :: forall id. OutputableBndr id => HsExpr id -> SDoc
-ppr_expr (HsVar v)       = pprPrefixOcc v
-ppr_expr (HsIPVar v)     = ppr v
-ppr_expr (HsLit lit)     = ppr lit
-ppr_expr (HsOverLit lit) = ppr lit
-ppr_expr (HsPar e)       = parens (ppr_lexpr e)
+ppr_expr (HsVar v)        = pprPrefixOcc v
+ppr_expr (HsUnboundVar v) = pprPrefixOcc v
+ppr_expr (HsIPVar v)      = ppr v
+ppr_expr (HsLit lit)      = ppr lit
+ppr_expr (HsOverLit lit)  = ppr lit
+ppr_expr (HsPar e)        = parens (ppr_lexpr e)
 
 ppr_expr (HsCoreAnn _ (_,s) e)
   = vcat [ptext (sLit "HsCoreAnn") <+> ftext s, ppr_lexpr e]
@@ -762,8 +769,6 @@ ppr_expr (HsArrForm (L _ (HsVar v)) (Just _) [arg1, arg2])
 ppr_expr (HsArrForm op _ args)
   = hang (ptext (sLit "(|") <+> ppr_lexpr op)
          4 (sep (map (pprCmdArg.unLoc) args) <+> ptext (sLit "|)"))
-ppr_expr (HsUnboundVar nm)
-  = ppr nm
 
 {-
 HsSyn records exactly where the user put parens, with HsPar.
@@ -816,14 +821,14 @@ hsExprNeedsParens _ = True
 
 isAtomicHsExpr :: HsExpr id -> Bool
 -- True of a single token
-isAtomicHsExpr (HsVar {})     = True
-isAtomicHsExpr (HsLit {})     = True
-isAtomicHsExpr (HsOverLit {}) = True
-isAtomicHsExpr (HsIPVar {})   = True
+isAtomicHsExpr (HsVar {})        = True
+isAtomicHsExpr (HsLit {})        = True
+isAtomicHsExpr (HsOverLit {})    = True
+isAtomicHsExpr (HsIPVar {})      = True
 isAtomicHsExpr (HsUnboundVar {}) = True
-isAtomicHsExpr (HsWrap _ e)   = isAtomicHsExpr e
-isAtomicHsExpr (HsPar e)      = isAtomicHsExpr (unLoc e)
-isAtomicHsExpr _              = False
+isAtomicHsExpr (HsWrap _ e)      = isAtomicHsExpr e
+isAtomicHsExpr (HsPar e)         = isAtomicHsExpr (unLoc e)
+isAtomicHsExpr _                 = False
 
 {-
 ************************************************************************
diff --git a/compiler/rename/RnEnv.hs b/compiler/rename/RnEnv.hs
index 2bdf9b5b6a..3dcf2ccb11 100644
--- a/compiler/rename/RnEnv.hs
+++ b/compiler/rename/RnEnv.hs
@@ -14,7 +14,7 @@ module RnEnv (
         lookupLocalOccThLvl_maybe,
         lookupTypeOccRn, lookupKindOccRn,
         lookupGlobalOccRn, lookupGlobalOccRn_maybe,
-        reportUnboundName,
+        reportUnboundName, unknownNameSuggestions,
 
         HsSigCtxt(..), lookupLocalTcNames, lookupSigOccRn,
         lookupSigCtxtOccRn,
@@ -896,6 +896,7 @@ addUsedRdrName :: Bool -> GlobalRdrElt -> RdrName -> RnM ()
 addUsedRdrName warn_if_deprec gre rdr
   = do { unless (isLocalGRE gre) $
          do { env <- getGblEnv
+            ; traceRn (text "addUsedRdrName 1" <+> ppr gre)
             ; updMutVar (tcg_used_rdrnames env)
                         (\s -> Set.insert rdr s) }
 
@@ -909,6 +910,7 @@ addUsedRdrNames :: [RdrName] -> RnM ()
 -- NB: no call to warnIfDeprecated; see Note [Handling of deprecations]
 addUsedRdrNames rdrs
   = do { env <- getGblEnv
+       ; traceRn (text "addUsedRdrName 2" <+> ppr rdrs)
        ; updMutVar (tcg_used_rdrnames env)
                    (\s -> foldr Set.insert s rdrs) }
 
@@ -1566,12 +1568,16 @@ unboundName wl rdr = unboundNameX wl rdr Outputable.empty
 
 unboundNameX :: WhereLooking -> RdrName -> SDoc -> RnM Name
 unboundNameX where_look rdr_name extra
-  = do  { show_helpful_errors <- goptM Opt_HelpfulErrors
-        ; let what = pprNonVarNameSpace (occNameSpace (rdrNameOcc rdr_name))
+  = do  { dflags <- getDynFlags
+        ; let show_helpful_errors = gopt Opt_HelpfulErrors dflags
+              what = pprNonVarNameSpace (occNameSpace (rdrNameOcc rdr_name))
               err = unknownNameErr what rdr_name $$ extra
         ; if not show_helpful_errors
           then addErr err
-          else do { suggestions <- unknownNameSuggestErr where_look rdr_name
+          else do { local_env  <- getLocalRdrEnv
+                  ; global_env <- getGlobalRdrEnv
+                  ; let suggestions = unknownNameSuggestions_ where_look
+                                         dflags global_env local_env rdr_name
                   ; addErr (err $$ suggestions) }
         ; return (mkUnboundName rdr_name) }
 
@@ -1588,27 +1594,33 @@ type HowInScope = Either SrcSpan ImpDeclSpec
      -- Left loc    =>  locally bound at loc
      -- Right ispec =>  imported as specified by ispec
 
-unknownNameSuggestErr :: WhereLooking -> RdrName -> RnM SDoc
-unknownNameSuggestErr where_look tried_rdr_name
-  = do { local_env <- getLocalRdrEnv
-       ; global_env <- getGlobalRdrEnv
-       ; dflags <- getDynFlags
-
-       ; let all_possibilities :: [(String, (RdrName, HowInScope))]
-             all_possibilities
-                =  [ (showPpr dflags r, (r, Left loc))
-                   | (r,loc) <- local_possibilities local_env ]
-                ++ [ (showPpr dflags r, rp) | (r, rp) <- global_possibilities global_env ]
-
-             suggest = fuzzyLookup (showPpr dflags tried_rdr_name) all_possibilities
-             perhaps = ptext (sLit "Perhaps you meant")
-             extra_err = case suggest of
-                           []  -> Outputable.empty
-                           [p] -> perhaps <+> pp_item p
-                           ps  -> sep [ perhaps <+> ptext (sLit "one of these:")
-                                      , nest 2 (pprWithCommas pp_item ps) ]
-       ; return extra_err }
+unknownNameSuggestions :: DynFlags
+                       -> GlobalRdrEnv -> LocalRdrEnv
+                       -> RdrName -> SDoc
+-- Called from the typechecker (TcErrors)
+-- when we find an unbound variable
+unknownNameSuggestions = unknownNameSuggestions_ WL_Any
+
+unknownNameSuggestions_ :: WhereLooking -> DynFlags
+                        -> GlobalRdrEnv -> LocalRdrEnv
+                        -> RdrName -> SDoc
+unknownNameSuggestions_ where_look dflags global_env
+                        local_env tried_rdr_name
+  = case suggest of
+      []  -> Outputable.empty
+      [p] -> perhaps <+> pp_item p
+      ps  -> sep [ perhaps <+> ptext (sLit "one of these:")
+                 , nest 2 (pprWithCommas pp_item ps) ]
   where
+    all_possibilities :: [(String, (RdrName, HowInScope))]
+    all_possibilities
+       =  [ (showPpr dflags r, (r, Left loc))
+          | (r,loc) <- local_possibilities local_env ]
+       ++ [ (showPpr dflags r, rp) | (r, rp) <- global_possibilities global_env ]
+
+    suggest = fuzzyLookup (showPpr dflags tried_rdr_name) all_possibilities
+    perhaps = ptext (sLit "Perhaps you meant")
+
     pp_item :: (RdrName, HowInScope) -> SDoc
     pp_item (rdr, Left loc) = pp_ns rdr <+> quotes (ppr rdr) <+> loc' -- Locally defined
         where loc' = case loc of
diff --git a/compiler/rename/RnExpr.hs b/compiler/rename/RnExpr.hs
index ef77247a5d..da0d38754d 100644
--- a/compiler/rename/RnExpr.hs
+++ b/compiler/rename/RnExpr.hs
@@ -28,7 +28,7 @@ import RnSplice         ( rnBracket, rnSpliceExpr, checkThLocalName )
 import RnTypes
 import RnPat
 import DynFlags
-import BasicTypes       ( FixityDirection(..) )
+import BasicTypes       ( FixityDirection(..), Fixity(..), minPrecedence )
 import PrelNames
 
 import Name
@@ -81,12 +81,26 @@ finishHsVar name
         checkThLocalName name
       ; return (HsVar name, unitFV name) }
 
+rnUnboundVar :: RdrName -> RnM (HsExpr Name, FreeVars)
+rnUnboundVar v
+ = do { stage <- getStage
+      ; if isUnqual v && not (in_untyped_bracket stage)
+        then -- Treat this as a "hole"
+             -- Do not fail right now; instead, return HsUnboundVar
+             -- and let the type checker report the error
+             return (HsUnboundVar (rdrNameOcc v), emptyFVs)
+
+        else -- Fail immediately (qualified name, or in untyped bracket)
+             do { n <- reportUnboundName v
+                ; return (HsVar n, emptyFVs) } }
+  where
+    in_untyped_bracket (Brack _ (RnPendingUntyped {})) = True
+    in_untyped_bracket _ = False
+
 rnExpr (HsVar v)
   = do { mb_name <- lookupOccRn_maybe v
        ; case mb_name of {
-           Nothing -> do { if startsWithUnderscore (rdrNameOcc v)
-                           then return (HsUnboundVar v, emptyFVs)
-                           else do { n <- reportUnboundName v; finishHsVar n } } ;
+           Nothing -> rnUnboundVar v ;
            Just name
               | name == nilDataConName -- Treat [] as an ExplicitList, so that
                                        -- OverloadedLists works correctly
@@ -119,25 +133,23 @@ rnExpr (HsApp fun arg)
        ; (arg',fvArg) <- rnLExpr arg
        ; return (HsApp fun' arg', fvFun `plusFV` fvArg) }
 
-rnExpr (OpApp e1 (L op_loc (HsVar op_rdr)) _ e2)
+rnExpr (OpApp e1 op  _ e2)
   = do  { (e1', fv_e1) <- rnLExpr e1
         ; (e2', fv_e2) <- rnLExpr e2
-        ; op_name <- setSrcSpan op_loc (lookupOccRn op_rdr)
-        ; (op', fv_op) <- finishHsVar op_name
-                -- NB: op' is usually just a variable, but might be
-                --     an applicatoin (assert "Foo.hs:47")
+        ; (op', fv_op) <- rnLExpr op
+
         -- Deal with fixity
         -- When renaming code synthesised from "deriving" declarations
         -- we used to avoid fixity stuff, but we can't easily tell any
         -- more, so I've removed the test.  Adding HsPars in TcGenDeriv
         -- should prevent bad things happening.
-        ; fixity <- lookupFixityRn op_name
-        ; final_e <- mkOpAppRn e1' (L op_loc op') fixity e2'
+        ; fixity <- case op' of
+                      L _ (HsVar n) -> lookupFixityRn n
+                      _             -> return (Fixity minPrecedence InfixL)
+                                       -- c.f. lookupFixity for unbound
+
+        ; final_e <- mkOpAppRn e1' op' fixity e2'
         ; return (final_e, fv_e1 `plusFV` fv_op `plusFV` fv_e2) }
-rnExpr (OpApp _ other_op _ _)
-  = failWith (vcat [ hang (ptext (sLit "Infix application with a non-variable operator:"))
-                        2 (ppr other_op)
-                   , ptext (sLit "(Probably resulting from a Template Haskell splice)") ])
 
 rnExpr (NegApp e _)
   = do { (e', fv_e)         <- rnLExpr e
@@ -288,7 +300,7 @@ Since all the symbols are reservedops we can simply reject them.
 We return a (bogus) EWildPat in each case.
 -}
 
-rnExpr EWildPat        = return (hsHoleExpr, emptyFVs)
+rnExpr EWildPat        = return (hsHoleExpr, emptyFVs)   -- "_" is just a hole
 rnExpr e@(EAsPat {})   = patSynErr e
 rnExpr e@(EViewPat {}) = patSynErr e
 rnExpr e@(ELazyPat {}) = patSynErr e
@@ -362,8 +374,8 @@ rnExpr e@(HsArrForm {}) = arrowFail e
 rnExpr other = pprPanic "rnExpr: unexpected expression" (ppr other)
         -- HsWrap
 
-hsHoleExpr :: HsExpr Name
-hsHoleExpr = HsUnboundVar (mkRdrUnqual (mkVarOcc "_"))
+hsHoleExpr :: HsExpr id
+hsHoleExpr = HsUnboundVar (mkVarOcc "_")
 
 arrowFail :: HsExpr RdrName -> RnM (HsExpr Name, FreeVars)
 arrowFail e
diff --git a/compiler/typecheck/TcErrors.hs b/compiler/typecheck/TcErrors.hs
index 20103dd760..3af562be76 100644
--- a/compiler/typecheck/TcErrors.hs
+++ b/compiler/typecheck/TcErrors.hs
@@ -13,6 +13,7 @@ import TcRnTypes
 import TcRnMonad
 import TcMType
 import TcType
+import RnEnv( unknownNameSuggestions )
 import TypeRep
 import Type
 import Kind ( isKind )
@@ -25,7 +26,7 @@ import TyCon
 import DataCon
 import TcEvidence
 import Name
-import RdrName          ( lookupGRE_Name, GlobalRdrEnv )
+import RdrName ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual )
 import Id
 import Var
 import VarSet
@@ -164,7 +165,8 @@ report_unsolved mb_binds_var err_as_warn defer_errs expr_holes type_holes wanted
                             , cec_warn_redundant = warn_redundant
                             , cec_binds    = mb_binds_var }
 
-       ; reportWanteds err_ctxt wanted }
+       ; tc_lvl <- getTcLevel
+       ; reportWanteds err_ctxt tc_lvl wanted }
 
 --------------------------------------------
 --      Internal functions
@@ -223,30 +225,34 @@ reportImplic :: ReportErrCtxt -> Implication -> TcM ()
 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                                  , ic_wanted = wanted, ic_binds = evb
                                  , ic_status = status, ic_info = info
-                                 , ic_env = tcl_env })
+                                 , ic_env = tcl_env, ic_tclvl = tc_lvl })
   | BracketSkol <- info
-  , not (isInsolubleStatus status)
+  , not insoluble
   = return ()        -- For Template Haskell brackets report only
                      -- definite errors. The whole thing will be re-checked
                      -- later when we plug it in, and meanwhile there may
                      -- certainly be un-satisfied constraints
 
   | otherwise
-  = do { reportWanteds ctxt' wanted
+  = do { reportWanteds ctxt' tc_lvl wanted
        ; traceTc "reportImplic" (ppr implic)
        ; when (cec_warn_redundant ctxt) $
          warnRedundantConstraints ctxt' tcl_env info' dead_givens }
   where
+    insoluble    = isInsolubleStatus status
     (env1, tvs') = mapAccumL tidyTyVarBndr (cec_tidy ctxt) tvs
     (env2, info') = tidySkolemInfo env1 info
     implic' = implic { ic_skols = tvs'
                      , ic_given = map (tidyEvVar env2) given
                      , ic_info  = info' }
-    ctxt' = ctxt { cec_tidy  = env2
-                 , cec_encl  = implic' : cec_encl ctxt
-                 , cec_binds = case cec_binds ctxt of
-                                 Nothing -> Nothing
-                                 Just {} -> Just evb }
+    ctxt' = ctxt { cec_tidy     = env2
+                 , cec_encl     = implic' : cec_encl ctxt
+                 , cec_suppress = insoluble  -- Suppress inessential errors if there
+                                             -- are are insolubles anywhere in the
+                                             -- tree rooted here
+                 , cec_binds    = case cec_binds ctxt of
+                                     Nothing -> Nothing
+                                     Just {} -> Just evb }
     dead_givens = case status of
                     IC_Solved { ics_dead = dead } -> dead
                     _                             -> []
@@ -297,26 +303,24 @@ But without the context we won't find beta := Zero.
 This only matters in instance declarations..
 -}
 
-reportWanteds :: ReportErrCtxt -> WantedConstraints -> TcM ()
-reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
+reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
+reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   = do { traceTc "reportWanteds" (vcat [ ptext (sLit "Simples =") <+> ppr simples
                                        , ptext (sLit "Suppress =") <+> ppr (cec_suppress ctxt)])
-       ; let tidy_insols  = bagToList (mapBag (tidyCt env) insols)
-             tidy_simples = bagToList (mapBag (tidyCt env) simples)
+       ; let tidy_cts = bagToList (mapBag (tidyCt env) (insols `unionBags` simples))
 
          -- First deal with things that are utterly wrong
          -- Like Int ~ Bool (incl nullary TyCons)
          -- or  Int ~ t a   (AppTy on one side)
-         -- Do this first so that we know the ctxt for the nested implications
-       ; (ctxt1, insols1) <- tryReporters ctxt  insol_given  tidy_insols
-       ; (ctxt2, insols2) <- tryReporters ctxt1 insol_wanted insols1
-
-         -- For the simple wanteds, suppress them if there are any
-         -- insolubles in the tree, to avoid unnecessary clutter
-       ; let ctxt2' = ctxt { cec_suppress = cec_suppress ctxt2
-                                         || anyBag insolubleImplic implics }
-
-       ; (_, leftovers) <- tryReporters ctxt2' reporters (insols2 ++ tidy_simples)
+         -- These ones are not suppressed by the incoming context
+       ; let ctxt_for_insols = ctxt { cec_suppress = False }
+       ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
+
+         -- Now all the other constraints.  We suppress errors here if
+         -- any of the first batch failed, or if the enclosing context
+         -- says to suppress
+       ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
+       ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
        ; MASSERT2( null leftovers, ppr leftovers )
 
             -- All the Derived ones have been filtered out of simples
@@ -324,52 +328,56 @@ reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = impli
             -- to report unsolved Derived goals as errors
             -- See Note [Do not report derived but soluble errors]
 
-     ; mapBagM_ (reportImplic ctxt1) implics }
+     ; mapBagM_ (reportImplic ctxt2) implics }
             -- NB ctxt1: don't suppress inner insolubles if there's only a
             -- wanted insoluble here; but do suppress inner insolubles
             -- if there's a *given* insoluble here (= inaccessible code)
  where
     env = cec_tidy ctxt
-    insol_given  = [ ("insoluble1", is_given &&& utterly_wrong,  True, mkGroupReporter mkEqErr)
-                   , ("insoluble2", is_given &&& is_equality,    True, mkSkolReporter) ]
-    insol_wanted = [ ("insoluble3",              utterly_wrong,  True, mkGroupReporter mkEqErr)
-                   , ("insoluble4",              is_equality,    True, mkSkolReporter) ]
-
-    reporters = [ ("Holes",          is_hole,         False, mkHoleReporter)
-
-                  -- Report equalities of form (a~ty).  They are usually
-                  -- skolem-equalities, and they cause confusing knock-on
-                  -- effects in other errors; see test T4093b.
-                , ("Skolem equalities", is_skol_eq,  True,  mkSkolReporter)
-
-                  -- Other equalities; also confusing knock on effects
-                , ("Equalities",      is_equality, True,  mkGroupReporter mkEqErr)
-
-                , ("Implicit params", is_ip,       False, mkGroupReporter mkIPErr)
-                , ("Irreds",          is_irred,    False, mkGroupReporter mkIrredErr)
-                , ("Dicts",           is_dict,     False, mkGroupReporter mkDictErr) ]
 
-    (&&&) :: (Ct->PredTree->Bool) -> (Ct->PredTree->Bool) -> (Ct->PredTree->Bool)
-    (&&&) p1 p2 ct pred = p1 ct pred && p2 ct pred
-
-    is_skol_eq, is_hole, is_dict,
+    -- report1: ones that should *not* be suppresed by
+    --          an insoluble somewhere else in the tree
+    -- It's crucial that anything that is considered insoluble
+    -- (see TcRnTypes.trulyInsoluble) is caught here, otherwise
+    -- we might suppress its error message, and proceed on past
+    -- type checking to get a Lint error later
+    report1 = [ ("insoluble1",   is_given,        True, mkGroupReporter mkEqErr)
+              , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
+              , ("insoluble3",   rigid_nom_tv_eq, True, mkSkolReporter)
+              , ("insoluble4",   rigid_nom_eq,    True, mkGroupReporter mkEqErr)
+              , ("Out of scope", is_out_of_scope, True,  mkHoleReporter)
+              , ("Holes",        is_hole,         False, mkHoleReporter)
+
+                  -- The only remaining equalities are alpha ~ ty,
+                  -- where alpha is untouchable; and representational equalities
+              , ("Other eqs",    is_equality,     False, mkGroupReporter mkEqErr) ]
+
+    -- report2: we suppress these if there are insolubles elsewhere in the tree
+    report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)
+              , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)
+              , ("Dicts",           is_dict,         False, mkGroupReporter mkDictErr) ]
+
+    rigid_nom_eq, rigid_nom_tv_eq, is_hole, is_dict,
       is_equality, is_ip, is_irred :: Ct -> PredTree -> Bool
 
-    utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigid ty1 && isRigid ty2
+    utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
     utterly_wrong _ _                      = False
 
-    is_hole ct _ = isHoleCt ct
+    is_out_of_scope ct _ = isOutOfScopeCt ct
+    is_hole         ct _ = isHoleCt ct
 
     is_given  ct _ = not (isWantedCt ct)  -- The Derived ones are actually all from Givens
 
+    -- Skolem (i.e. non-meta) type variable on the left
+    rigid_nom_eq _ pred = isRigidEqPred tc_lvl pred
+
+    rigid_nom_tv_eq _ pred
+      | EqPred _ ty1 _ <- pred = isRigidEqPred tc_lvl pred && isTyVarTy ty1
+      | otherwise              = False
+
     is_equality _ (EqPred {}) = True
     is_equality _ _           = False
 
-    is_skol_eq ct (EqPred NomEq ty1 ty2) =  not (isDerivedCt ct)
-                                         && isRigidOrSkol ty1
-                                         && isRigidOrSkol ty2
-    is_skol_eq _ _ = False
-
     is_dict _ (ClassPred {}) = True
     is_dict _ _              = False
 
@@ -380,22 +388,7 @@ reportWanteds ctxt (WC { wc_simple = simples, wc_insol = insols, wc_impl = impli
     is_irred _ _              = False
 
 
--- isRigidEqPred :: PredTree -> Bool
--- isRigidEqPred (EqPred NomEq ty1 ty2) = isRigid ty1 && isRigid ty2
--- isRigidEqPred _                      = False
-
 ---------------
-isRigid, isRigidOrSkol :: Type -> Bool
-isRigid ty
-  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
-  | Just {} <- tcSplitAppTy_maybe ty        = True
-  | isForAllTy ty                           = True
-  | otherwise                               = False
-
-isRigidOrSkol ty
-  | Just tv <- getTyVar_maybe ty = isSkolemTyVar tv
-  | otherwise                    = isRigid ty
-
 isTyFun_maybe :: Type -> Maybe TyCon
 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
                       Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
@@ -686,28 +679,52 @@ mkIrredErr ctxt cts
 ----------------
 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
 mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
-  = do { let tyvars = varSetElems (tyVarsOfCt ct)
-             tyvars_msg = map loc_msg tyvars
-             msg = vcat [ hang (ptext (sLit "Found hole") <+> quotes (ppr occ))
-                             2 (ptext (sLit "with type:") <+> pprType (ctEvPred (ctEvidence ct)))
-                        , ppUnless (null tyvars) (ptext (sLit "Where:") <+> vcat tyvars_msg)
-                        , hint ]
-       ; (ctxt, binds_doc, ct) <- relevantBindings False ctxt ct
+  | isOutOfScopeCt ct
+  = do { dflags  <- getDynFlags
+       ; rdr_env <- getGlobalRdrEnv
+       ; mkLongErrAt (RealSrcSpan (tcl_loc lcl_env)) var_msg
+                     (unknownNameSuggestions dflags rdr_env
+                                             (tcl_rdr lcl_env) (mkRdrUnqual occ)) }
+
+  | otherwise
+  = do { (ctxt, binds_doc, ct) <- relevantBindings False ctxt ct
                -- The 'False' means "don't filter the bindings"; see Trac #8191
-       ; mkErrorMsgFromCt ctxt ct (msg $$ binds_doc) }
+       ; mkErrorMsgFromCt ctxt ct (hole_msg $$ binds_doc) }
+
   where
-    hint
-      | TypeHole  <- hole_sort
-      , HoleError <- cec_type_holes ctxt
-      = ptext (sLit "To use the inferred type, enable PartialTypeSignatures")
+    ct_loc  = ctLoc ct
+    lcl_env = ctLocEnv ct_loc
 
-      | ExprHole <- hole_sort         -- Give hint for, say,   f x = _x
-      , lengthFS (occNameFS occ) > 1  -- Don't give this hint for plain "_", which isn't legal Haskell
-      = ptext (sLit "Or perhaps") <+> quotes (ppr occ)
-        <+> ptext (sLit "is mis-spelled, or not in scope")
+    var_msg  = hang herald  -- Print v :: ty only if the type has structure
+                  2 (if boring_type
+                     then ppr occ
+                     else pp_with_type)
 
-      | otherwise
-      = empty
+    hole_msg = vcat [ hang (ptext (sLit "Found hole:"))
+                         2 pp_with_type
+                    , tyvars_msg, hint ]
+
+    pp_with_type = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
+    herald | isDataOcc occ = ptext (sLit "Data constructor not in scope:")
+           | otherwise     = ptext (sLit "Variable not in scope:")
+
+    hole_ty    = ctEvPred (ctEvidence ct)
+    tyvars     = varSetElems (tyVarsOfType hole_ty)
+    tyvars_msg = ppUnless (null tyvars) $
+                 ptext (sLit "Where:") <+> vcat (map loc_msg tyvars)
+    boring_type = isTyVarTy hole_ty
+
+    hint | TypeHole  <- hole_sort
+         , HoleError <- cec_type_holes ctxt
+         = ptext (sLit "To use the inferred type, enable PartialTypeSignatures")
+
+         | ExprHole <- hole_sort         -- Give hint for, say,   f x = _x
+         , lengthFS (occNameFS occ) > 1  -- Don't give this hint for plain "_"
+         = ptext (sLit "Or perhaps") <+> quotes (ppr occ)
+           <+> ptext (sLit "is mis-spelled, or not in scope")
+
+         | otherwise
+         = empty
 
     loc_msg tv
        = case tcTyVarDetails tv of
@@ -1041,7 +1058,7 @@ misMatchOrCND :: ReportErrCtxt -> Ct -> Maybe SwapFlag -> TcType -> TcType -> SD
 -- If oriented then ty1 is actual, ty2 is expected
 misMatchOrCND ctxt ct oriented ty1 ty2
   | null givens ||
-    (isRigid ty1 && isRigid ty2) ||
+    (isRigidTy ty1 && isRigidTy ty2) ||
     isGivenCt ct
        -- If the equality is unconditionally insoluble
        -- or there is no context, don't report the context
@@ -1180,7 +1197,7 @@ sameOccExtra ty1 ty2
   , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
   , let n1 = tyConName tc1
         n2 = tyConName tc2
-        same_occ = nameOccName n1                  == nameOccName n2
+        same_occ = nameOccName n1                   == nameOccName n2
         same_pkg = modulePackageKey (nameModule n1) == modulePackageKey (nameModule n2)
   , n1 /= n2   -- Different Names
   , same_occ   -- but same OccName
diff --git a/compiler/typecheck/TcExpr.hs b/compiler/typecheck/TcExpr.hs
index 397834a00c..826d1432a7 100644
--- a/compiler/typecheck/TcExpr.hs
+++ b/compiler/typecheck/TcExpr.hs
@@ -38,7 +38,6 @@ import DsMonad
 import Id
 import ConLike
 import DataCon
-import RdrName
 import Name
 import TyCon
 import Type
@@ -126,8 +125,16 @@ tcInferRhoNC (L loc expr)
     do { (expr', rho) <- tcInfer (tcExpr expr)
        ; return (L loc expr', rho) }
 
-tcHole :: OccName -> TcRhoType -> TcM (HsExpr TcId)
-tcHole occ res_ty
+tcUnboundId :: OccName -> TcRhoType -> TcM (HsExpr TcId)
+-- Typechedk an occurrence of an unbound Id
+--
+-- Some of these started life as a true hole "_".  Others might simply
+-- be variables that accidentally have no binding site
+--
+-- We turn all of them into HsVar, since HsUnboundVar can't contain an
+-- Id; and indeed the evidence for the CHoleCan does bind it, so it's
+-- not unbound any more!
+tcUnboundId occ res_ty
  = do { ty <- newFlexiTyVarTy liftedTypeKind
       ; name <- newSysName occ
       ; let ev = mkLocalId name ty
@@ -149,7 +156,8 @@ tcExpr :: HsExpr Name -> TcRhoType -> TcM (HsExpr TcId)
 tcExpr e res_ty | debugIsOn && isSigmaTy res_ty     -- Sanity check
                 = pprPanic "tcExpr: sigma" (ppr res_ty $$ ppr e)
 
-tcExpr (HsVar name)  res_ty = tcCheckId name res_ty
+tcExpr (HsVar name)     res_ty = tcCheckId name res_ty
+tcExpr (HsUnboundVar v) res_ty = tcUnboundId v res_ty
 
 tcExpr (HsApp e1 e2) res_ty = tcApp e1 [e2] res_ty
 
@@ -237,8 +245,6 @@ tcExpr (HsType ty) _
         -- so it's not enabled yet.
         -- Can't eliminate it altogether from the parser, because the
         -- same parser parses *patterns*.
-tcExpr (HsUnboundVar v) res_ty
-  = tcHole (rdrNameOcc v) res_ty
 
 {-
 ************************************************************************
diff --git a/compiler/typecheck/TcRnTypes.hs b/compiler/typecheck/TcRnTypes.hs
index 411294b398..6c3c73e584 100644
--- a/compiler/typecheck/TcRnTypes.hs
+++ b/compiler/typecheck/TcRnTypes.hs
@@ -55,7 +55,7 @@ module TcRnTypes(
         isEmptyCts, isCTyEqCan, isCFunEqCan,
         isCDictCan_Maybe, isCFunEqCan_maybe,
         isCIrredEvCan, isCNonCanonical, isWantedCt, isDerivedCt,
-        isGivenCt, isHoleCt, isExprHoleCt, isTypeHoleCt,
+        isGivenCt, isHoleCt, isOutOfScopeCt, isExprHoleCt, isTypeHoleCt,
         ctEvidence, ctLoc, setCtLoc, ctPred, ctFlavour, ctEqRel, ctOrigin,
         mkNonCanonical, mkNonCanonicalCt,
         ctEvPred, ctEvLoc, ctEvOrigin, ctEvEqRel,
@@ -1395,6 +1395,13 @@ isHoleCt:: Ct -> Bool
 isHoleCt (CHoleCan {}) = True
 isHoleCt _ = False
 
+isOutOfScopeCt :: Ct -> Bool
+-- A Hole that does not have a leading underscore is
+-- simply an out-of-scope variable, and we treat that
+-- a bit differently when it comes to error reporting
+isOutOfScopeCt (CHoleCan { cc_occ = occ }) = not (startsWithUnderscore occ)
+isOutOfScopeCt _ = False
+
 isExprHoleCt :: Ct -> Bool
 isExprHoleCt (CHoleCan { cc_hole = ExprHole }) = True
 isExprHoleCt _ = False
@@ -1510,22 +1517,20 @@ isInsolubleStatus _            = False
 insolubleImplic :: Implication -> Bool
 insolubleImplic ic = isInsolubleStatus (ic_status ic)
 
-insolubleWC :: WantedConstraints -> Bool
-insolubleWC (WC { wc_impl = implics, wc_insol = insols })
-  =  anyBag trulyInsoluble  insols
+insolubleWC :: TcLevel -> WantedConstraints -> Bool
+insolubleWC tc_lvl (WC { wc_impl = implics, wc_insol = insols })
+  =  anyBag (trulyInsoluble tc_lvl) insols
   || anyBag insolubleImplic implics
 
-trulyInsoluble :: Ct -> Bool
+trulyInsoluble :: TcLevel -> Ct -> Bool
 -- The constraint is in the wc_insol set,
 -- but we do not treat as truly isoluble
 --  a) type-holes, arising from PartialTypeSignatures,
---  b) superclass constraints, arising from the emitInsoluble
---     in TcInstDcls.tcSuperClasses. In fact only equalities
---     are truly-insoluble.
+--  b) an out-of-scope variable
 -- Yuk!
-trulyInsoluble insol
-  =  isEqPred (ctPred insol)
-  && not (isTypeHoleCt insol)
+trulyInsoluble tc_lvl insol
+  =  isOutOfScopeCt insol
+  || isRigidEqPred tc_lvl (classifyPredType (ctPred insol))
 
 instance Outputable WantedConstraints where
   ppr (WC {wc_simple = s, wc_impl = i, wc_insol = n})
diff --git a/compiler/typecheck/TcRules.hs b/compiler/typecheck/TcRules.hs
index 3ac160ec3d..f36c476d62 100644
--- a/compiler/typecheck/TcRules.hs
+++ b/compiler/typecheck/TcRules.hs
@@ -298,12 +298,13 @@ simplifyRule :: RuleName
 simplifyRule name lhs_wanted rhs_wanted
   = do {         -- We allow ourselves to unify environment
                  -- variables: runTcS runs with topTcLevel
-         (insoluble, _) <- runTcS $
+          tc_lvl <- getTcLevel
+       ;  (insoluble, _) <- runTcS $
              do { -- First solve the LHS and *then* solve the RHS
                   -- See Note [Solve order for RULES]
                   lhs_resid <- solveWanteds lhs_wanted
                 ; rhs_resid <- solveWanteds rhs_wanted
-                ; return (insolubleWC lhs_resid || insolubleWC rhs_resid) }
+                ; return (insolubleWC tc_lvl lhs_resid || insolubleWC tc_lvl rhs_resid) }
 
        ; zonked_lhs_simples <- zonkSimples (wc_simple lhs_wanted)
        ; let (q_cts, non_q_cts) = partitionBag quantify_me zonked_lhs_simples
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 5ea20ed83d..a8e75c04f3 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -33,7 +33,7 @@ module TcSMonad (
     checkReductionDepth,
 
     getInstEnvs, getFamInstEnvs,                -- Getting the environments
-    getTopEnv, getGblEnv, getTcEvBinds, getTcLevel,
+    getTopEnv, getGblEnv, getLclEnv, getTcEvBinds, getTcLevel,
     getTcEvBindsMap,
     tcLookupClass,
 
@@ -2458,6 +2458,9 @@ getTopEnv = wrapTcS $ TcM.getTopEnv
 getGblEnv :: TcS TcGblEnv
 getGblEnv = wrapTcS $ TcM.getGblEnv
 
+getLclEnv :: TcS TcLclEnv
+getLclEnv = wrapTcS $ TcM.getLclEnv
+
 tcLookupClass :: Name -> TcS Class
 tcLookupClass c = wrapTcS $ TcM.tcLookupClass c
 
@@ -2851,7 +2854,7 @@ deferTcSForAllEq role loc (tvs1,body1) (tvs2,body2)
         ; coe_inside <- case freshness of
             Cached -> return (ctEvCoercion ctev)
             Fresh  -> do { ev_binds_var <- newTcEvBinds
-                         ; env <- wrapTcS $ TcM.getLclEnv
+                         ; env <- getLclEnv
                          ; let ev_binds = TcEvBinds ev_binds_var
                                new_ct = mkNonCanonical ctev
                                new_co = ctEvCoercion ctev
diff --git a/compiler/typecheck/TcSimplify.hs b/compiler/typecheck/TcSimplify.hs
index 9d73940621..f4ff467ae4 100644
--- a/compiler/typecheck/TcSimplify.hs
+++ b/compiler/typecheck/TcSimplify.hs
@@ -330,7 +330,8 @@ simplifyAmbiguityCheck ty wanteds
        -- inaccessible code
        ; allow_ambiguous <- xoptM Opt_AllowAmbiguousTypes
        ; traceTc "reportUnsolved(ambig) {" empty
-       ; unless (allow_ambiguous && not (insolubleWC final_wc))
+       ; tc_lvl <- TcRn.getTcLevel
+       ; unless (allow_ambiguous && not (insolubleWC tc_lvl final_wc))
                 (discardResult (reportUnsolved final_wc))
        ; traceTc "reportUnsolved(ambig) }" empty
 
@@ -439,7 +440,7 @@ simplifyInfer rhs_tclvl apply_mr name_taus wanteds
        ; null_ev_binds_var <- TcM.newTcEvBinds
        ; let wanted_transformed = dropDerivedWC wanted_transformed_incl_derivs
        ; quant_pred_candidates   -- Fully zonked
-           <- if insolubleWC wanted_transformed_incl_derivs
+           <- if insolubleWC rhs_tclvl wanted_transformed_incl_derivs
               then return []   -- See Note [Quantification with errors]
                                -- NB: must include derived errors in this test,
                                --     hence "incl_derivs"
@@ -997,6 +998,7 @@ setImplicationStatus :: Implication -> TcS (Maybe Implication)
 -- Return Nothing if we can discard the implication altogether
 setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _
                                     , ic_info = info
+                                    , ic_tclvl  = tc_lvl
                                     , ic_wanted = wc
                                     , ic_given = givens })
  | some_insoluble
@@ -1044,7 +1046,7 @@ setImplicationStatus implic@(Implic { ic_binds = EvBindsVar ev_binds_var _
  where
    WC { wc_simple = simples, wc_impl = implics, wc_insol = insols } = wc
 
-   some_insoluble = insolubleWC wc
+   some_insoluble = insolubleWC tc_lvl wc
    some_unsolved = not (isEmptyBag simples && isEmptyBag insols)
                  || isNothing mb_implic_needs
 
@@ -1775,7 +1777,11 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
   where
     try_group
       | Just subst <- mb_subst
-      = do { wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
+      = do { lcl_env <- TcS.getLclEnv
+           ; let loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
+                             , ctl_env    = lcl_env
+                             , ctl_depth  = initialSubGoalDepth }
+           ; wanted_evs <- mapM (newWantedEvVarNC loc . substTy subst . ctPred)
                                 wanteds
            ; residual_wanted <- solveSimpleWanteds $ listToBag $
                                 map mkNonCanonical wanted_evs
@@ -1788,9 +1794,6 @@ disambigGroup (default_ty:default_tys) group@(the_tv, wanteds)
       -- Make sure the kinds match too; hence this call to tcMatchTy
       -- E.g. suppose the only constraint was (Typeable k (a::k))
 
-    loc = CtLoc { ctl_origin = GivenOrigin UnkSkol
-                , ctl_env = panic "disambigGroup:env"
-                , ctl_depth = initialSubGoalDepth }
 
 {-
 Note [Avoiding spurious errors]
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index 75d0a5cfd9..c3e12c3c83 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -70,6 +70,7 @@ module TcType (
   isTauTy, isTauTyCon, tcIsTyVarTy, tcIsForAllTy,
   isPredTy, isTyVarClassPred, isTyVarExposed,
   checkValidClsArgs, hasTyVarHead,
+  isRigidEqPred, isRigidTy,
 
   ---------------------------------
   -- Misc type manipulators
@@ -1477,6 +1478,28 @@ isTyVarExposed tv (AppTy fun arg) = isTyVarExposed tv fun
                                  || isTyVarExposed tv arg
 isTyVarExposed _  (ForAllTy {})   = False
 
+isRigidTy :: TcType -> Bool
+isRigidTy ty
+  | Just (tc,_) <- tcSplitTyConApp_maybe ty = isGenerativeTyCon tc Nominal
+  | Just {} <- tcSplitAppTy_maybe ty        = True
+  | isForAllTy ty                           = True
+  | otherwise                               = False
+
+isRigidEqPred :: TcLevel -> PredTree -> Bool
+-- ^ True of all Nominal equalities that are solidly insoluble
+-- This means all equalities *except*
+--   * Meta-tv non-SigTv on LHS
+--   * Meta-tv SigTv on LHS, tyvar on right
+isRigidEqPred tc_lvl (EqPred NomEq ty1 _)
+  | Just tv1 <- tcGetTyVar_maybe ty1
+  = ASSERT2( isTcTyVar tv1, ppr tv1 )
+    not (isMetaTyVar tv1) || isTouchableMetaTyVar tc_lvl tv1
+
+  | otherwise  -- LHS is not a tyvar
+  = True
+
+isRigidEqPred _ _ = False  -- Not an equality
+
 {-
 ************************************************************************
 *                                                                      *
diff --git a/docs/users_guide/glasgow_exts.xml b/docs/users_guide/glasgow_exts.xml
index 44caf76295..462509290a 100644
--- a/docs/users_guide/glasgow_exts.xml
+++ b/docs/users_guide/glasgow_exts.xml
@@ -8779,15 +8779,39 @@ be suppressed entirely by <option>-fnowarn-typed-holes</option>).
 <para>
 The result is that a hole will behave
 like <literal>undefined</literal>, but with the added benefits that it shows a
-warning at compile time and will show another warning message if it gets
-evaluated at runtime.. This behaviour follows that of the
+warning at compile time, and will show the same message if it gets
+evaluated at runtime. This behaviour follows that of the
 <literal>-fdefer-type-errors</literal> option, which implies
 <literal>-fdefer-typed-holes</literal>. See <xref linkend="defer-type-errors"/>.
 </para>
 </listitem>
 
 <listitem><para>
-Unbound identifiers with the same name are never unified, even within the 
+All unbound identifiers are treated as typed holes, <emphasis>whether or not they
+start with an underscore</emphasis>.  The only difference is in the error message:
+<programlisting>
+cons z = z : True : _x : y
+</programlisting>
+yields the errors
+<programlisting>
+Foo.hs:5:15: error:
+    Found hole: _x :: Bool
+    Relevant bindings include
+      p :: Bool (bound at Foo.hs:3:6)
+      cons :: Bool -> [Bool] (bound at Foo.hs:3:1)
+
+Foo.hs:5:20: error:
+    Variable not in scope: y :: [Bool]
+</programlisting>
+More information is given for explicit holes (i.e. ones that start with an underscore),
+than for out-of-scope variables, because the latter are often
+unintended typos, so the extra information is distracting.
+If you the detailed information, use a leading underscore to
+make explicit your intent to use a hole.
+</para></listitem>
+
+<listitem><para>
+Unbound identifiers with the same name are never unified, even within the
 same function, but shown individually.
 For example:
 <programlisting>
@@ -8824,9 +8848,18 @@ is a perfectly legal variable, and its behaviour is unchanged when it is in scop
 <programlisting>
 f _x = _x + 1
 </programlisting>
-does not elict any errors.  Only a variable starting with an underscore <emphasis>that is not in scope</emphasis>
-is treated as an error (which it always was), albeit now with a more informative error message
+does not elict any errors.  Only a variable <emphasis>that is not in scope</emphasis>
+(whether or not it starts with an underscore)
+is treated as an error (which it always was), albeit now with a more informative error message.
+</para></listitem>
+
+<listitem><para>
+Unbound data constructors used in expressions behave exactly as above.
+However, unbound data constructors used in <emphasis>patterns</emphasis> cannot
+be deferred, and instead bring compilation to a halt.  (In implementation terms, they
+are reported by the renamer rather than the type checker.)
 </para></listitem>
+
 </itemizedlist>
 </para>