Typos in comments [ci skip]
[ghc.git] / compiler / typecheck / TcErrors.hs
index 48c0361..324391f 100644 (file)
@@ -12,8 +12,9 @@ module TcErrors(
 import TcRnTypes
 import TcRnMonad
 import TcMType
+import TcUnify( occCheckForErrors, OccCheckResult(..) )
 import TcType
-import RnEnv( unknownNameSuggestions )
+import RnUnbound ( unknownNameSuggestions )
 import Type
 import TyCoRep
 import Kind
@@ -27,11 +28,13 @@ import TyCon
 import Class
 import DataCon
 import TcEvidence
+import HsExpr  ( UnboundVar(..) )
 import HsBinds ( PatSynBind(..) )
 import Name
-import RdrName ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual )
-import PrelNames ( typeableClassName, hasKey, ptrRepLiftedDataConKey
-                 , ptrRepUnliftedDataConKey )
+import RdrName ( lookupGlobalRdrEnv, lookupGRE_Name, GlobalRdrEnv
+               , mkRdrUnqual, isLocalGRE, greSrcSpan, pprNameProvenance
+               , GlobalRdrElt (..), globalRdrEnvElts )
+import PrelNames ( typeableClassName, hasKey, liftedRepDataConKey )
 import Id
 import Var
 import VarSet
@@ -40,19 +43,22 @@ import NameSet
 import Bag
 import ErrUtils         ( ErrMsg, errDoc, pprLocErrMsg )
 import BasicTypes
-import ConLike          ( ConLike(..) )
+import ConLike          ( ConLike(..), conLikeWrapId_maybe )
 import Util
+import HscTypes (HscEnv, lookupTypeHscEnv, TypeEnv, lookupTypeEnv )
+import NameEnv (lookupNameEnv)
 import FastString
 import Outputable
 import SrcLoc
 import DynFlags
-import StaticFlags      ( opt_PprStyle_Debug )
 import ListSetOps       ( equivClasses )
 import Maybes
 import qualified GHC.LanguageExtensions as LangExt
+import FV ( fvVarList, unionFV )
 
 import Control.Monad    ( when )
-import Data.List        ( partition, mapAccumL, nub, sortBy )
+import Data.List        ( partition, mapAccumL, nub, sortBy, unfoldr )
+import qualified Data.Set as Set
 
 #if __GLASGOW_HASKELL__ > 710
 import Data.Semigroup   ( Semigroup )
@@ -132,8 +138,17 @@ reportUnsolved wanted
                         | warn_partial_sigs = HoleWarn
                         | otherwise         = HoleDefer
 
-       ; report_unsolved (Just binds_var) False type_errors expr_holes type_holes wanted
-       ; getTcEvBinds binds_var }
+       ; defer_out_of_scope <- goptM Opt_DeferOutOfScopeVariables
+       ; warn_out_of_scope <- woptM Opt_WarnDeferredOutOfScopeVariables
+       ; let out_of_scope_holes | not defer_out_of_scope = HoleError
+                                | warn_out_of_scope      = HoleWarn
+                                | otherwise              = HoleDefer
+
+       ; report_unsolved binds_var False type_errors expr_holes
+          type_holes out_of_scope_holes wanted
+
+       ; ev_binds <- getTcEvBindsMap binds_var
+       ; return (evBindMapBinds ev_binds)}
 
 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
 -- However, do not make any evidence bindings, because we don't
@@ -144,23 +159,29 @@ reportUnsolved wanted
 -- and for simplifyDefault.
 reportAllUnsolved :: WantedConstraints -> TcM ()
 reportAllUnsolved wanted
-  = report_unsolved Nothing False TypeError HoleError HoleError wanted
+  = do { ev_binds <- newTcEvBinds
+       ; report_unsolved ev_binds False TypeError
+                         HoleError HoleError HoleError wanted }
 
 -- | Report all unsolved goals as warnings (but without deferring any errors to
 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
 -- TcSimplify
 warnAllUnsolved :: WantedConstraints -> TcM ()
 warnAllUnsolved wanted
-  = report_unsolved Nothing True TypeWarn HoleWarn HoleWarn wanted
+  = do { ev_binds <- newTcEvBinds
+       ; report_unsolved ev_binds True TypeWarn
+                         HoleWarn HoleWarn HoleWarn wanted }
 
 -- | Report unsolved goals as errors or warnings.
-report_unsolved :: Maybe EvBindsVar  -- cec_binds
+report_unsolved :: EvBindsVar        -- cec_binds
                 -> Bool              -- Errors as warnings
                 -> TypeErrorChoice   -- Deferred type errors
                 -> HoleChoice        -- Expression holes
                 -> HoleChoice        -- Type holes
+                -> HoleChoice        -- Out of scope holes
                 -> WantedConstraints -> TcM ()
-report_unsolved mb_binds_var err_as_warn type_errors expr_holes type_holes wanted
+report_unsolved mb_binds_var err_as_warn type_errors expr_holes
+    type_holes out_of_scope_holes wanted
   | isEmptyWC wanted
   = return ()
   | otherwise
@@ -171,11 +192,11 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes type_holes wante
             -- If we are deferring we are going to need /all/ evidence around,
             -- including the evidence produced by unflattening (zonkWC)
        ; let tidy_env = tidyFreeTyCoVars env0 free_tvs
-             free_tvs = tyCoVarsOfWC wanted
+             free_tvs = tyCoVarsOfWCList wanted
 
-       ; traceTc "reportUnsolved (after zonking and tidying):" $
-         vcat [ pprTvBndrs (varSetElems free_tvs)
-              , ppr wanted ]
+       ; traceTc "reportUnsolved (after zonking):" $
+         vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
+              , text "Wanted:" <+> ppr wanted ]
 
        ; warn_redundant <- woptM Opt_WarnRedundantConstraints
        ; let err_ctxt = CEC { cec_encl  = []
@@ -184,6 +205,7 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes type_holes wante
                             , cec_errors_as_warns = err_as_warn
                             , cec_expr_holes = expr_holes
                             , cec_type_holes = type_holes
+                            , cec_out_of_scope_holes = out_of_scope_holes
                             , cec_suppress = False -- See Note [Suppressing error messages]
                             , cec_warn_redundant = warn_redundant
                             , cec_binds    = mb_binds_var }
@@ -200,8 +222,17 @@ report_unsolved mb_binds_var err_as_warn type_errors expr_holes type_holes wante
 data Report
   = Report { report_important :: [SDoc]
            , report_relevant_bindings :: [SDoc]
+           , report_valid_substitutions :: [SDoc]
            }
 
+instance Outputable Report where   -- Debugging only
+  ppr (Report { report_important = imp
+              , report_relevant_bindings = rel
+              , report_valid_substitutions = val })
+    = vcat [ text "important:" <+> vcat imp
+           , text "relevant:"  <+> vcat rel
+           , text "valid:"  <+> vcat val ]
+
 {- Note [Error report]
 The idea is that error msgs are divided into three parts: the main msg, the
 context block (\"In the second argument of ...\"), and the relevant bindings
@@ -217,12 +248,13 @@ multiple places so they have to be in the Report.
 
 #if __GLASGOW_HASKELL__ > 710
 instance Semigroup Report where
-    Report a1 b1 <> Report a2 b2 = Report (a1 ++ a2) (b1 ++ b2)
+    Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
 #endif
 
 instance Monoid Report where
-    mempty = Report [] []
-    mappend (Report a1 b1) (Report a2 b2) = Report (a1 ++ a2) (b1 ++ b2)
+    mempty = Report [] [] []
+    mappend (Report a1 b1 c1) (Report a2 b2 c2)
+      = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
 
 -- | Put a doc into the important msgs block.
 important :: SDoc -> Report
@@ -232,6 +264,10 @@ important doc = mempty { report_important = [doc] }
 relevant_bindings :: SDoc -> Report
 relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
 
+-- | Put a doc into the valid substitutions block.
+valid_substitutions :: SDoc -> Report
+valid_substitutions docs = mempty { report_valid_substitutions = [docs] }
+
 data TypeErrorChoice   -- What to do for type errors found by the type checker
   = TypeError     -- A type error aborts compilation with an error message
   | TypeWarn      -- A type error is deferred to runtime, plus a compile-time warning
@@ -242,30 +278,39 @@ data HoleChoice
   | HoleWarn      -- Defer to runtime, emit a compile-time warning
   | HoleDefer     -- Defer to runtime, no warning
 
+instance Outputable HoleChoice where
+  ppr HoleError = text "HoleError"
+  ppr HoleWarn  = text "HoleWarn"
+  ppr HoleDefer = text "HoleDefer"
+
+instance Outputable TypeErrorChoice  where
+  ppr TypeError = text "TypeError"
+  ppr TypeWarn  = text "TypeWarn"
+  ppr TypeDefer = text "TypeDefer"
+
 data ReportErrCtxt
     = CEC { cec_encl :: [Implication]  -- Enclosing implications
                                        --   (innermost first)
                                        -- ic_skols and givens are tidied, rest are not
           , cec_tidy  :: TidyEnv
 
-          , cec_binds :: Maybe EvBindsVar
-                         -- Nothing <=> Report all errors, including holes
-                         --             Do not add any evidence bindings, because
-                         --             we have no convenient place to put them
-                         --             See TcErrors.reportAllUnsolved
-                         -- Just ev <=> make some errors (depending on cec_defer)
-                         --             into warnings, and emit evidence bindings
-                         --             into 'ev' for unsolved constraints
+          , cec_binds :: EvBindsVar    -- Make some errors (depending on cec_defer)
+                                       -- into warnings, and emit evidence bindings
+                                       -- into 'cec_binds' for unsolved constraints
 
           , cec_errors_as_warns :: Bool   -- Turn all errors into warnings
                                           -- (except for Holes, which are
                                           -- controlled by cec_type_holes and
                                           -- cec_expr_holes)
           , cec_defer_type_errors :: TypeErrorChoice -- Defer type errors until runtime
-                                                     -- Irrelevant if cec_binds = Nothing
 
-          , cec_expr_holes :: HoleChoice  -- Holes in expressions
-          , cec_type_holes :: HoleChoice  -- Holes in types
+          -- cec_expr_holes is a union of:
+          --   cec_type_holes - a set of typed holes: '_', '_a', '_foo'
+          --   cec_out_of_scope_holes - a set of variables which are
+          --                            out of scope: 'x', 'y', 'bar'
+          , cec_expr_holes :: HoleChoice           -- Holes in expressions
+          , cec_type_holes :: HoleChoice           -- Holes in types
+          , cec_out_of_scope_holes :: HoleChoice   -- Out of scope holes
 
           , cec_warn_redundant :: Bool    -- True <=> -Wredundant-constraints
 
@@ -275,6 +320,25 @@ data ReportErrCtxt
                                     -- See Note [Suppressing error messages]
       }
 
+instance Outputable ReportErrCtxt where
+  ppr (CEC { cec_binds              = bvar
+           , cec_errors_as_warns    = ew
+           , cec_defer_type_errors  = dte
+           , cec_expr_holes         = eh
+           , cec_type_holes         = th
+           , cec_out_of_scope_holes = osh
+           , cec_warn_redundant     = wr
+           , cec_suppress           = sup })
+    = text "CEC" <+> braces (vcat
+         [ text "cec_binds"              <+> equals <+> ppr bvar
+         , text "cec_errors_as_warns"    <+> equals <+> ppr ew
+         , text "cec_defer_type_errors"  <+> equals <+> ppr dte
+         , text "cec_expr_holes"         <+> equals <+> ppr eh
+         , text "cec_type_holes"         <+> equals <+> ppr th
+         , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
+         , text "cec_warn_redundant"     <+> equals <+> ppr wr
+         , text "cec_suppress"           <+> equals <+> ppr sup ])
+
 {-
 Note [Suppressing error messages]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -291,7 +355,7 @@ Specifically (see reportWanteds)
 
 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
 reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
-                                 , ic_wanted = wanted, ic_binds = m_evb
+                                 , ic_wanted = wanted, ic_binds = evb
                                  , ic_status = status, ic_info = info
                                  , ic_env = tcl_env, ic_tclvl = tc_lvl })
   | BracketSkol <- info
@@ -302,8 +366,8 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                      -- certainly be un-satisfied constraints
 
   | otherwise
-  = do { reportWanteds ctxt' tc_lvl wanted
-       ; traceTc "reportImplic" (ppr implic)
+  = do { traceTc "reportImplic" (ppr implic')
+       ; reportWanteds ctxt' tc_lvl wanted
        ; when (cec_warn_redundant ctxt) $
          warnRedundantConstraints ctxt' tcl_env info' dead_givens }
   where
@@ -322,17 +386,14 @@ reportImplic ctxt implic@(Implic { ic_skols = tvs, ic_given = given
                       -- tree rooted here, or we've come across
                       -- a suppress-worthy constraint higher up (Trac #11541)
 
-                 , cec_binds    = cec_binds ctxt *> m_evb }
-                      -- If cec_binds ctxt is Nothing, that means
-                      -- we're reporting *all* errors. Don't change
-                      -- that behavior just because we're going into
-                      -- an implication.
+                 , cec_binds    = evb }
 
     dead_givens = case status of
                     IC_Solved { ics_dead = dead } -> dead
                     _                             -> []
 
 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
+-- See Note [Tracking redundant constraints] in TcSimplify
 warnRedundantConstraints ctxt env info ev_vars
  | null redundant_evs
  = return ()
@@ -369,7 +430,7 @@ they can give rise to improvement.  Example (Trac #10100):
     instance Add Zero b b
     instance Add a b ab => Add (Succ a) b (Succ ab)
 The context (Add a b ab) for the instance is clearly unused in terms
-of evidence, since the dictionary has no feilds.  But it is still
+of evidence, since the dictionary has no fields.  But it is still
 needed!  With the context, a wanted constraint
    Add (Succ Zero) beta (Succ Zero)
 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
@@ -381,13 +442,14 @@ This only matters in instance declarations..
 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl = implics })
   = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
+                                       , text "Insols =" <+> ppr insols
                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)])
        ; 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)
-         -- These ones are not suppressed by the incoming context
+         -- 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
 
@@ -418,12 +480,12 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     -- type checking to get a Lint error later
     report1 = [ ("custom_error", is_user_type_error,
                                                   True, mkUserTypeErrorReporter)
-              , ("insoluble1",   is_given_eq,     True, mkGroupReporter mkEqErr)
+              , given_eq_spec
               , ("insoluble2",   utterly_wrong,   True, mkGroupReporter mkEqErr)
               , ("skolem eq1",   very_wrong,      True, mkSkolReporter)
               , ("skolem eq2",   skolem_eq,       True, mkSkolReporter)
               , ("non-tv eq",    non_tv_eq,       True, mkSkolReporter)
-              , ("Out of scope", is_out_of_scope, True,  mkHoleReporter)
+              , ("Out of scope", is_out_of_scope, True, mkHoleReporter)
               , ("Holes",        is_hole,         False, mkHoleReporter)
 
                   -- The only remaining equalities are alpha ~ ty,
@@ -460,12 +522,6 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
     non_tv_eq _ _                    = False
 
---    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_out_of_scope ct _ = isOutOfScopeCt ct
     is_hole         ct _ = isHoleCt ct
 
@@ -483,6 +539,22 @@ reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_insol = insols, wc_impl
     is_irred _ (IrredPred {}) = True
     is_irred _ _              = False
 
+    given_eq_spec = case find_gadt_match (cec_encl ctxt) of
+       Just imp -> ("insoluble1a", is_given_eq, True,  mkGivenErrorReporter imp)
+       Nothing  -> ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
+                  -- False means don't suppress subsequent errors
+                  -- Reason: we don't report all given errors
+                  --         (see mkGivenErrorReporter), and we should only suppress
+                  --         subsequent errors if we actually report this one!
+                  --         Trac #13446 is an example
+
+    find_gadt_match [] = Nothing
+    find_gadt_match (implic : implics)
+      | PatSkol {} <- ic_info implic
+      , not (ic_no_eqs implic)
+      = Just implic
+      | otherwise
+      = find_gadt_match implics
 
 ---------------
 isSkolemTy :: TcLevel -> Type -> Bool
@@ -525,21 +597,22 @@ mkSkolReporter ctxt cts
           (yeses, noes) = partition (group_with ct) cts
 
      group_with ct1 ct2
-       | EQ <- cmp_loc      ct1 ct2 = True
-       | EQ <- cmp_lhs_type ct1 ct2 = True
-       | otherwise                  = False
+       | EQ <- cmp_loc ct1 ct2 = True
+       | eq_lhs_type   ct1 ct2 = True
+       | otherwise             = False
 
 mkHoleReporter :: Reporter
 -- Reports errors one at a time
 mkHoleReporter ctxt
-  = mapM_ $ \ct ->
-    do { err <- mkHoleError ctxt ct
-       ; maybeReportHoleError ctxt ct err
-       ; maybeAddDeferredHoleBinding ctxt err ct }
+  = mapM_ $ \ct -> do { err <- mkHoleError ctxt ct
+                      ; maybeReportHoleError ctxt ct err
+                      ; maybeAddDeferredHoleBinding ctxt err ct }
 
 mkUserTypeErrorReporter :: Reporter
 mkUserTypeErrorReporter ctxt
-  = mapM_ $ \ct -> maybeReportError ctxt =<< mkUserTypeError ctxt ct
+  = mapM_ $ \ct -> do { err <- mkUserTypeError ctxt ct
+                      ; maybeReportError ctxt err
+                      ; addDeferredBinding ctxt err ct }
 
 mkUserTypeError :: ReportErrCtxt -> Ct -> TcM ErrMsg
 mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
@@ -550,6 +623,71 @@ mkUserTypeError ctxt ct = mkErrorMsgFromCt ctxt ct
                             Nothing  -> pprPanic "mkUserTypeError" (ppr ct)
 
 
+mkGivenErrorReporter :: Implication -> Reporter
+-- See Note [Given errors]
+mkGivenErrorReporter implic ctxt cts
+  = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
+       ; dflags <- getDynFlags
+       ; let ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
+                   -- For given constraints we overwrite the env (and hence src-loc)
+                  -- with one from the implication.  See Note [Inaccessible code]
+
+             inaccessible_msg = hang (text "Inaccessible code in")
+                                   2 (ppr (ic_info implic))
+             report = important inaccessible_msg `mappend`
+                      relevant_bindings binds_msg
+
+       ; err <- mkEqErr_help dflags ctxt report ct'
+                             Nothing ty1 ty2
+
+       ; traceTc "mkGivenErrorRporter" (ppr ct)
+       ; maybeReportError ctxt err }
+  where
+    (ct : _ )  = cts    -- Never empty
+    (ty1, ty2) = getEqPredTys (ctPred ct)
+
+ignoreErrorReporter :: Reporter
+-- Discard Given errors that don't come from
+-- a pattern match; maybe we should warn instead?ignoreErrorReporter ctxt cts
+ignoreErrorReporter ctxt cts
+  = do { traceTc "mkGivenErrorRporter no" (ppr cts $$ ppr (cec_encl ctxt))
+       ; return () }
+
+
+{- Note [Given errors]
+~~~~~~~~~~~~~~~~~~~~~~
+Given constraints represent things for which we have (or will have)
+evidence, so they aren't errors.  But if a Given constraint is
+insoluble, this code is inaccessible, and we might want to at least
+warn about that.  A classic case is
+
+   data T a where
+     T1 :: T Int
+     T2 :: T a
+     T3 :: T Bool
+
+   f :: T Int -> Bool
+   f T1 = ...
+   f T2 = ...
+   f T3 = ...  -- We want to report this case as inaccessible
+
+We'd like to point out that the T3 match is inaccessible. It
+will have a Given constraint [G] Int ~ Bool.
+
+But we don't want to report ALL insoluble Given constraints.  See Trac
+#12466 for a long discussion on.  For example, if we aren't careful
+we'll complain about
+   f :: ((Int ~ Bool) => a -> a) -> Int
+which arguably is OK.  It's more debatable for
+   g :: (Int ~ Bool) => Int -> Int
+but it's tricky to distinguish these cases to we don't report
+either.
+
+The bottom line is this: find_gadt_match looks for an encosing
+pattern match which binds some equality constraints.  If we
+find one, we report the insoluble Given.
+-}
+
 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
                              -- Make error message for a group
                 -> Reporter  -- Deal with lots of constraints
@@ -557,13 +695,12 @@ mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg)
 -- and report only the first (to avoid a cascade)
 mkGroupReporter mk_err ctxt cts
   = mapM_ (reportGroup mk_err ctxt) (equivClasses cmp_loc cts)
-  where
 
-cmp_lhs_type :: Ct -> Ct -> Ordering
-cmp_lhs_type ct1 ct2
+eq_lhs_type :: Ct -> Ct -> Bool
+eq_lhs_type ct1 ct2
   = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
        (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
-         (eq_rel1 `compare` eq_rel2) `thenCmp` (ty1 `cmpType` ty2)
+         (eq_rel1 == eq_rel2) && (ty1 `eqType` ty2)
        _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
 
 cmp_loc :: Ct -> Ct -> Ordering
@@ -574,16 +711,20 @@ reportGroup :: (ReportErrCtxt -> [Ct] -> TcM ErrMsg) -> ReportErrCtxt
 reportGroup mk_err ctxt cts =
   case partition isMonadFailInstanceMissing cts of
         -- Only warn about missing MonadFail constraint when
-        -- there are no other missing contstraints!
+        -- there are no other missing constraints!
         (monadFailCts, []) ->
             do { err <- mk_err ctxt monadFailCts
                ; reportWarning (Reason Opt_WarnMissingMonadFailInstances) err }
 
         (_, cts') -> do { err <- mk_err ctxt cts'
                         ; maybeReportError ctxt err
-                        ; mapM_ (maybeAddDeferredBinding ctxt err) cts' }
-                                -- Add deferred bindings for all
-                                -- But see Note [Always warn with -fdefer-type-errors]
+                            -- But see Note [Always warn with -fdefer-type-errors]
+                        ; traceTc "reportGroup" (ppr cts')
+                        ; mapM_ (addDeferredBinding ctxt err) cts' }
+                            -- Add deferred bindings for all
+                            -- Redundant if we are going to abort compilation,
+                            -- but that's hard to know for sure, and if we don't
+                            -- abort, we need bindings for all (e.g. Trac #12156)
   where
     isMonadFailInstanceMissing ct =
         case ctLocOrigin (ctLoc ct) of
@@ -604,9 +745,22 @@ maybeReportHoleError ctxt ct err
        HoleWarn  -> reportWarning (Reason Opt_WarnPartialTypeSignatures) err
        HoleDefer -> return ()
 
-  -- Otherwise this is a typed hole in an expression
+  -- Always report an error for out-of-scope variables
+  -- Unless -fdefer-out-of-scope-variables is on,
+  -- in which case the messages are discarded.
+  -- See Trac #12170, #12406
+  | isOutOfScopeCt ct
+  = -- If deferring, report a warning only if -Wout-of-scope-variables is on
+    case cec_out_of_scope_holes ctxt of
+      HoleError -> reportError err
+      HoleWarn  ->
+        reportWarning (Reason Opt_WarnDeferredOutOfScopeVariables) err
+      HoleDefer -> return ()
+
+  -- Otherwise this is a typed hole in an expression,
+  -- but not for an out-of-scope variable
   | otherwise
-  = -- If deferring, report a warning only if -Wtyped-holds is on
+  = -- If deferring, report a warning only if -Wtyped-holes is on
     case cec_expr_holes ctxt of
        HoleError -> reportError err
        HoleWarn  -> reportWarning (Reason Opt_WarnTypedHoles) err
@@ -632,12 +786,12 @@ addDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
 addDeferredBinding ctxt err ct
   | CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
     -- Only add deferred bindings for Wanted constraints
-  , Just ev_binds_var <- cec_binds ctxt  -- We have somewhere to put the bindings
   = do { dflags <- getDynFlags
        ; let err_msg = pprLocErrMsg err
              err_fs  = mkFastString $ showSDoc dflags $
                        err_msg $$ text "(deferred type error)"
              err_tm  = EvDelayedError pred err_fs
+             ev_binds_var = cec_binds ctxt
 
        ; case dest of
            EvVarDest evar
@@ -653,23 +807,10 @@ addDeferredBinding ctxt err ct
 
 maybeAddDeferredHoleBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
 maybeAddDeferredHoleBinding ctxt err ct
-    | isExprHoleCt ct
-    , case cec_expr_holes ctxt of
-        HoleDefer -> True
-        HoleWarn  -> True
-        HoleError -> False
-    = addDeferredBinding ctxt err ct  -- Only add bindings for holes in expressions
-    | otherwise                       -- not for holes in partial type signatures
-    = return ()
-
-maybeAddDeferredBinding :: ReportErrCtxt -> ErrMsg -> Ct -> TcM ()
-maybeAddDeferredBinding ctxt err ct =
-  case cec_defer_type_errors ctxt of
-        TypeDefer -> deferred
-        TypeWarn -> deferred
-        TypeError -> return ()
-  where
-    deferred = addDeferredBinding ctxt err ct
+  | isExprHoleCt ct
+  = addDeferredBinding ctxt err ct  -- Only add bindings for holes in expressions
+  | otherwise                       -- not for holes in partial type signatures
+  = return ()
 
 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
 -- Use the first reporter in the list whose predicate says True
@@ -692,9 +833,10 @@ tryReporters ctxt reporters cts
 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
 tryReporter ctxt (str, keep_me,  suppress_after, reporter) cts
   | null yeses = return (ctxt, cts)
-  | otherwise  = do { traceTc "tryReporter:" (text str <+> ppr yeses)
+  | otherwise  = do { traceTc "tryReporter" (text str <+> ppr yeses)
                     ; reporter ctxt yeses
                     ; let ctxt' = ctxt { cec_suppress = suppress_after || cec_suppress ctxt }
+                    ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
                     ; return (ctxt', nos) }
   where
     (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
@@ -736,22 +878,21 @@ mkErrorMsgFromCt ctxt ct report
   = mkErrorReport ctxt (ctLocEnv (ctLoc ct)) report
 
 mkErrorReport :: ReportErrCtxt -> TcLclEnv -> Report -> TcM ErrMsg
-mkErrorReport ctxt tcl_env (Report important relevant_bindings)
+mkErrorReport ctxt tcl_env (Report important relevant_bindings valid_subs)
   = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
        ; mkErrDocAt (RealSrcSpan (tcl_loc tcl_env))
-            (errDoc important [context] relevant_bindings)
+            (errDoc important [context] (relevant_bindings ++ valid_subs))
        }
 
-type UserGiven = ([EvVar], SkolemInfo, Bool, RealSrcSpan)
+type UserGiven = Implication
 
 getUserGivens :: ReportErrCtxt -> [UserGiven]
 -- One item for each enclosing implication
-getUserGivens (CEC {cec_encl = ctxt})
-  = reverse $
-    [ (givens, info, no_eqs, tcl_loc env)
-    | Implic { ic_given = givens, ic_env = env
-             , ic_no_eqs = no_eqs, ic_info = info } <- ctxt
-    , not (null givens) ]
+getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
+
+getUserGivensFromImplics :: [Implication] -> [UserGiven]
+getUserGivensFromImplics implics
+  = reverse (filterOut (null . ic_given) implics)
 
 {-
 Note [Always warn with -fdefer-type-errors]
@@ -850,45 +991,99 @@ mkIrredErr ctxt cts
 
 ----------------
 mkHoleError :: ReportErrCtxt -> Ct -> TcM ErrMsg
-mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
-  | isOutOfScopeCt ct  -- Out of scope variables, like 'a', where 'a' isn't bound
-                       -- Suggest possible in-scope variables in the message
-  = do { dflags  <- getDynFlags
-       ; rdr_env <- getGlobalRdrEnv
-       ; impInfo <- getImports
-       ; mkErrDocAt (RealSrcSpan (tcl_loc lcl_env)) $
-                    errDoc [out_of_scope_msg] []
-                           [unknownNameSuggestions dflags rdr_env
-                            (tcl_rdr lcl_env) impInfo (mkRdrUnqual occ)] }
-
-  | otherwise  -- Explicit holes, like "_" or "_f"
-  = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
-               -- The 'False' means "don't filter the bindings"; see Trac #8191
-       ; mkErrorMsgFromCt ctxt ct $
-            important hole_msg `mappend` relevant_bindings binds_msg }
+mkHoleError _ctxt ct@(CHoleCan { cc_hole = ExprHole (OutOfScope occ rdr_env0) })
+  -- Out-of-scope variables, like 'a', where 'a' isn't bound; suggest possible
+  -- in-scope variables in the message, and note inaccessible exact matches
+  = do { dflags   <- getDynFlags
+       ; imp_info <- getImports
+       ; let suggs_msg = unknownNameSuggestions dflags rdr_env0
+                                                (tcl_rdr lcl_env) imp_info rdr
+       ; rdr_env     <- getGlobalRdrEnv
+       ; splice_locs <- getTopLevelSpliceLocs
+       ; let match_msgs = mk_match_msgs rdr_env splice_locs
+       ; mkErrDocAt (RealSrcSpan err_loc) $
+                    errDoc [out_of_scope_msg] [] (match_msgs ++ [suggs_msg]) }
 
   where
+    rdr         = mkRdrUnqual occ
     ct_loc      = ctLoc ct
     lcl_env     = ctLocEnv ct_loc
+    err_loc     = tcl_loc lcl_env
     hole_ty     = ctEvPred (ctEvidence ct)
-    tyvars      = tyCoVarsOfTypeList hole_ty
     boring_type = isTyVarTy hole_ty
 
     out_of_scope_msg -- Print v :: ty only if the type has structure
       | boring_type = hang herald 2 (ppr occ)
-      | otherwise   = hang herald 2 pp_with_type
+      | otherwise   = hang herald 2 (pp_with_type occ hole_ty)
 
-    pp_with_type = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
     herald | isDataOcc occ = text "Data constructor not in scope:"
            | otherwise     = text "Variable not in scope:"
 
-    hole_msg = case hole_sort of
-      ExprHole -> vcat [ hang (text "Found hole:")
-                            2 pp_with_type
-                       , tyvars_msg, expr_hole_hint ]
-      TypeHole -> vcat [ hang (text "Found type wildcard" <+> quotes (ppr occ))
-                            2 (text "standing for" <+> quotes (pprType hole_ty))
-                       , tyvars_msg, type_hole_hint ]
+    -- Indicate if the out-of-scope variable exactly (and unambiguously) matches
+    -- a top-level binding in a later inter-splice group; see Note [OutOfScope
+    -- exact matches]
+    mk_match_msgs rdr_env splice_locs
+      = let gres = filter isLocalGRE (lookupGlobalRdrEnv rdr_env occ)
+        in case gres of
+             [gre]
+               |  RealSrcSpan bind_loc <- greSrcSpan gre
+                  -- Find splice between the unbound variable and the match; use
+                  -- lookupLE, not lookupLT, since match could be in the splice
+               ,  Just th_loc <- Set.lookupLE bind_loc splice_locs
+               ,  err_loc < th_loc
+               -> [mk_bind_scope_msg bind_loc th_loc]
+             _ -> []
+
+    mk_bind_scope_msg bind_loc th_loc
+      | is_th_bind
+      = hang (quotes (ppr occ) <+> parens (text "splice on" <+> th_rng))
+           2 (text "is not in scope before line" <+> int th_start_ln)
+      | otherwise
+      = hang (quotes (ppr occ) <+> bind_rng <+> text "is not in scope")
+           2 (text "before the splice on" <+> th_rng)
+      where
+        bind_rng = parens (text "line" <+> int bind_ln)
+        th_rng
+          | th_start_ln == th_end_ln = single
+          | otherwise                = multi
+        single = text "line"  <+> int th_start_ln
+        multi  = text "lines" <+> int th_start_ln <> text "-" <> int th_end_ln
+        bind_ln     = srcSpanStartLine bind_loc
+        th_start_ln = srcSpanStartLine th_loc
+        th_end_ln   = srcSpanEndLine   th_loc
+        is_th_bind = th_loc `containsSpan` bind_loc
+
+mkHoleError ctxt ct@(CHoleCan { cc_hole = hole })
+  -- Explicit holes, like "_" or "_f"
+  = do { (ctxt, binds_msg, ct) <- relevantBindings False ctxt ct
+               -- The 'False' means "don't filter the bindings"; see Trac #8191
+
+       ; show_hole_constraints <- goptM Opt_ShowHoleConstraints
+       ; let constraints_msg
+               | isExprHoleCt ct, show_hole_constraints
+                  = givenConstraintsMsg ctxt
+               | otherwise = empty
+
+       ; sub_msg <-  validSubstitutions ct
+       ; mkErrorMsgFromCt ctxt ct $
+            important hole_msg `mappend`
+            relevant_bindings (binds_msg $$ constraints_msg) `mappend`
+            valid_substitutions sub_msg}
+
+  where
+    occ     = holeOcc hole
+    hole_ty = ctEvPred (ctEvidence ct)
+    tyvars  = tyCoVarsOfTypeList hole_ty
+
+    hole_msg = case hole of
+      ExprHole {} -> vcat [ hang (text "Found hole:")
+                               2 (pp_with_type occ hole_ty)
+                          , tyvars_msg, expr_hole_hint ]
+      TypeHole {} -> vcat [ hang (text "Found type wildcard" <+>
+                                  quotes (ppr occ))
+                               2 (text "standing for" <+>
+                                  quotes (pprType hole_ty))
+                          , tyvars_msg, type_hole_hint ]
 
     tyvars_msg = ppUnless (null tyvars) $
                  text "Where:" <+> vcat (map loc_msg tyvars)
@@ -909,9 +1104,8 @@ mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
     loc_msg tv
        | isTyVar tv
        = case tcTyVarDetails tv of
-          SkolemTv {} -> pprSkol (cec_encl ctxt) tv
-          MetaTv {}   -> quotes (ppr tv) <+> text "is an ambiguous type variable"
-          det -> pprTcTyVarDetails det
+           MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
+           _         -> extraTyVarInfo ctxt tv
        | otherwise
        = sdocWithDynFlags $ \dflags ->
          if gopt Opt_PrintExplicitCoercions dflags
@@ -920,6 +1114,118 @@ mkHoleError ctxt ct@(CHoleCan { cc_occ = occ, cc_hole = hole_sort })
 
 mkHoleError _ ct = pprPanic "mkHoleError" (ppr ct)
 
+
+-- See Note [Valid substitutions include ...]
+validSubstitutions :: Ct -> TcM SDoc
+validSubstitutions ct | isExprHoleCt ct =
+  do { top_env <- getTopEnv
+     ; rdr_env <- getGlobalRdrEnv
+     ; gbl_env <- tcg_type_env <$> getGblEnv
+     ; lcl_env <- getLclTypeEnv
+     ; dflags <- getDynFlags
+     ; (discards, substitutions) <-
+        go (gbl_env, lcl_env, top_env) (maxValidSubstitutions dflags)
+         $ localsFirst $ globalRdrEnvElts rdr_env
+     ; return $ ppUnless (null substitutions) $
+                 hang (text "Valid substitutions include")
+                  2 (vcat (map (ppr_sub rdr_env) substitutions)
+                    $$ ppWhen discards subsDiscardMsg) }
+  where
+    hole_ty :: TcPredType
+    hole_ty = ctEvPred (ctEvidence ct)
+
+    hole_env = ctLocEnv $ ctEvLoc $ ctEvidence ct
+
+    localsFirst :: [GlobalRdrElt] -> [GlobalRdrElt]
+    localsFirst elts = lcl ++ gbl
+      where (lcl, gbl) = partition gre_lcl elts
+
+    getBndrOcc :: TcIdBinder -> OccName
+    getBndrOcc (TcIdBndr id _) = occName $ getName id
+    getBndrOcc (TcIdBndr_ExpType name _ _) = occName $ getName name
+
+    relBindSet =  mkOccSet $ map getBndrOcc $ tcl_bndrs hole_env
+
+    shouldBeSkipped :: GlobalRdrElt -> Bool
+    shouldBeSkipped el = (occName $ gre_name el) `elemOccSet` relBindSet
+
+    ppr_sub :: GlobalRdrEnv -> Id -> SDoc
+    ppr_sub rdr_env id = case lookupGRE_Name rdr_env (idName id) of
+        Just elt -> sep [ idAndTy, nest 2 (parens $ pprNameProvenance elt)]
+        _ -> idAndTy
+      where name = idName id
+            ty = varType id
+            idAndTy = (pprPrefixOcc name <+> dcolon <+> pprType ty)
+
+    tyToId :: TyThing -> Maybe Id
+    tyToId (AnId i) = Just i
+    tyToId (AConLike c) = conLikeWrapId_maybe c
+    tyToId _ = Nothing
+
+    tcTyToId :: TcTyThing -> Maybe Id
+    tcTyToId (AGlobal id) = tyToId id
+    tcTyToId (ATcId id _) = Just id
+    tcTyToId _ = Nothing
+
+    substituteable :: Id -> Bool
+    substituteable = tcEqType hole_ty . varType
+
+    lookupTopId :: HscEnv -> Name -> IO (Maybe Id)
+    lookupTopId env name =
+        maybe Nothing tyToId <$> lookupTypeHscEnv env name
+
+    lookupGblId :: TypeEnv -> Name -> Maybe Id
+    lookupGblId env name = maybe Nothing tyToId $ lookupTypeEnv env name
+
+    lookupLclId :: TcTypeEnv -> Name -> Maybe Id
+    lookupLclId env name = maybe Nothing tcTyToId $ lookupNameEnv env name
+
+    go ::  (TypeEnv, TcTypeEnv, HscEnv) -> Maybe Int -> [GlobalRdrElt]
+       -> TcM (Bool, [Id])
+    go = go_ []
+
+    go_ ::  [Id] -> (TypeEnv, TcTypeEnv, HscEnv) -> Maybe Int -> [GlobalRdrElt]
+         -> TcM (Bool, [Id])
+    go_ subs _ _ [] = return (False, reverse subs)
+    go_ subs _ (Just 0) _ = return (True, reverse subs)
+    go_ subs envs@(gbl,lcl,top) maxleft (el:elts) =
+       if shouldBeSkipped el then discard_it
+         else do { maybeId <- liftIO lookupId
+                 ; case maybeId of
+                     Just id | substituteable id ->
+                       go_ (id:subs) envs ((\n -> n - 1) <$> maxleft) elts
+                     _ -> discard_it }
+      where name = gre_name el
+            discard_it = go_ subs envs maxleft elts
+            getTopId = lookupTopId top name
+            gbl_id = lookupGblId gbl name
+            lcl_id = lookupLclId lcl name
+            lookupId = if (isJust lcl_id) then return lcl_id
+                       else if (isJust gbl_id) then return gbl_id else getTopId
+
+
+validSubstitutions _ = return empty
+
+
+-- See Note [Constraints include ...]
+givenConstraintsMsg :: ReportErrCtxt -> SDoc
+givenConstraintsMsg ctxt =
+    let constraints :: [(Type, RealSrcSpan)]
+        constraints =
+          do { Implic{ ic_given = given, ic_env = env } <- cec_encl ctxt
+             ; constraint <- given
+             ; return (varType constraint, tcl_loc env) }
+
+        pprConstraint (constraint, loc) =
+          ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
+
+    in ppUnless (null constraints) $
+         hang (text "Constraints include")
+            2 (vcat $ map pprConstraint constraints)
+
+pp_with_type :: OccName -> Type -> SDoc
+pp_with_type occ ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType ty)
+
 ----------------
 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM ErrMsg
 mkIPErr ctxt cts
@@ -930,7 +1236,7 @@ mkIPErr ctxt cts
              msg | null givens
                  = addArising orig $
                    sep [ text "Unbound implicit parameter" <> plural cts
-                       , nest 2 (pprTheta preds) ]
+                       , nest 2 (pprParendTheta preds) ]
                  | otherwise
                  = couldNotDeduce givens (preds, orig)
 
@@ -940,6 +1246,168 @@ mkIPErr ctxt cts
     (ct1:_) = cts
 
 {-
+Note [Valid substitutions include ...]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+`validSubstitutions` returns the "Valid substitutions include ..." message.
+For example, look at the following definitions in a file called test.hs:
+
+    ps :: String -> IO ()
+    ps = putStrLn
+
+    ps2 :: a -> IO ()
+    ps2 _ = putStrLn "hello, world"
+
+    main :: IO ()
+    main = _ "hello, world"
+
+The hole in `main` would generate the message:
+
+    Valid substitutions include
+      ps :: String -> IO () ((defined at test.hs:2:1)
+      putStrLn :: String -> IO ()
+        (imported from ‘Prelude’ at test.hs:1:1
+         (and originally defined in ‘System.IO’))
+      putStr :: String -> IO ()
+        (imported from ‘Prelude’ at test.hs:1:1
+         (and originally defined in ‘System.IO’))
+
+Valid substitutions are found by checking names in scope.
+
+Currently the implementation only looks at exact type matches, as given by
+`tcEqType`, so we DO NOT report `ps2` as a valid substitution in the example,
+even though it fits in the hole. To determine that `ps2` fits in the hole,
+we would need to check ids for subsumption, i.e. that the type of the hole is
+a subtype of the id. This can be done using `tcSubType` from `TcUnify` and
+`tcCheckSatisfiability` in `TcSimplify`.  Unfortunately, `TcSimplify` uses
+`TcErrors` to report errors found during constraint checking, so checking for
+subsumption in holes would involve shuffling some code around in `TcSimplify`,
+to make a non-error reporting constraint satisfiability checker which could
+then be used for checking whether a given id satisfies the constraints imposed
+by the hole.
+
+Note [Constraints include ...]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
+-fshow-hole-constraints. For example, the following hole:
+
+    foo :: (Eq a, Show a) => a -> String
+    foo x = _
+
+would generate the message:
+
+    Constraints include
+      Eq a (from foo.hs:1:1-36)
+      Show a (from foo.hs:1:1-36)
+
+Constraints are displayed in order from innermost (closest to the hole) to
+outermost. There's currently no filtering or elimination of duplicates.
+
+
+Note [OutOfScope exact matches]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When constructing an out-of-scope error message, we not only generate a list of
+possible in-scope alternatives but also search for an exact, unambiguous match
+in a later inter-splice group.  If we find such a match, we report its presence
+(and indirectly, its scope) in the message.  For example, if a module A contains
+the following declarations,
+
+   foo :: Int
+   foo = x
+
+   $(return [])  -- Empty top-level splice
+
+   x :: Int
+   x = 23
+
+we will issue an error similar to
+
+   A.hs:6:7: error:
+       • Variable not in scope: x :: Int
+       • ‘x’ (line 11) is not in scope before the splice on line 8
+
+By providing information about the match, we hope to clarify why declaring a
+variable after a top-level splice but using it before the splice generates an
+out-of-scope error (a situation which is often confusing to Haskell newcomers).
+
+Note that if we find multiple exact matches to the out-of-scope variable
+(hereafter referred to as x), we report nothing.  Such matches can only be
+duplicate record fields, as the presence of any other duplicate top-level
+declarations would have already halted compilation.  But if these record fields
+are declared in a later inter-splice group, then so too are their corresponding
+types.  Thus, these types must not occur in the inter-splice group containing x
+(any unknown types would have already been reported), and so the matches to the
+record fields are most likely coincidental.
+
+One oddity of the exact match portion of the error message is that we specify
+where the match to x is NOT in scope.  Why not simply state where the match IS
+in scope?  It most cases, this would be just as easy and perhaps a little
+clearer for the user.  But now consider the following example:
+
+    {-# LANGUAGE TemplateHaskell #-}
+
+    module A where
+
+    import Language.Haskell.TH
+    import Language.Haskell.TH.Syntax
+
+    foo = x
+
+    $(do -------------------------------------------------
+        ds <- [d| ok1 = x
+                |]
+        addTopDecls ds
+        return [])
+
+    bar = $(do
+            ds <- [d| x = 23
+                      ok2 = x
+                    |]
+            addTopDecls ds
+            litE $ stringL "hello")
+
+    $(return []) -----------------------------------------
+
+    ok3 = x
+
+Here, x is out-of-scope in the declaration of foo, and so we report
+
+    A.hs:8:7: error:
+        • Variable not in scope: x
+        • ‘x’ (line 16) is not in scope before the splice on lines 10-14
+
+If we instead reported where x IS in scope, we would have to state that it is in
+scope after the second top-level splice as well as among all the top-level
+declarations added by both calls to addTopDecls.  But doing so would not only
+add complexity to the code but also overwhelm the user with unneeded
+information.
+
+The logic which determines where x is not in scope is straightforward: it simply
+finds the last top-level splice which occurs after x but before (or at) the
+match to x (assuming such a splice exists).  In most cases, the check that the
+splice occurs after x acts only as a sanity check.  For example, when the match
+to x is a non-TH top-level declaration and a splice S occurs before the match,
+then x must precede S; otherwise, it would be in scope.  But when dealing with
+addTopDecls, this check serves a practical purpose.  Consider the following
+declarations:
+
+    $(do
+        ds <- [d| ok = x
+                  x = 23
+                |]
+        addTopDecls ds
+        return [])
+
+    foo = x
+
+In this case, x is not in scope in the declaration for foo.  Since x occurs
+AFTER the splice containing the match, the logic does not find any splices after
+x but before or at its match, and so we report nothing about x's scope.  If we
+had not checked whether x occurs before the splice, we would have instead
+reported that x is not in scope before the splice.  While correct, such an error
+message is more likely to confuse than to enlighten.
+-}
+
+{-
 ************************************************************************
 *                                                                      *
                 Equality errors
@@ -986,17 +1454,8 @@ mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
 mkEqErr _ [] = panic "mkEqErr"
 
 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM ErrMsg
-mkEqErr1 ctxt ct
-  | arisesFromGivens ct
-  = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
-       ; let (given_loc, given_msg) = mk_given (ctLoc ct) (cec_encl ctxt)
-       ; dflags <- getDynFlags
-       ; let report = important given_msg `mappend` relevant_bindings binds_msg
-       ; mkEqErr_help dflags ctxt report
-                      (setCtLoc ct given_loc) -- Note [Inaccessible code]
-                      Nothing ty1 ty2 }
-
-  | otherwise   -- Wanted or derived
+mkEqErr1 ctxt ct   -- Wanted or derived;
+                   -- givens handled in mkGivenErrorReporter
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; rdr_env <- getGlobalRdrEnv
        ; fam_envs <- tcGetFamInstEnvs
@@ -1007,7 +1466,7 @@ mkEqErr1 ctxt ct
                NomEq  -> empty
                ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
        ; dflags <- getDynFlags
-       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
+       ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct) $$ ppr keep_going)
        ; let report = mconcat [important wanted_msg, important coercible_msg,
                                relevant_bindings binds_msg]
        ; if keep_going
@@ -1016,14 +1475,6 @@ mkEqErr1 ctxt ct
   where
     (ty1, ty2) = getEqPredTys (ctPred ct)
 
-    mk_given :: CtLoc -> [Implication] -> (CtLoc, SDoc)
-    -- For given constraints we overwrite the env (and hence src-loc)
-    -- with one from the implication.  See Note [Inaccessible code]
-    mk_given loc []           = (loc, empty)
-    mk_given loc (implic : _) = (setCtLocEnv loc (ic_env implic)
-                                , hang (text "Inaccessible code in")
-                                     2 (ppr (ic_info implic)))
-
        -- If the types in the error message are the same as the types
        -- we are unifying, don't add the extra expected/actual message
     mk_wanted_extra :: CtLoc -> Bool -> (Bool, Maybe SwapFlag, SDoc)
@@ -1089,7 +1540,7 @@ mkCoercibleExplanation rdr_env fam_envs ty1 ty2
         | isNewTyCon tc
         , [data_con] <- tyConDataCons tc
         , let dc_name = dataConName data_con
-        , null (lookupGRE_Name rdr_env dc_name)
+        , isNothing (lookupGRE_Name rdr_env dc_name)
         = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
                     2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
                            , text "is not in scope" ])
@@ -1149,39 +1600,58 @@ reportEqErr :: ReportErrCtxt -> Report
             -> Maybe SwapFlag   -- Nothing <=> not sure
             -> TcType -> TcType -> TcM ErrMsg
 reportEqErr ctxt report ct oriented ty1 ty2
-  = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, eqInfo, report])
+  = mkErrorMsgFromCt ctxt ct (mconcat [misMatch, report, eqInfo])
   where misMatch = important $ misMatchOrCND ctxt ct oriented ty1 ty2
         eqInfo = important $ mkEqInfoMsg ct ty1 ty2
 
-mkTyVarEqErr :: DynFlags -> ReportErrCtxt -> Report -> Ct
+mkTyVarEqErr, mkTyVarEqErr'
+  :: DynFlags -> ReportErrCtxt -> Report -> Ct
              -> Maybe SwapFlag -> TcTyVar -> TcType -> TcM ErrMsg
 -- tv1 and ty2 are already tidied
 mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
-  | isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
+  = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
+       ; mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2 }
+
+mkTyVarEqErr' dflags ctxt report ct oriented tv1 ty2
+  | not insoluble_occurs_check   -- See Note [Occurs check wins]
+  , isUserSkolem ctxt tv1   -- ty2 won't be a meta-tyvar, or else the thing would
                             -- be oriented the other way round;
                             -- see TcCanonical.canEqTyVarTyVar
-  || isSigTyVar tv1 && not (isTyVarTy ty2)
-  || ctEqRel ct == ReprEq && not (isTyVarUnderDatatype tv1 ty2)
+    || isSigTyVar tv1 && not (isTyVarTy ty2)
+    || ctEqRel ct == ReprEq
      -- the cases below don't really apply to ReprEq (except occurs check)
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchOrCND ctxt ct oriented ty1 ty2
-        , important $ extraTyVarInfo ctxt tv1 ty2
+        , important $ extraTyVarEqInfo ctxt tv1 ty2
         , report
         ]
 
-  -- So tv is a meta tyvar (or started that way before we
-  -- generalised it).  So presumably it is an *untouchable*
-  -- meta tyvar or a SigTv, else it'd have been unified
   | OC_Occurs <- occ_check_expand
-  , ctEqRel ct == NomEq || isTyVarUnderDatatype tv1 ty2
-         -- See Note [Occurs check error] in TcCanonical
-  = do { let occCheckMsg = important $ addArising (ctOrigin ct) $
-                           hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
+    -- We report an "occurs check" even for  a ~ F t a, where F is a type
+    -- function; it's not insoluble (because in principle F could reduce)
+    -- but we have certainly been unable to solve it
+    -- See Note [Occurs check error] in TcCanonical
+  = do { let main_msg = addArising (ctOrigin ct) $
+                        hang (text "Occurs check: cannot construct the infinite" <+> what <> colon)
                               2 (sep [ppr ty1, char '~', ppr ty2])
+
              extra2 = important $ mkEqInfoMsg ct ty1 ty2
-       ; mkErrorMsgFromCt ctxt ct $ mconcat [occCheckMsg, extra2, report] }
 
-  | OC_Forall <- occ_check_expand
+             interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
+                                  filter isTyVar $
+                                  fvVarList $
+                                  tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
+             extra3 = relevant_bindings $
+                      ppWhen (not (null interesting_tyvars)) $
+                      hang (text "Type variable kinds:") 2 $
+                      vcat (map (tyvar_binding . tidyTyVarOcc (cec_tidy ctxt))
+                                interesting_tyvars)
+
+             tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
+       ; mkErrorMsgFromCt ctxt ct $
+         mconcat [important main_msg, extra2, extra3, report] }
+
+  | OC_Bad <- occ_check_expand
   = do { let msg = vcat [ text "Cannot instantiate unification variable"
                           <+> quotes (ppr tv1)
                         , hang (text "with a" <+> what <+> text "involving foralls:") 2 (ppr ty2)
@@ -1200,7 +1670,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
   , tv1 `elem` skols
   = mkErrorMsgFromCt ctxt ct $ mconcat
         [ important $ misMatchMsg ct oriented ty1 ty2
-        , important $ extraTyVarInfo ctxt tv1 ty2
+        , important $ extraTyVarEqInfo ctxt tv1 ty2
         , report
         ]
 
@@ -1228,11 +1698,14 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
        ; mkErrorMsgFromCt ctxt ct (mconcat [msg, tv_extra, report]) }
 
   -- Nastiest case: attempt to unify an untouchable variable
+  -- So tv is a meta tyvar (or started that way before we
+  -- generalised it).  So presumably it is an *untouchable*
+  -- meta tyvar or a SigTv, else it'd have been unified
   -- See Note [Error messages for untouchables]
   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
   , Implic { ic_env = env, ic_given = given
            , ic_tclvl = lvl, ic_info = skol_info } <- implic
-  = ASSERT2( isTcTyVar tv1 && not (isTouchableMetaTyVar lvl tv1)
+  = ASSERT2( not (isTouchableMetaTyVar lvl tv1)
            , ppr tv1 )  -- See Note [Error messages for untouchables]
     do { let msg = important $ misMatchMsg ct oriented ty1 ty2
              tclvl_extra = important $
@@ -1241,7 +1714,7 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
                       , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
                       , nest 2 $ text "bound by" <+> ppr skol_info
                       , nest 2 $ text "at" <+> ppr (tcl_loc env) ]
-             tv_extra = important $ extraTyVarInfo ctxt tv1 ty2
+             tv_extra = important $ extraTyVarEqInfo ctxt tv1 ty2
              add_sig  = important $ suggestAddSig ctxt ty1 ty2
        ; mkErrorMsgFromCt ctxt ct $ mconcat
             [msg, tclvl_extra, tv_extra, add_sig, report] }
@@ -1252,8 +1725,9 @@ mkTyVarEqErr dflags ctxt report ct oriented tv1 ty2
         -- Consider an ambiguous top-level constraint (a ~ F a)
         -- Not an occurs check, because F is a type function.
   where
-    occ_check_expand = occurCheckExpand dflags tv1 ty2
-    ty1    = mkTyVarTy tv1
+    ty1 = mkTyVarTy tv1
+    occ_check_expand       = occCheckForErrors dflags tv1 ty2
+    insoluble_occurs_check = isInsolubleOccursCheck (ctEqRel ct) tv1 ty2
 
     what = case ctLocTypeOrKind_maybe (ctLoc ct) of
       Just KindLevel -> text "kind"
@@ -1276,13 +1750,16 @@ mkEqInfoMsg ct ty1 ty2
               = snd (mkAmbigMsg False ct)
               | otherwise = empty
 
-    invis_msg | Just vis <- tcEqTypeVis ty1 ty2
-              , vis /= Visible
-              = sdocWithDynFlags $ \dflags ->
-                if gopt Opt_PrintExplicitKinds dflags
-                then text "Use -fprint-explicit-kinds to see the kind arguments"
-                else empty
+    -- better to check the exp/act types in the CtOrigin than the actual
+    -- mismatched types for suggestion about -fprint-explicit-kinds
+    (act_ty, exp_ty) = case ctOrigin ct of
+      TypeEqOrigin { uo_actual = act
+                   , uo_expected = exp } -> (act, exp)
+      _                                  -> (ty1, ty2)
 
+    invis_msg | Just vis <- tcEqTypeVis act_ty exp_ty
+              , not vis
+              = ppSuggestExplicitKinds
               | otherwise
               = empty
 
@@ -1320,7 +1797,7 @@ misMatchOrCND ctxt ct oriented ty1 ty2
     ev      = ctEvidence ct
     eq_pred = ctEvPred ev
     orig    = ctEvOrigin ev
-    givens  = [ given | given@(_, _, no_eqs, _) <- getUserGivens ctxt, not no_eqs]
+    givens  = [ given | given <- getUserGivens ctxt, not (ic_no_eqs given)]
               -- Keep only UserGivens that have some equalities
 
 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> SDoc
@@ -1335,30 +1812,32 @@ pp_givens givens
          (g:gs) ->      ppr_given (text "from the context:") g
                  : map (ppr_given (text "or from:")) gs
     where
-       ppr_given herald (gs, skol_info, _, loc)
+       ppr_given herald (Implic { ic_given = gs, ic_info = skol_info
+                                , ic_env = env })
            = hang (herald <+> pprEvVarTheta gs)
                 2 (sep [ text "bound by" <+> ppr skol_info
-                       , text "at" <+> ppr loc])
+                       , text "at" <+> ppr (tcl_loc env) ])
 
-extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
+extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> SDoc
 -- Add on extra info about skolem constants
 -- NB: The types themselves are already tidied
-extraTyVarInfo ctxt tv1 ty2
-  = ASSERT2( isTcTyVar tv1, ppr tv1 )
-    tv_extra tv1 $$ ty_extra ty2
+extraTyVarEqInfo ctxt tv1 ty2
+  = extraTyVarInfo ctxt tv1 $$ ty_extra ty2
   where
-    implics = cec_encl ctxt
     ty_extra ty = case tcGetTyVar_maybe ty of
-                    Just tv -> tv_extra tv
+                    Just tv -> extraTyVarInfo ctxt tv
                     Nothing -> empty
 
-    tv_extra tv
-      | let pp_tv = quotes (ppr tv)
-      = case tcTyVarDetails tv of
+extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
+extraTyVarInfo ctxt tv
+  = ASSERT2( isTyVar tv, ppr tv )
+    case tcTyVarDetails tv of
           SkolemTv {}   -> pprSkol implics tv
-          FlatSkol {}   -> pp_tv <+> text "is a flattening type variable"
           RuntimeUnk {} -> pp_tv <+> text "is an interactive-debugger skolem"
           MetaTv {}     -> empty
+  where
+    implics = cec_encl ctxt
+    pp_tv = quotes (ppr tv)
 
 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> SDoc
 -- See Note [Suggest adding a type signature]
@@ -1373,7 +1852,7 @@ suggestAddSig ctxt ty1 ty2
     inferred_bndrs = nub (get_inf ty1 ++ get_inf ty2)
     get_inf ty | Just tv <- tcGetTyVar_maybe ty
                , isSkolemTyVar tv
-               , (_, InferSkol prs) <- getSkolemInfo (cec_encl ctxt) tv
+               , InferSkol prs <- ic_info (getSkolemInfo (cec_encl ctxt) tv)
                = map fst prs
                | otherwise
                = []
@@ -1387,20 +1866,14 @@ misMatchMsg ct oriented ty1 ty2
   = misMatchMsg ct (Just IsSwapped) ty2 ty1
 
   -- These next two cases are when we're about to report, e.g., that
-  -- 'PtrRepLifted doesn't match 'VoidRep. Much better just to say
+  -- 'LiftedRep doesn't match 'VoidRep. Much better just to say
   -- lifted vs. unlifted
   | Just (tc1, []) <- splitTyConApp_maybe ty1
-  , tc1 `hasKey` ptrRepLiftedDataConKey
+  , tc1 `hasKey` liftedRepDataConKey
   = lifted_vs_unlifted
 
   | Just (tc2, []) <- splitTyConApp_maybe ty2
-  , tc2 `hasKey` ptrRepLiftedDataConKey
-  = lifted_vs_unlifted
-
-  | Just (tc1, []) <- splitTyConApp_maybe ty1
-  , Just (tc2, []) <- splitTyConApp_maybe ty2
-  ,    (tc1 `hasKey` ptrRepLiftedDataConKey && tc2 `hasKey` ptrRepUnliftedDataConKey)
-    || (tc1 `hasKey` ptrRepUnliftedDataConKey && tc2 `hasKey` ptrRepLiftedDataConKey)
+  , tc2 `hasKey` liftedRepDataConKey
   = lifted_vs_unlifted
 
   | otherwise  -- So now we have Nothing or (Just IsSwapped)
@@ -1445,7 +1918,7 @@ mkExpectedActualMsg :: Type -> Type -> CtOrigin -> Maybe TypeOrKind -> Bool
 -- NotSwapped means (actual, expected), IsSwapped is the reverse
 -- First return val is whether or not to print a herald above this msg
 mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
-                                          , uo_expected = Check exp
+                                          , uo_expected = exp
                                           , uo_thing = maybe_thing })
                     m_level printExpanded
   | KindLevel <- level, occurs_check_error       = (True, Nothing, empty)
@@ -1523,23 +1996,20 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
                    Just num_act_args -> num_act_args >= -n
                      -- don't report to strip off args that aren't there
                -> Just $ text "Expecting" <+> speakN (abs n) <+>
-                         more_or_fewer <+> plural_n (abs n) (text "argument")
-                                       <+> text "to" <+> quotes (ppr thing)
+                         more_or_fewer <+> quotes (ppr thing)
                where
-                 more_or_fewer | n < 0     = text "fewer"
-                               | otherwise = text "more"
+                 more_or_fewer
+                  | n < 0     = text "fewer arguments to"
+                  | n == 1    = text "more argument to"
+                  | otherwise = text "more arguments to"  -- n > 1
              _ -> Nothing
 
-
     maybe_num_args_msg = case num_args_msg of
       Nothing -> empty
       Just m  -> m
 
     count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
 
-    plural_n 1 doc = doc
-    plural_n _ doc = doc <> char 's'
-
     expandedTys =
       ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
         [ text "Type synonyms expanded:"
@@ -1551,7 +2021,22 @@ mkExpectedActualMsg ty1 ty2 (TypeEqOrigin { uo_actual = act
 
 mkExpectedActualMsg _ _ _ _ _ = panic "mkExpectedAcutalMsg"
 
-{-
+{- Note [Insoluble occurs check wins]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider [G] a ~ [a],  [W] a ~ [a] (Trac #13674).  The Given is insoluble
+so we don't use it for rewriting.  The Wanted is also insoluble, and
+we don't solve it from the Given.  It's very confusing to say
+    Cannot solve a ~ [a] from given constraints a ~ [a]
+
+And indeed even thinking about the Givens is silly; [W] a ~ [a] is
+just as insoluble as Int ~ Bool.
+
+Conclusion: if there's an insoluble occurs check (isInsolubleOccursCheck)
+then report it first.
+
+(NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
+want to be as draconian with them.)
+
 Note [Expanding type synonyms to make types similar]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -1562,108 +2047,146 @@ harder to understand. The whole point here is to make the difference in expected
 and found types clearer.
 
 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
-only as much as necessary. It should work like this:
+only as much as necessary. Given two types t1 and t2:
 
-Given two types t1 and t2:
-
-  * If they're already same, it shouldn't expand any type synonyms and
-    just return.
+  * If they're already same, it just returns the types.
 
   * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
-    type constructors), it should expand C1 and C2 if they're different type
-    synonyms. Then it should continue doing same thing on expanded types. If C1
-    and C2 are same, then we should apply same procedure to arguments of C1
-    and argument of C2 to make them as similar as possible.
+    type constructors), it expands C1 and C2 if they're different type synonyms.
+    Then it recursively does the same thing on expanded types. If C1 and C2 are
+    same, then it applies the same procedure to arguments of C1 and arguments of
+    C2 to make them as similar as possible.
 
     Most important thing here is to keep number of synonym expansions at
-    minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is
-    `T (T5, T3, Bool)` where T5 = T4, T4 = T3, ..., T1 = X, we should return
-    `T (T3, T3, Int)` and `T (T3, T3, Bool)`.
-
-In the implementation, we just search in all possible solutions for a solution
-that does minimum amount of expansions. This leads to a complex algorithm: If
-we have two synonyms like X_m = X_{m-1} = .. X and Y_n = Y_{n-1} = .. Y, where
-X and Y are rigid types, we expand m * n times. But in practice it's not a
-problem because deeply nested synonyms with no intervening rigid type
-constructors are vanishingly rare.
-
+    minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
+    Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
+    `T (T3, T3, Bool)`.
+
+  * Otherwise types don't have same shapes and so the difference is clearly
+    visible. It doesn't do any expansions and show these types.
+
+Note that we only expand top-layer type synonyms. Only when top-layer
+constructors are the same we start expanding inner type synonyms.
+
+Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
+respectively. If their type-synonym-expanded forms will meet at some point (i.e.
+will have same shapes according to `sameShapes` function), it's possible to find
+where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
+comparisons. We first collect all the top-layer expansions of t1 and t2 in two
+lists, then drop the prefix of the longer list so that they have same lengths.
+Then we search through both lists in parallel, and return the first pair of
+types that have same shapes. Inner types of these two types with same shapes
+are then expanded using the same algorithm.
+
+In case they don't meet, we return the last pair of types in the lists, which
+has top-layer type synonyms completely expanded. (in this case the inner types
+are not expanded at all, as the current form already shows the type error)
 -}
 
--- | Expand type synonyms in given types only enough to make them as equal as
+-- | Expand type synonyms in given types only enough to make them as similar as
 -- possible. Returned types are the same in terms of used type synonyms.
 --
 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
+--
+-- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
+-- some examples of how this should work.
 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
   where
-    (_, ty1_ret, ty2_ret) = go 0 ty1 ty2
+    (ty1_ret, ty2_ret) = go ty1 ty2
 
-    -- | Returns (number of synonym expansions done to make types similar,
-    --            type synonym expanded version of first type,
+    -- | Returns (type synonym expanded version of first type,
     --            type synonym expanded version of second type)
-    --
-    -- Int argument is number of synonym expansions done so far.
-    go :: Int -> Type -> Type -> (Int, Type, Type)
-    go exps t1 t2
+    go :: Type -> Type -> (Type, Type)
+    go t1 t2
       | t1 `pickyEqType` t2 =
         -- Types are same, nothing to do
-        (exps, t1, t2)
+        (t1, t2)
 
-    go exps t1@(TyConApp tc1 tys1) t2@(TyConApp tc2 tys2)
+    go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       | tc1 == tc2 =
         -- Type constructors are same. They may be synonyms, but we don't
         -- expand further.
-        let (exps', tys1', tys2') = unzip3 $ zipWith (go 0) tys1 tys2
-         in (exps + sum exps', TyConApp tc1 tys1', TyConApp tc2 tys2')
-      | otherwise =
-        -- Try to expand type constructors
-        case (coreView t1, coreView t2) of
-          -- When only one of the constructors is a synonym, we just
-          -- expand it and continue search
-          (Just t1', Nothing) ->
-            go (exps + 1) t1' t2
-          (Nothing, Just t2') ->
-            go (exps + 1) t1 t2'
-          (Just t1', Just t2') ->
-            -- Both constructors are synonyms, but they may be synonyms of
-            -- each other. We just search for minimally expanded solution.
-            -- See Note [Expanding type synonyms to make types similar].
-            let sol1@(exp1, _, _) = go (exps + 1) t1' t2
-                sol2@(exp2, _, _) = go (exps + 1) t1 t2'
-             in if exp1 < exp2 then sol1 else sol2
-          (Nothing, Nothing) ->
-            -- None of the constructors are synonyms, nothing to do
-            (exps, t1, t2)
-
-    go exps t1@TyConApp{} t2
-      | Just t1' <- coreView t1 = go (exps + 1) t1' t2
-      | otherwise               = (exps, t1, t2)
-
-    go exps t1 t2@TyConApp{}
-      | Just t2' <- coreView t2 = go (exps + 1) t1 t2'
-      | otherwise               = (exps, t1, t2)
-
-    go exps (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
-      let (exps1, t1_1', t2_1') = go 0 t1_1 t2_1
-          (exps2, t1_2', t2_2') = go 0 t1_2 t2_2
-       in (exps + exps1 + exps2, mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
-
-    go exps (ForAllTy (Anon t1_1) t1_2) (ForAllTy (Anon t2_1) t2_2) =
-      let (exps1, t1_1', t2_1') = go 0 t1_1 t2_1
-          (exps2, t1_2', t2_2') = go 0 t1_2 t2_2
-       in (exps + exps1 + exps2, mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
-
-    go exps (ForAllTy (Named tv1 vis1) t1) (ForAllTy (Named tv2 vis2) t2) =
+        let (tys1', tys2') =
+              unzip (zipWith (\ty1 ty2 -> go ty1 ty2) tys1 tys2)
+         in (TyConApp tc1 tys1', TyConApp tc2 tys2')
+
+    go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
+      let (t1_1', t2_1') = go t1_1 t2_1
+          (t1_2', t2_2') = go t1_2 t2_2
+       in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
+
+    go (FunTy t1_1 t1_2) (FunTy t2_1 t2_2) =
+      let (t1_1', t2_1') = go t1_1 t2_1
+          (t1_2', t2_2') = go t1_2 t2_2
+       in (mkFunTy t1_1' t1_2', mkFunTy t2_1' t2_2')
+
+    go (ForAllTy b1 t1) (ForAllTy b2 t2) =
       -- NOTE: We may have a bug here, but we just can't reproduce it easily.
       -- See D1016 comments for details and our attempts at producing a test
       -- case. Short version: We probably need RnEnv2 to really get this right.
-      let (exps1, t1', t2') = go exps t1 t2
-       in (exps1, ForAllTy (Named tv1 vis1) t1', ForAllTy (Named tv2 vis2) t2')
-
-    go exps (CastTy ty1 _) ty2 = go exps ty1 ty2
-    go exps ty1 (CastTy ty2 _) = go exps ty1 ty2
-
-    go exps t1 t2 = (exps, t1, t2)
+      let (t1', t2') = go t1 t2
+       in (ForAllTy b1 t1', ForAllTy b2 t2')
+
+    go (CastTy ty1 _) ty2 = go ty1 ty2
+    go ty1 (CastTy ty2 _) = go ty1 ty2
+
+    go t1 t2 =
+      -- See Note [Expanding type synonyms to make types similar] for how this
+      -- works
+      let
+        t1_exp_tys = t1 : tyExpansions t1
+        t2_exp_tys = t2 : tyExpansions t2
+        t1_exps    = length t1_exp_tys
+        t2_exps    = length t2_exp_tys
+        dif        = abs (t1_exps - t2_exps)
+      in
+        followExpansions $
+          zipEqual "expandSynonymsToMatch.go"
+            (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
+            (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
+
+    -- | Expand the top layer type synonyms repeatedly, collect expansions in a
+    -- list. The list does not include the original type.
+    --
+    -- Example, if you have:
+    --
+    --   type T10 = T9
+    --   type T9  = T8
+    --   ...
+    --   type T0  = Int
+    --
+    -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
+    --
+    -- This only expands the top layer, so if you have:
+    --
+    --   type M a = Maybe a
+    --
+    -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
+    tyExpansions :: Type -> [Type]
+    tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
+
+    -- | Drop the type pairs until types in a pair look alike (i.e. the outer
+    -- constructors are the same).
+    followExpansions :: [(Type, Type)] -> (Type, Type)
+    followExpansions [] = pprPanic "followExpansions" empty
+    followExpansions [(t1, t2)]
+      | sameShapes t1 t2 = go t1 t2 -- expand subtrees
+      | otherwise        = (t1, t2) -- the difference is already visible
+    followExpansions ((t1, t2) : tss)
+      -- Traverse subtrees when the outer shapes are the same
+      | sameShapes t1 t2 = go t1 t2
+      -- Otherwise follow the expansions until they look alike
+      | otherwise = followExpansions tss
+
+    sameShapes :: Type -> Type -> Bool
+    sameShapes AppTy{}          AppTy{}          = True
+    sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
+    sameShapes (FunTy {})       (FunTy {})       = True
+    sameShapes (ForAllTy {})    (ForAllTy {})    = True
+    sameShapes (CastTy ty1 _)   ty2              = sameShapes ty1 ty2
+    sameShapes ty1              (CastTy ty2 _)   = sameShapes ty1 ty2
+    sameShapes _                _                = False
 
 sameOccExtra :: TcType -> TcType -> SDoc
 -- See Note [Disambiguating (X ~ X) errors]
@@ -1727,7 +2250,7 @@ But nowadays when inferring the type of a function with no type signature,
 even if there are errors inside, we still generalise its signature and
 carry on. For example
    f x = x:x
-Here we will infer somethiing like
+Here we will infer something like
    f :: forall a. a -> [a]
 with a deferred error of (a ~ [a]).  So in the deferred unsolved constraint
 'a' is now a skolem, but not one bound by the programmer in the context!
@@ -1775,7 +2298,7 @@ mkDictErr ctxt cts
     is_no_inst (ct, (matches, unifiers, _))
       =  no_givens
       && null matches
-      && (null unifiers || all (not . isAmbiguousTyVar) (varSetElems (tyCoVarsOfCt ct)))
+      && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
 
     lookup_cls_inst inst_envs ct
                 -- Note [Flattening in error message generation]
@@ -1796,7 +2319,7 @@ mk_dict_err :: ReportErrCtxt -> (Ct, ClsInstLookupResult)
             -> TcM (ReportErrCtxt, SDoc)
 -- Report an overlap error if this class constraint results
 -- from an overlap (returning Left clas), otherwise return (Right pred)
-mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
+mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
   | null matches  -- No matches but perhaps several unifiers
   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
        ; candidate_insts <- get_candidate_instances
@@ -1813,8 +2336,9 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
     (clas, tys)   = getClassPredTys pred
     ispecs        = [ispec | (ispec, _) <- matches]
     unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
-    givens        = getUserGivens ctxt
-    all_tyvars    = all isTyVarTy tys
+    useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
+         -- useful_givens are the enclosing implications with non-empty givens,
+         -- modulo the horrid discardProvCtxtGivens
 
     get_candidate_instances :: TcM [ClsInst]
     -- See Note [Report candidate instances]
@@ -1840,11 +2364,16 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
     cannot_resolve_msg ct candidate_insts binds_msg
       = vcat [ no_inst_msg
              , nest 2 extra_note
-             , vcat (pp_givens givens)
-             , in_other_words
-             , ppWhen (has_ambig_tvs && not (null unifiers && null givens))
+             , vcat (pp_givens useful_givens)
+             , mb_patsyn_prov `orElse` empty
+             , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
                (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
-             , show_fixes (add_to_ctxt_fixes has_ambig_tvs ++ drv_fixes)
+
+             , ppWhen (isNothing mb_patsyn_prov) $
+                   -- Don't suggest fixes for the provided context of a pattern
+                   -- synonym; the right fix is to bind more in the pattern
+               show_fixes (ctxtFixes has_ambig_tvs pred implics
+                           ++ drv_fixes)
              , ppWhen (not (null candidate_insts))
                (hang (text "There are instances for similar types:")
                    2 (vcat (map ppr candidate_insts))) ]
@@ -1853,7 +2382,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
         orig = ctOrigin ct
         -- See Note [Highlighting ambiguous type variables]
         lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
-                        && not (null unifiers) && null givens
+                        && not (null unifiers) && null useful_givens
 
         (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
         ambig_tvs = uncurry (++) (getAmbigTkvs ct)
@@ -1864,7 +2393,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
               $$ text "prevents the constraint" <+>  quotes (pprParendType pred)
               <+> text "from being solved."
 
-          | null givens
+          | null useful_givens
           = addArising orig $ text "No instance for"
             <+> pprParendType pred
 
@@ -1885,37 +2414,20 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
                  , text "These potential instance" <> plural unifiers
                    <+> text "exist:"]
 
-        in_other_words
+        mb_patsyn_prov :: Maybe SDoc
+        mb_patsyn_prov
           | not lead_with_ambig
-          , ProvCtxtOrigin PSB{ psb_id  = (L _ name)
-                              , psb_def = (L _ pat) } <- orig
-            -- Here we check if the "required" context is empty, otherwise
-            -- the "In other words" is not strictly true
-          , null [ n | (_, SigSkol (PatSynCtxt n) _, _, _) <- givens, name == n ]
-          = vcat [ text "In other words, a successful match on the pattern"
-                 , nest 2 $ ppr pat
-                 , text "does not provide the constraint" <+> pprParendType pred ]
-          | otherwise = empty
+          , ProvCtxtOrigin PSB{ psb_def = L _ pat } <- orig
+          = Just (vcat [ text "In other words, a successful match on the pattern"
+                       , nest 2 $ ppr pat
+                       , text "does not provide the constraint" <+> pprParendType pred ])
+          | otherwise = Nothing
 
     -- Report "potential instances" only when the constraint arises
     -- directly from the user's use of an overloaded function
     want_potential (TypeEqOrigin {}) = False
     want_potential _                 = True
 
-    add_to_ctxt_fixes has_ambig_tvs
-      | not has_ambig_tvs && all_tyvars
-      , (orig:origs) <- usefulContext ctxt ct
-      = [sep [ text "add" <+> pprParendType pred
-               <+> text "to the context of"
-             , nest 2 $ ppr_skol orig $$
-                        vcat [ text "or" <+> ppr_skol orig
-                             | orig <- origs ] ] ]
-      | otherwise = []
-
-    ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
-    ppr_skol (PatSkol (PatSynCon ps)   _) = text "the pattern synonym"  <+> quotes (ppr ps)
-    ppr_skol skol_info = ppr skol_info
-
     extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
                = text "(maybe you haven't applied a function to enough arguments?)"
                | className clas == typeableClassName  -- Avoid mysterious "No instance for (Typeable T)
@@ -1960,7 +2472,7 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
                 -- simply report back the whole given
                 -- context. Accelerate Smart.hs showed this problem.
                   sep [ text "There exists a (perhaps superclass) match:"
-                      , nest 2 (vcat (pp_givens givens))]
+                      , nest 2 (vcat (pp_givens useful_givens))]
 
              ,  ppWhen (isSingleton matches) $
                 parens (vcat [ text "The choice depends on the instantiation of" <+>
@@ -1969,25 +2481,24 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
                                vcat [ text "To pick the first instance above, use IncoherentInstances"
                                     , text "when compiling the other instance declarations"]
                         ])]
-        where
-            givens = getUserGivens ctxt
-            matching_givens = mapMaybe matchable givens
-
-            matchable (evvars,skol_info,_,loc)
-              = case ev_vars_matching of
-                     [] -> Nothing
-                     _  -> Just $ hang (pprTheta ev_vars_matching)
-                                    2 (sep [ text "bound by" <+> ppr skol_info
-                                           , text "at" <+> ppr loc])
-                where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
-                      ev_var_matches ty = case getClassPredTys_maybe ty of
-                         Just (clas', tys')
-                           | clas' == clas
-                           , Just _ <- tcMatchTys tys tys'
-                           -> True
-                           | otherwise
-                           -> any ev_var_matches (immSuperClasses clas' tys')
-                         Nothing -> False
+
+    matching_givens = mapMaybe matchable useful_givens
+
+    matchable (Implic { ic_given = evvars, ic_info = skol_info, ic_env = env })
+      = case ev_vars_matching of
+             [] -> Nothing
+             _  -> Just $ hang (pprTheta ev_vars_matching)
+                            2 (sep [ text "bound by" <+> ppr skol_info
+                                   , text "at" <+> ppr (tcl_loc env) ])
+        where ev_vars_matching = filter ev_var_matches (map evVarPred evvars)
+              ev_var_matches ty = case getClassPredTys_maybe ty of
+                 Just (clas', tys')
+                   | clas' == clas
+                   , Just _ <- tcMatchTys tys tys'
+                   -> True
+                   | otherwise
+                   -> any ev_var_matches (immSuperClasses clas' tys')
+                 Nothing -> False
 
     -- Overlap error because of Safe Haskell (first
     -- match should be the most specific match)
@@ -2005,6 +2516,63 @@ mk_dict_err ctxt (ct, (matches, unifiers, unsafe_overlapped))
                    ]
             ]
 
+
+ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
+ctxtFixes has_ambig_tvs pred implics
+  | not has_ambig_tvs
+  , isTyVarClassPred pred
+  , (skol:skols) <- usefulContext implics pred
+  , let what | null skols
+             , SigSkol (PatSynCtxt {}) _ _ <- skol
+             = text "\"required\""
+             | otherwise
+             = empty
+  = [sep [ text "add" <+> pprParendType pred
+           <+> text "to the" <+> what <+> text "context of"
+         , nest 2 $ ppr_skol skol $$
+                    vcat [ text "or" <+> ppr_skol skol
+                         | skol <- skols ] ] ]
+  | otherwise = []
+  where
+    ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
+    ppr_skol (PatSkol (PatSynCon ps)   _) = text "the pattern synonym"  <+> quotes (ppr ps)
+    ppr_skol skol_info = ppr skol_info
+
+discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
+discardProvCtxtGivens orig givens  -- See Note [discardProvCtxtGivens]
+  | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig
+  = filterOut (discard name) givens
+  | otherwise
+  = givens
+  where
+    discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
+    discard _ _                                                  = False
+
+usefulContext :: [Implication] -> PredType -> [SkolemInfo]
+-- usefulContext picks out the implications whose context
+-- the programmer might plausibly augment to solve 'pred'
+usefulContext implics pred
+  = go implics
+  where
+    pred_tvs = tyCoVarsOfType pred
+    go [] = []
+    go (ic : ics)
+       | implausible ic = rest
+       | otherwise      = ic_info ic : rest
+       where
+          -- Stop when the context binds a variable free in the predicate
+          rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
+               | otherwise                                 = go ics
+
+    implausible ic
+      | null (ic_skols ic)            = True
+      | implausible_info (ic_info ic) = True
+      | otherwise                     = False
+
+    implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
+    implausible_info _                             = False
+    -- Do not suggest adding constraints to an *inferred* type signature
+
 {- Note [Report candidate instances]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
@@ -2031,40 +2599,50 @@ from being solved:
   - Lastly, I don't want to mess with error reporting for
     unknown runtime types so we just fall back to the old message there.
 Once these conditions are satisfied, we can safely say that ambiguity prevents
-the constraint from being solved. -}
-
+the constraint from being solved.
+
+Note [discardProvCtxtGivens]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In most situations we call all enclosing implications "useful". There is one
+exception, and that is when the constraint that causes the error is from the
+"provided" context of a pattern synonym declaration:
+
+  pattern Pat :: (Num a, Eq a) => Show a   => a -> Maybe a
+             --  required      => provided => type
+  pattern Pat x <- (Just x, 4)
+
+When checking the pattern RHS we must check that it does actually bind all
+the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
+bind the (Show a) constraint.  Answer: no!
+
+But the implication we generate for this will look like
+   forall a. (Num a, Eq a) => [W] Show a
+because when checking the pattern we must make the required
+constraints available, since they are needed to match the pattern (in
+this case the literal '4' needs (Num a, Eq a)).
+
+BUT we don't want to suggest adding (Show a) to the "required" constraints
+of the pattern synonym, thus:
+  pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
+It would then typecheck but it's silly.  We want the /pattern/ to bind
+the alleged "provided" constraints, Show a.
+
+So we suppress that Implication in discardProvCtxtGivens.  It's
+painfully ad-hoc but the truth is that adding it to the "required"
+constraints would work.  Suprressing it solves two problems.  First,
+we never tell the user that we could not deduce a "provided"
+constraint from the "required" context. Second, we never give a
+possible fix that suggests to add a "provided" constraint to the
+"required" context.
+
+For example, without this distinction the above code gives a bad error
+message (showing both problems):
+
+  error: Could not deduce (Show a) ... from the context: (Eq a)
+         ... Possible fix: add (Show a) to the context of
+         the signature for pattern synonym `Pat' ...
 
-usefulContext :: ReportErrCtxt -> Ct -> [SkolemInfo]
-usefulContext ctxt ct
-  = go (cec_encl ctxt)
-  where
-    pred_tvs = tyCoVarsOfType $ ctPred ct
-    go [] = []
-    go (ic : ics)
-       | implausible ic = rest
-       | otherwise      = ic_info ic : rest
-       where
-          -- Stop when the context binds a variable free in the predicate
-          rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
-               | otherwise                                 = go ics
-
-    implausible ic
-      | null (ic_skols ic)            = True
-      | implausible_info (ic_info ic) = True
-      | otherwise                     = False
-
-    implausible_info (SigSkol (InfSigCtxt {}  ) _) = True
-    implausible_info (SigSkol (PatSynCtxt name) _)
-      | (ProvCtxtOrigin PSB{ psb_id = (L _ name') }) <- ctOrigin ct
-      , name == name'                              = True
-    implausible_info _                             = False
-    -- Do not suggest adding constraints to an *inferred* type signature, or to
-    -- a pattern synonym signature when its "provided" context is the origin of
-    -- the wanted constraint.  For example,
-    --   pattern Pat :: () => Show a => a -> Maybe a
-    --   pattern Pat x = Just x
-    -- This declaration should not give the possible fix:
-    --   add (Show a) to the "required" context of the signature for `Pat'
+-}
 
 show_fixes :: [SDoc] -> SDoc
 show_fixes []     = empty
@@ -2104,7 +2682,7 @@ pprPotentials dflags sty herald insts
        -- are lexically in scope; these instances are likely
        -- to be more useful
     inst_in_scope :: ClsInst -> Bool
-    inst_in_scope cls_inst = foldNameSet ((&&) . name_in_scope) True $
+    inst_in_scope cls_inst = nameSetAll name_in_scope $
                              orphNamesOfTypes (is_tys cls_inst)
 
     name_in_scope name
@@ -2197,8 +2775,9 @@ mkAmbigMsg prepend_msg ct
         = pp_ambig (text "type") ambig_tvs
 
         | otherwise  -- All ambiguous kind variabes; suggest -fprint-explicit-kinds
+                     -- See Note [Suggest -fprint-explicit-kinds]
         = vcat [ pp_ambig (text "kind") ambig_kvs
-               , sdocWithDynFlags suggest_explicit_kinds ]
+               , ppSuggestExplicitKinds ]
 
     pp_ambig what tkvs
       | prepend_msg -- "Ambiguous type variable 't0'"
@@ -2212,44 +2791,34 @@ mkAmbigMsg prepend_msg ct
     is_or_are [_] = text "is"
     is_or_are _   = text "are"
 
-    suggest_explicit_kinds dflags  -- See Note [Suggest -fprint-explicit-kinds]
-      | gopt Opt_PrintExplicitKinds dflags = empty
-      | otherwise = text "Use -fprint-explicit-kinds to see the kind arguments"
-
 pprSkol :: [Implication] -> TcTyVar -> SDoc
 pprSkol implics tv
-  | (skol_tvs, skol_info) <- getSkolemInfo implics tv
   = case skol_info of
-      UnkSkol         -> pp_tv <+> text "is an unknown type variable"
-      SigSkol ctxt ty -> ppr_rigid (pprSigSkolInfo ctxt
-                                      (mkCheckExpType $
-                                       mkSpecForAllTys skol_tvs
-                                         (checkingExpType "pprSkol" ty)))
-      _               -> ppr_rigid (pprSkolInfo skol_info)
+      UnkSkol -> quotes (ppr tv) <+> text "is an unknown type variable"
+      _       -> ppr_rigid (pprSkolInfo skol_info)
   where
-    pp_tv = quotes (ppr tv)
-    ppr_rigid pp_info = hang (pp_tv <+> text "is a rigid type variable bound by")
-                           2 (sep [ pp_info
-                                  , text "at" <+> ppr (getSrcLoc tv) ])
+    Implic { ic_info = skol_info } = getSkolemInfo implics tv
+    ppr_rigid pp_info
+       = hang (quotes (ppr tv) <+> text "is a rigid type variable bound by")
+            2 (sep [ pp_info
+                   , text "at" <+> ppr (getSrcSpan tv) ])
 
 getAmbigTkvs :: Ct -> ([Var],[Var])
 getAmbigTkvs ct
   = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
   where
-    tkv_set       = tyCoVarsOfCt ct
-    ambig_tkv_set = filterVarSet isAmbiguousTyVar tkv_set
-    dep_tkv_set   = tyCoVarsOfTypes (map tyVarKind (varSetElems tkv_set))
-    ambig_tkvs    = varSetElems ambig_tkv_set
+    tkvs       = tyCoVarsOfCtList ct
+    ambig_tkvs = filter isAmbiguousTyVar tkvs
+    dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
 
-getSkolemInfo :: [Implication] -> TcTyVar -> ([TcTyVar], SkolemInfo)
+getSkolemInfo :: [Implication] -> TcTyVar -> Implication
 -- Get the skolem info for a type variable
 -- from the implication constraint that binds it
 getSkolemInfo [] tv
   = pprPanic "No skolem info:" (ppr tv)
 
 getSkolemInfo (implic:implics) tv
-  | let skols = ic_skols implic
-  , tv `elem` ic_skols implic = (skols, ic_info implic)
+  | tv `elem` ic_skols implic = implic
   | otherwise                 = getSkolemInfo implics tv
 
 -----------------------
@@ -2287,9 +2856,9 @@ relevantBindings want_filtering ctxt ct
                     [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
 
        ; (tidy_env', docs, discards)
-              <- go env1 ct_tvs (maxRelevantBinds dflags)
+              <- go dflags env1 ct_tvs (maxRelevantBinds dflags)
                     emptyVarSet [] False
-                    (tcl_bndrs lcl_env)
+                    (remove_shadowing $ tcl_bndrs lcl_env)
          -- tcl_bndrs has the innermost bindings first,
          -- which are probably the most relevant ones
 
@@ -2315,14 +2884,24 @@ relevantBindings want_filtering ctxt ct
     dec_max :: Maybe Int -> Maybe Int
     dec_max = fmap (\n -> n - 1)
 
-    go :: TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
+    ---- fixes #12177
+    ---- builds up a list of bindings whose OccName has not been seen before
+    remove_shadowing :: [TcIdBinder] -> [TcIdBinder]
+    remove_shadowing bindings = reverse $ fst $ foldl
+      (\(bindingAcc, seenNames) binding ->
+        if (occName binding) `elemOccSet` seenNames -- if we've seen it
+          then (bindingAcc, seenNames)              -- skip it
+          else (binding:bindingAcc, extendOccSet seenNames (occName binding)))
+      ([], emptyOccSet) bindings
+
+    go :: DynFlags -> TidyEnv -> TcTyVarSet -> Maybe Int -> TcTyVarSet -> [SDoc]
        -> Bool                          -- True <=> some filtered out due to lack of fuel
        -> [TcIdBinder]
        -> TcM (TidyEnv, [SDoc], Bool)   -- The bool says if we filtered any out
                                         -- because of lack of fuel
-    go tidy_env _ _ _ docs discards []
+    go tidy_env _ _ _ docs discards []
       = return (tidy_env, reverse docs, discards)
-    go tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
+    go dflags tidy_env ct_tvs n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
       = case tc_bndr of
           TcIdBndr id top_lvl -> go2 (idName id) (idType id) top_lvl
           TcIdBndr_ExpType name et top_lvl ->
@@ -2330,13 +2909,15 @@ relevantBindings want_filtering ctxt ct
                    -- et really should be filled in by now. But there's a chance
                    -- it hasn't, if, say, we're reporting a kind error en route to
                    -- checking a term. See test indexed-types/should_fail/T8129
-               ; ty <- case mb_ty of
-                   Just ty -> return ty
-                   Nothing -> do { traceTc "Defaulting an ExpType in relevantBindings"
-                                     (ppr et)
-                                 ; expTypeToType et }
-               ; go2 name ty top_lvl }
+                   -- Or we are reporting errors from the ambiguity check on
+                   -- a local type signature
+               ; case mb_ty of
+                   Just ty -> go2 name ty top_lvl
+                   Nothing -> discard_it  -- No info; discard
+               }
       where
+        discard_it = go dflags tidy_env ct_tvs n_left tvs_seen docs
+                        discards tc_bndrs
         go2 id_name id_type top_lvl
           = do { (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env id_type
                ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
@@ -2346,36 +2927,44 @@ relevantBindings want_filtering ctxt ct
                                     <+> ppr (getSrcLoc id_name)))]
                      new_seen = tvs_seen `unionVarSet` id_tvs
 
-               ; if (want_filtering && not opt_PprStyle_Debug
+               ; if (want_filtering && not (hasPprDebug dflags)
                                     && id_tvs `disjointVarSet` ct_tvs)
                           -- We want to filter out this binding anyway
                           -- so discard it silently
-                 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
+                 then discard_it
 
                  else if isTopLevel top_lvl && not (isNothing n_left)
                           -- It's a top-level binding and we have not specified
                           -- -fno-max-relevant-bindings, so discard it silently
-                 then go tidy_env ct_tvs n_left tvs_seen docs discards tc_bndrs
+                 then discard_it
 
                  else if run_out n_left && id_tvs `subVarSet` tvs_seen
                           -- We've run out of n_left fuel and this binding only
-                          -- mentions aleady-seen type variables, so discard it
-                 then go tidy_env ct_tvs n_left tvs_seen docs True tc_bndrs
+                          -- mentions already-seen type variables, so discard it
+                 then go dflags tidy_env ct_tvs n_left tvs_seen docs
+                         True      -- Record that we have now discarded something
+                         tc_bndrs
 
                           -- Keep this binding, decrement fuel
-                 else go tidy_env' ct_tvs (dec_max n_left) new_seen (doc:docs) discards tc_bndrs }
+                 else go dflags tidy_env' ct_tvs (dec_max n_left) new_seen
+                         (doc:docs) discards tc_bndrs }
 
 discardMsg :: SDoc
 discardMsg = text "(Some bindings suppressed;" <+>
              text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
 
+subsDiscardMsg :: SDoc
+subsDiscardMsg =
+    text "(Some substitutions suppressed;" <+>
+    text "use -fmax-valid-substitutions=N or -fno-max-valid-substitutions)"
+
 -----------------------
 warnDefaulting :: [Ct] -> Type -> TcM ()
 warnDefaulting wanteds default_ty
   = do { warn_default <- woptM Opt_WarnTypeDefaults
        ; env0 <- tcInitTidyEnv
        ; let tidy_env = tidyFreeTyCoVars env0 $
-                        foldr (unionVarSet . tyCoVarsOfCt) emptyVarSet wanteds
+                        tyCoVarsOfCtsList (listToBag wanteds)
              tidy_wanteds = map (tidyCt tidy_env) wanteds
              (loc, ppr_wanteds) = pprWithArising tidy_wanteds
              warn_msg =
@@ -2407,7 +2996,7 @@ solverDepthErrorTcS loc ty
   = setCtLocM loc $
     do { ty <- zonkTcType ty
        ; env0 <- tcInitTidyEnv
-       ; let tidy_env     = tidyFreeTyCoVars env0 (tyCoVarsOfType ty)
+       ; let tidy_env     = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
              tidy_ty      = tidyType tidy_env ty
              msg
                = vcat [ text "Reduction stack overflow; size =" <+> ppr depth