never executed always true always false
    1 
    2 {-# LANGUAGE LambdaCase          #-}
    3 {-# LANGUAGE ScopedTypeVariables #-}
    4 
    5 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns   #-}
    6 {-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
    7 
    8 module GHC.Tc.Errors(
    9        reportUnsolved, reportAllUnsolved, warnAllUnsolved,
   10        warnDefaulting,
   11 
   12        solverDepthErrorTcS
   13   ) where
   14 
   15 import GHC.Prelude
   16 
   17 import GHC.Driver.Env (hsc_units)
   18 import GHC.Driver.Session
   19 import GHC.Driver.Ppr
   20 import GHC.Driver.Config.Diagnostic
   21 
   22 import GHC.Tc.Types
   23 import GHC.Tc.Utils.Monad
   24 import GHC.Tc.Errors.Types
   25 import GHC.Tc.Types.Constraint
   26 import GHC.Tc.Utils.TcMType
   27 import GHC.Tc.Utils.Env( tcInitTidyEnv )
   28 import GHC.Tc.Utils.TcType
   29 import GHC.Tc.Utils.Unify ( checkTyVarEq )
   30 import GHC.Tc.Types.Origin
   31 import GHC.Tc.Types.Evidence
   32 import GHC.Tc.Types.EvTerm
   33 import GHC.Tc.Instance.Family
   34 import GHC.Tc.Utils.Instantiate
   35 import {-# SOURCE #-} GHC.Tc.Errors.Hole ( findValidHoleFits )
   36 
   37 import GHC.Types.Name
   38 import GHC.Types.Name.Reader ( lookupGRE_Name, GlobalRdrEnv, mkRdrUnqual
   39                              , emptyLocalRdrEnv, lookupGlobalRdrEnv , lookupLocalRdrOcc )
   40 import GHC.Types.Id
   41 import GHC.Types.Var
   42 import GHC.Types.Var.Set
   43 import GHC.Types.Var.Env
   44 import GHC.Types.Name.Env
   45 import GHC.Types.Name.Set
   46 import GHC.Types.SrcLoc
   47 import GHC.Types.Basic
   48 import GHC.Types.Error
   49 import GHC.Types.Unique.Set ( nonDetEltsUniqSet )
   50 
   51 import GHC.Rename.Unbound ( unknownNameSuggestions, WhatLooking(..) )
   52 import GHC.Unit.Module
   53 import GHC.Hs.Binds ( PatSynBind(..) )
   54 import GHC.Builtin.Names ( typeableClassName, pretendNameIsInScope )
   55 import qualified GHC.LanguageExtensions as LangExt
   56 
   57 import GHC.Core.Predicate
   58 import GHC.Core.Type
   59 import GHC.Core.Coercion
   60 import GHC.Core.TyCo.Rep
   61 import GHC.Core.TyCo.Ppr  ( pprTyVars, pprWithExplicitKindsWhen, pprSourceTyCon
   62                           , pprWithTYPE )
   63 import GHC.Core.Unify     ( tcMatchTys )
   64 import GHC.Core.InstEnv
   65 import GHC.Core.TyCon
   66 import GHC.Core.Class
   67 import GHC.Core.DataCon
   68 import GHC.Core.ConLike ( ConLike(..))
   69 
   70 import GHC.Utils.Error  (diagReasonSeverity,  pprLocMsgEnvelope )
   71 import GHC.Utils.Misc
   72 import GHC.Utils.Outputable as O
   73 import GHC.Utils.Panic
   74 import GHC.Utils.Panic.Plain
   75 import GHC.Utils.FV ( fvVarList, unionFV )
   76 
   77 import GHC.Data.Bag
   78 import GHC.Data.FastString
   79 import GHC.Utils.Trace (pprTraceUserWarning)
   80 import GHC.Data.List.SetOps ( equivClasses, nubOrdBy )
   81 import GHC.Data.Maybe
   82 import qualified GHC.Data.Strict as Strict
   83 
   84 import Control.Monad    ( unless, when, foldM, forM_ )
   85 import Data.Foldable    ( toList )
   86 import Data.Functor     ( (<&>) )
   87 import Data.Function    ( on )
   88 import Data.List        ( partition, mapAccumL, sortBy, unfoldr )
   89 -- import Data.Semigroup   ( Semigroup )
   90 import qualified Data.Semigroup as Semigroup
   91 
   92 
   93 {-
   94 ************************************************************************
   95 *                                                                      *
   96 \section{Errors and contexts}
   97 *                                                                      *
   98 ************************************************************************
   99 
  100 ToDo: for these error messages, should we note the location as coming
  101 from the insts, or just whatever seems to be around in the monad just
  102 now?
  103 
  104 Note [Deferring coercion errors to runtime]
  105 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  106 While developing, sometimes it is desirable to allow compilation to succeed even
  107 if there are type errors in the code. Consider the following case:
  108 
  109   module Main where
  110 
  111   a :: Int
  112   a = 'a'
  113 
  114   main = print "b"
  115 
  116 Even though `a` is ill-typed, it is not used in the end, so if all that we're
  117 interested in is `main` it is handy to be able to ignore the problems in `a`.
  118 
  119 Since we treat type equalities as evidence, this is relatively simple. Whenever
  120 we run into a type mismatch in GHC.Tc.Utils.Unify, we normally just emit an error. But it
  121 is always safe to defer the mismatch to the main constraint solver. If we do
  122 that, `a` will get transformed into
  123 
  124   co :: Int ~ Char
  125   co = ...
  126 
  127   a :: Int
  128   a = 'a' `cast` co
  129 
  130 The constraint solver would realize that `co` is an insoluble constraint, and
  131 emit an error with `reportUnsolved`. But we can also replace the right-hand side
  132 of `co` with `error "Deferred type error: Int ~ Char"`. This allows the program
  133 to compile, and it will run fine unless we evaluate `a`. This is what
  134 `deferErrorsToRuntime` does.
  135 
  136 It does this by keeping track of which errors correspond to which coercion
  137 in GHC.Tc.Errors. GHC.Tc.Errors.reportTidyWanteds does not print the errors
  138 and does not fail if -fdefer-type-errors is on, so that we can continue
  139 compilation. The errors are turned into warnings in `reportUnsolved`.
  140 -}
  141 
  142 -- | Report unsolved goals as errors or warnings. We may also turn some into
  143 -- deferred run-time errors if `-fdefer-type-errors` is on.
  144 reportUnsolved :: WantedConstraints -> TcM (Bag EvBind)
  145 reportUnsolved wanted
  146   = do { binds_var <- newTcEvBinds
  147        ; defer_errors <- goptM Opt_DeferTypeErrors
  148        ; let type_errors | not defer_errors = ErrorWithoutFlag
  149                          | otherwise        = WarningWithFlag Opt_WarnDeferredTypeErrors
  150 
  151        ; defer_holes <- goptM Opt_DeferTypedHoles
  152        ; let expr_holes | not defer_holes = ErrorWithoutFlag
  153                         | otherwise       = WarningWithFlag Opt_WarnTypedHoles
  154 
  155        ; partial_sigs      <- xoptM LangExt.PartialTypeSignatures
  156        ; let type_holes | not partial_sigs
  157                         = ErrorWithoutFlag
  158                         | otherwise
  159                         = WarningWithFlag Opt_WarnPartialTypeSignatures
  160 
  161        ; defer_out_of_scope <- goptM Opt_DeferOutOfScopeVariables
  162        ; let out_of_scope_holes | not defer_out_of_scope
  163                                 = ErrorWithoutFlag
  164                                 | otherwise
  165                                 = WarningWithFlag Opt_WarnDeferredOutOfScopeVariables
  166 
  167        ; report_unsolved type_errors expr_holes
  168                          type_holes out_of_scope_holes
  169                          binds_var wanted
  170 
  171        ; ev_binds <- getTcEvBindsMap binds_var
  172        ; return (evBindMapBinds ev_binds)}
  173 
  174 -- | Report *all* unsolved goals as errors, even if -fdefer-type-errors is on
  175 -- However, do not make any evidence bindings, because we don't
  176 -- have any convenient place to put them.
  177 -- NB: Type-level holes are OK, because there are no bindings.
  178 -- See Note [Deferring coercion errors to runtime]
  179 -- Used by solveEqualities for kind equalities
  180 --      (see Note [Fail fast on kind errors] in "GHC.Tc.Solver")
  181 reportAllUnsolved :: WantedConstraints -> TcM ()
  182 reportAllUnsolved wanted
  183   = do { ev_binds <- newNoTcEvBinds
  184 
  185        ; partial_sigs      <- xoptM LangExt.PartialTypeSignatures
  186        ; let type_holes | not partial_sigs  = ErrorWithoutFlag
  187                         | otherwise         = WarningWithFlag Opt_WarnPartialTypeSignatures
  188 
  189        ; report_unsolved ErrorWithoutFlag
  190                          ErrorWithoutFlag type_holes ErrorWithoutFlag
  191                          ev_binds wanted }
  192 
  193 -- | Report all unsolved goals as warnings (but without deferring any errors to
  194 -- run-time). See Note [Safe Haskell Overlapping Instances Implementation] in
  195 -- "GHC.Tc.Solver"
  196 warnAllUnsolved :: WantedConstraints -> TcM ()
  197 warnAllUnsolved wanted
  198   = do { ev_binds <- newTcEvBinds
  199        ; report_unsolved WarningWithoutFlag
  200                          WarningWithoutFlag
  201                          WarningWithoutFlag
  202                          WarningWithoutFlag
  203                          ev_binds wanted }
  204 
  205 -- | Report unsolved goals as errors or warnings.
  206 report_unsolved :: DiagnosticReason -- Deferred type errors
  207                 -> DiagnosticReason -- Expression holes
  208                 -> DiagnosticReason -- Type holes
  209                 -> DiagnosticReason -- Out of scope holes
  210                 -> EvBindsVar        -- cec_binds
  211                 -> WantedConstraints -> TcM ()
  212 report_unsolved type_errors expr_holes
  213     type_holes out_of_scope_holes binds_var wanted
  214   | isEmptyWC wanted
  215   = return ()
  216   | otherwise
  217   = do { traceTc "reportUnsolved {" $
  218          vcat [ text "type errors:" <+> ppr type_errors
  219               , text "expr holes:" <+> ppr expr_holes
  220               , text "type holes:" <+> ppr type_holes
  221               , text "scope holes:" <+> ppr out_of_scope_holes ]
  222        ; traceTc "reportUnsolved (before zonking and tidying)" (ppr wanted)
  223 
  224        ; wanted <- zonkWC wanted   -- Zonk to reveal all information
  225        ; let tidy_env = tidyFreeTyCoVars emptyTidyEnv free_tvs
  226              free_tvs = filterOut isCoVar $
  227                         tyCoVarsOfWCList wanted
  228                         -- tyCoVarsOfWC returns free coercion *holes*, even though
  229                         -- they are "bound" by other wanted constraints. They in
  230                         -- turn may mention variables bound further in, which makes
  231                         -- no sense. Really we should not return those holes at all;
  232                         -- for now we just filter them out.
  233 
  234        ; traceTc "reportUnsolved (after zonking):" $
  235          vcat [ text "Free tyvars:" <+> pprTyVars free_tvs
  236               , text "Tidy env:" <+> ppr tidy_env
  237               , text "Wanted:" <+> ppr wanted ]
  238 
  239        ; warn_redundant <- woptM Opt_WarnRedundantConstraints
  240        ; exp_syns <- goptM Opt_PrintExpandedSynonyms
  241        ; let err_ctxt = CEC { cec_encl  = []
  242                             , cec_tidy  = tidy_env
  243                             , cec_defer_type_errors = type_errors
  244                             , cec_expr_holes = expr_holes
  245                             , cec_type_holes = type_holes
  246                             , cec_out_of_scope_holes = out_of_scope_holes
  247                             , cec_suppress = insolubleWC wanted
  248                                  -- See Note [Suppressing error messages]
  249                                  -- Suppress low-priority errors if there
  250                                  -- are insoluble errors anywhere;
  251                                  -- See #15539 and c.f. setting ic_status
  252                                  -- in GHC.Tc.Solver.setImplicationStatus
  253                             , cec_warn_redundant = warn_redundant
  254                             , cec_expand_syns = exp_syns
  255                             , cec_binds    = binds_var }
  256 
  257        ; tc_lvl <- getTcLevel
  258        ; reportWanteds err_ctxt tc_lvl wanted
  259        ; traceTc "reportUnsolved }" empty }
  260 
  261 --------------------------------------------
  262 --      Internal functions
  263 --------------------------------------------
  264 
  265 -- | An error Report collects messages categorised by their importance.
  266 -- See Note [Error report] for details.
  267 data Report
  268   = Report { report_important :: [SDoc]
  269            , report_relevant_bindings :: [SDoc]
  270            , report_valid_hole_fits :: [SDoc]
  271            }
  272 
  273 instance Outputable Report where   -- Debugging only
  274   ppr (Report { report_important = imp
  275               , report_relevant_bindings = rel
  276               , report_valid_hole_fits = val })
  277     = vcat [ text "important:" <+> vcat imp
  278            , text "relevant:"  <+> vcat rel
  279            , text "valid:"  <+> vcat val ]
  280 
  281 {- Note [Error report]
  282 ~~~~~~~~~~~~~~~~~~~~~~
  283 The idea is that error msgs are divided into three parts: the main msg, the
  284 context block ("In the second argument of ..."), and the relevant bindings
  285 block, which are displayed in that order, with a mark to divide them. The
  286 the main msg ('report_important') varies depending on the error
  287 in question, but context and relevant bindings are always the same, which
  288 should simplify visual parsing.
  289 
  290 The context is added when the Report is passed off to 'mkErrorReport'.
  291 Unfortunately, unlike the context, the relevant bindings are added in
  292 multiple places so they have to be in the Report.
  293 -}
  294 
  295 instance Semigroup Report where
  296     Report a1 b1 c1 <> Report a2 b2 c2 = Report (a1 ++ a2) (b1 ++ b2) (c1 ++ c2)
  297 
  298 instance Monoid Report where
  299     mempty = Report [] [] []
  300     mappend = (Semigroup.<>)
  301 
  302 -- | Put a doc into the important msgs block.
  303 important :: SDoc -> Report
  304 important doc = mempty { report_important = [doc] }
  305 
  306 -- | Put a doc into the relevant bindings block.
  307 mk_relevant_bindings :: SDoc -> Report
  308 mk_relevant_bindings doc = mempty { report_relevant_bindings = [doc] }
  309 
  310 -- | Put a doc into the valid hole fits block.
  311 valid_hole_fits :: SDoc -> Report
  312 valid_hole_fits docs = mempty { report_valid_hole_fits = [docs] }
  313 
  314 data ReportErrCtxt
  315     = CEC { cec_encl :: [Implication]  -- Enclosing implications
  316                                        --   (innermost first)
  317                                        -- ic_skols and givens are tidied, rest are not
  318           , cec_tidy  :: TidyEnv
  319 
  320           , cec_binds :: EvBindsVar    -- Make some errors (depending on cec_defer)
  321                                        -- into warnings, and emit evidence bindings
  322                                        -- into 'cec_binds' for unsolved constraints
  323 
  324           , cec_defer_type_errors :: DiagnosticReason -- Defer type errors until runtime
  325 
  326           -- cec_expr_holes is a union of:
  327           --   cec_type_holes - a set of typed holes: '_', '_a', '_foo'
  328           --   cec_out_of_scope_holes - a set of variables which are
  329           --                            out of scope: 'x', 'y', 'bar'
  330           , cec_expr_holes :: DiagnosticReason -- Holes in expressions.
  331           , cec_type_holes :: DiagnosticReason -- Holes in types.
  332           , cec_out_of_scope_holes :: DiagnosticReason -- Out of scope holes.
  333 
  334           , cec_warn_redundant :: Bool    -- True <=> -Wredundant-constraints
  335           , cec_expand_syns    :: Bool    -- True <=> -fprint-expanded-synonyms
  336 
  337           , cec_suppress :: Bool    -- True <=> More important errors have occurred,
  338                                     --          so create bindings if need be, but
  339                                     --          don't issue any more errors/warnings
  340                                     -- See Note [Suppressing error messages]
  341       }
  342 
  343 instance Outputable ReportErrCtxt where
  344   ppr (CEC { cec_binds              = bvar
  345            , cec_defer_type_errors  = dte
  346            , cec_expr_holes         = eh
  347            , cec_type_holes         = th
  348            , cec_out_of_scope_holes = osh
  349            , cec_warn_redundant     = wr
  350            , cec_expand_syns        = es
  351            , cec_suppress           = sup })
  352     = text "CEC" <+> braces (vcat
  353          [ text "cec_binds"              <+> equals <+> ppr bvar
  354          , text "cec_defer_type_errors"  <+> equals <+> ppr dte
  355          , text "cec_expr_holes"         <+> equals <+> ppr eh
  356          , text "cec_type_holes"         <+> equals <+> ppr th
  357          , text "cec_out_of_scope_holes" <+> equals <+> ppr osh
  358          , text "cec_warn_redundant"     <+> equals <+> ppr wr
  359          , text "cec_expand_syns"        <+> equals <+> ppr es
  360          , text "cec_suppress"           <+> equals <+> ppr sup ])
  361 
  362 -- | Returns True <=> the ReportErrCtxt indicates that something is deferred
  363 deferringAnyBindings :: ReportErrCtxt -> Bool
  364   -- Don't check cec_type_holes, as these don't cause bindings to be deferred
  365 deferringAnyBindings (CEC { cec_defer_type_errors  = ErrorWithoutFlag
  366                           , cec_expr_holes         = ErrorWithoutFlag
  367                           , cec_out_of_scope_holes = ErrorWithoutFlag }) = False
  368 deferringAnyBindings _                                                   = True
  369 
  370 maybeSwitchOffDefer :: EvBindsVar -> ReportErrCtxt -> ReportErrCtxt
  371 -- Switch off defer-type-errors inside CoEvBindsVar
  372 -- See Note [Failing equalities with no evidence bindings]
  373 maybeSwitchOffDefer evb ctxt
  374  | CoEvBindsVar{} <- evb
  375  = ctxt { cec_defer_type_errors  = ErrorWithoutFlag
  376         , cec_expr_holes         = ErrorWithoutFlag
  377         , cec_out_of_scope_holes = ErrorWithoutFlag }
  378  | otherwise
  379  = ctxt
  380 
  381 {- Note [Failing equalities with no evidence bindings]
  382 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  383 If we go inside an implication that has no term evidence
  384 (e.g. unifying under a forall), we can't defer type errors.  You could
  385 imagine using the /enclosing/ bindings (in cec_binds), but that may
  386 not have enough stuff in scope for the bindings to be well typed.  So
  387 we just switch off deferred type errors altogether.  See #14605.
  388 
  389 This is done by maybeSwitchOffDefer.  It's also useful in one other
  390 place: see Note [Wrapping failing kind equalities] in GHC.Tc.Solver.
  391 
  392 Note [Suppressing error messages]
  393 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  394 The cec_suppress flag says "don't report any errors".  Instead, just create
  395 evidence bindings (as usual).  It's used when more important errors have occurred.
  396 
  397 Specifically (see reportWanteds)
  398   * If there are insoluble Givens, then we are in unreachable code and all bets
  399     are off.  So don't report any further errors.
  400   * If there are any insolubles (eg Int~Bool), here or in a nested implication,
  401     then suppress errors from the simple constraints here.  Sometimes the
  402     simple-constraint errors are a knock-on effect of the insolubles.
  403 
  404 This suppression behaviour is controlled by the Bool flag in
  405 ReportErrorSpec, as used in reportWanteds.
  406 
  407 But we need to take care: flags can turn errors into warnings, and we
  408 don't want those warnings to suppress subsequent errors (including
  409 suppressing the essential addTcEvBind for them: #15152). So in
  410 tryReporter we use askNoErrs to see if any error messages were
  411 /actually/ produced; if not, we don't switch on suppression.
  412 
  413 A consequence is that warnings never suppress warnings, so turning an
  414 error into a warning may allow subsequent warnings to appear that were
  415 previously suppressed.   (e.g. partial-sigs/should_fail/T14584)
  416 -}
  417 
  418 reportImplic :: ReportErrCtxt -> Implication -> TcM ()
  419 reportImplic ctxt implic@(Implic { ic_skols = tvs
  420                                  , ic_given = given
  421                                  , ic_wanted = wanted, ic_binds = evb
  422                                  , ic_status = status, ic_info = info
  423                                  , ic_tclvl = tc_lvl })
  424   | BracketSkol <- info
  425   , not insoluble
  426   = return ()        -- For Template Haskell brackets report only
  427                      -- definite errors. The whole thing will be re-checked
  428                      -- later when we plug it in, and meanwhile there may
  429                      -- certainly be un-satisfied constraints
  430 
  431   | otherwise
  432   = do { traceTc "reportImplic" (ppr implic')
  433        ; when bad_telescope $ reportBadTelescope ctxt tcl_env info tvs
  434                -- Do /not/ use the tidied tvs because then are in the
  435                -- wrong order, so tidying will rename things wrongly
  436        ; reportWanteds ctxt' tc_lvl wanted
  437        ; when (cec_warn_redundant ctxt) $
  438          warnRedundantConstraints ctxt' tcl_env info' dead_givens }
  439   where
  440     tcl_env      = ic_env implic
  441     insoluble    = isInsolubleStatus status
  442     (env1, tvs') = mapAccumL tidyVarBndr (cec_tidy ctxt) $
  443                    scopedSort tvs
  444         -- scopedSort: the ic_skols may not be in dependency order
  445         -- (see Note [Skolems in an implication] in GHC.Tc.Types.Constraint)
  446         -- but tidying goes wrong on out-of-order constraints;
  447         -- so we sort them here before tidying
  448     info'   = tidySkolemInfo env1 info
  449     implic' = implic { ic_skols = tvs'
  450                      , ic_given = map (tidyEvVar env1) given
  451                      , ic_info  = info' }
  452 
  453     ctxt1 = maybeSwitchOffDefer evb ctxt
  454     ctxt' = ctxt1 { cec_tidy     = env1
  455                   , cec_encl     = implic' : cec_encl ctxt
  456 
  457                   , cec_suppress = insoluble || cec_suppress ctxt
  458                         -- Suppress inessential errors if there
  459                         -- are insolubles anywhere in the
  460                         -- tree rooted here, or we've come across
  461                         -- a suppress-worthy constraint higher up (#11541)
  462 
  463                   , cec_binds    = evb }
  464 
  465     dead_givens = case status of
  466                     IC_Solved { ics_dead = dead } -> dead
  467                     _                             -> []
  468 
  469     bad_telescope = case status of
  470               IC_BadTelescope -> True
  471               _               -> False
  472 
  473 warnRedundantConstraints :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [EvVar] -> TcM ()
  474 -- See Note [Tracking redundant constraints] in GHC.Tc.Solver
  475 warnRedundantConstraints ctxt env info ev_vars
  476  | null redundant_evs
  477  = return ()
  478 
  479  | SigSkol user_ctxt _ _  <- info
  480  = setLclEnv env $  -- We want to add "In the type signature for f"
  481                     -- to the error context, which is a bit tiresome
  482    setSrcSpan (redundantConstraintsSpan user_ctxt) $
  483    addErrCtxt (text "In" <+> ppr info) $
  484    do { env <- getLclEnv
  485       ; msg <- mkErrorReport (WarningWithFlag Opt_WarnRedundantConstraints) ctxt env (important doc)
  486       ; reportDiagnostic msg }
  487 
  488  | otherwise  -- But for InstSkol there already *is* a surrounding
  489               -- "In the instance declaration for Eq [a]" context
  490               -- and we don't want to say it twice. Seems a bit ad-hoc
  491  = do { msg <- mkErrorReport (WarningWithFlag Opt_WarnRedundantConstraints) ctxt env (important doc)
  492       ; reportDiagnostic msg }
  493  where
  494    doc = text "Redundant constraint" <> plural redundant_evs <> colon
  495          <+> pprEvVarTheta redundant_evs
  496 
  497    redundant_evs =
  498        filterOut is_type_error $
  499        case info of -- See Note [Redundant constraints in instance decls]
  500          InstSkol -> filterOut (improving . idType) ev_vars
  501          _        -> ev_vars
  502 
  503    -- See #15232
  504    is_type_error = isJust . userTypeError_maybe . idType
  505 
  506    improving pred -- (transSuperClasses p) does not include p
  507      = any isImprovementPred (pred : transSuperClasses pred)
  508 
  509 reportBadTelescope :: ReportErrCtxt -> TcLclEnv -> SkolemInfo -> [TcTyVar] -> TcM ()
  510 reportBadTelescope ctxt env (ForAllSkol telescope) skols
  511   = do { msg <- mkErrorReport ErrorWithoutFlag ctxt env (important doc)
  512        ; reportDiagnostic msg }
  513   where
  514     doc = hang (text "These kind and type variables:" <+> telescope $$
  515                 text "are out of dependency order. Perhaps try this ordering:")
  516              2 (pprTyVars sorted_tvs)
  517 
  518     sorted_tvs = scopedSort skols
  519 
  520 reportBadTelescope _ _ skol_info skols
  521   = pprPanic "reportBadTelescope" (ppr skol_info $$ ppr skols)
  522 
  523 {- Note [Redundant constraints in instance decls]
  524 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  525 For instance declarations, we don't report unused givens if
  526 they can give rise to improvement.  Example (#10100):
  527     class Add a b ab | a b -> ab, a ab -> b
  528     instance Add Zero b b
  529     instance Add a b ab => Add (Succ a) b (Succ ab)
  530 The context (Add a b ab) for the instance is clearly unused in terms
  531 of evidence, since the dictionary has no fields.  But it is still
  532 needed!  With the context, a wanted constraint
  533    Add (Succ Zero) beta (Succ Zero)
  534 we will reduce to (Add Zero beta Zero), and thence we get beta := Zero.
  535 But without the context we won't find beta := Zero.
  536 
  537 This only matters in instance declarations..
  538 -}
  539 
  540 reportWanteds :: ReportErrCtxt -> TcLevel -> WantedConstraints -> TcM ()
  541 reportWanteds ctxt tc_lvl (WC { wc_simple = simples, wc_impl = implics
  542                               , wc_holes = holes })
  543   = do { traceTc "reportWanteds" (vcat [ text "Simples =" <+> ppr simples
  544                                        , text "Suppress =" <+> ppr (cec_suppress ctxt)
  545                                        , text "tidy_cts =" <+> ppr tidy_cts
  546                                        , text "tidy_holes = " <+> ppr tidy_holes ])
  547 
  548          -- First, deal with any out-of-scope errors:
  549        ; let (out_of_scope, other_holes) = partition isOutOfScopeHole tidy_holes
  550                -- don't suppress out-of-scope errors
  551              ctxt_for_scope_errs = ctxt { cec_suppress = False }
  552        ; (_, no_out_of_scope) <- askNoErrs $
  553                                  reportHoles tidy_cts ctxt_for_scope_errs out_of_scope
  554 
  555          -- Next, deal with things that are utterly wrong
  556          -- Like Int ~ Bool (incl nullary TyCons)
  557          -- or  Int ~ t a   (AppTy on one side)
  558          -- These /ones/ are not suppressed by the incoming context
  559          -- (but will be by out-of-scope errors)
  560        ; let ctxt_for_insols = ctxt { cec_suppress = not no_out_of_scope }
  561        ; reportHoles tidy_cts ctxt_for_insols other_holes
  562           -- holes never suppress
  563 
  564        ; (ctxt1, cts1) <- tryReporters ctxt_for_insols report1 tidy_cts
  565 
  566          -- Now all the other constraints.  We suppress errors here if
  567          -- any of the first batch failed, or if the enclosing context
  568          -- says to suppress
  569        ; let ctxt2 = ctxt { cec_suppress = cec_suppress ctxt || cec_suppress ctxt1 }
  570        ; (_, leftovers) <- tryReporters ctxt2 report2 cts1
  571        ; massertPpr (null leftovers)
  572            (text "The following unsolved Wanted constraints \
  573                  \have not been reported to the user:"
  574            $$ ppr leftovers)
  575 
  576             -- All the Derived ones have been filtered out of simples
  577             -- by the constraint solver. This is ok; we don't want
  578             -- to report unsolved Derived goals as errors
  579             -- See Note [Do not report derived but soluble errors]
  580 
  581      ; mapBagM_ (reportImplic ctxt2) implics }
  582             -- NB ctxt2: don't suppress inner insolubles if there's only a
  583             -- wanted insoluble here; but do suppress inner insolubles
  584             -- if there's a *given* insoluble here (= inaccessible code)
  585  where
  586     env = cec_tidy ctxt
  587     tidy_cts   = bagToList (mapBag (tidyCt env)   simples)
  588     tidy_holes = bagToList (mapBag (tidyHole env) holes)
  589 
  590     -- report1: ones that should *not* be suppressed by
  591     --          an insoluble somewhere else in the tree
  592     -- It's crucial that anything that is considered insoluble
  593     -- (see GHC.Tc.Utils.insolublWantedCt) is caught here, otherwise
  594     -- we might suppress its error message, and proceed on past
  595     -- type checking to get a Lint error later
  596     report1 = [ ("custom_error", unblocked is_user_type_error, True,  mkUserTypeErrorReporter)
  597 
  598               , given_eq_spec
  599               , ("insoluble2",   unblocked utterly_wrong,  True, mkGroupReporter mkEqErr)
  600               , ("skolem eq1",   unblocked very_wrong,     True, mkSkolReporter)
  601               , ("skolem eq2",   unblocked skolem_eq,      True, mkSkolReporter)
  602               , ("non-tv eq",    unblocked non_tv_eq,      True, mkSkolReporter)
  603 
  604                   -- The only remaining equalities are alpha ~ ty,
  605                   -- where alpha is untouchable; and representational equalities
  606                   -- Prefer homogeneous equalities over hetero, because the
  607                   -- former might be holding up the latter.
  608                   -- See Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
  609               , ("Homo eqs",      unblocked is_homo_equality, True,  mkGroupReporter mkEqErr)
  610               , ("Other eqs",     unblocked is_equality,      True,  mkGroupReporter mkEqErr)
  611               , ("Blocked eqs",   is_equality,           False, mkSuppressReporter mkBlockedEqErr)]
  612 
  613     -- report2: we suppress these if there are insolubles elsewhere in the tree
  614     report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)
  615               , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)
  616               , ("FixedRuntimeRep", is_FRR,          False, mkGroupReporter mkFRRErr)
  617               , ("Dicts",           is_dict,         False, mkGroupReporter mkDictErr) ]
  618 
  619     -- also checks to make sure the constraint isn't HoleBlockerReason
  620     -- See TcCanonical Note [Equalities with incompatible kinds], (4)
  621     unblocked :: (Ct -> Pred -> Bool) -> Ct -> Pred -> Bool
  622     unblocked _ (CIrredCan { cc_reason = HoleBlockerReason {}}) _ = False
  623     unblocked checker ct pred = checker ct pred
  624 
  625     -- rigid_nom_eq, rigid_nom_tv_eq,
  626     is_dict, is_equality, is_ip, is_FRR, is_irred :: Ct -> Pred -> Bool
  627 
  628     is_given_eq ct pred
  629        | EqPred {} <- pred = arisesFromGivens ct
  630        | otherwise         = False
  631        -- I think all given residuals are equalities
  632 
  633     -- Things like (Int ~N Bool)
  634     utterly_wrong _ (EqPred NomEq ty1 ty2) = isRigidTy ty1 && isRigidTy ty2
  635     utterly_wrong _ _                      = False
  636 
  637     -- Things like (a ~N Int)
  638     very_wrong _ (EqPred NomEq ty1 ty2) = isSkolemTy tc_lvl ty1 && isRigidTy ty2
  639     very_wrong _ _                      = False
  640 
  641     -- Things like (a ~N b) or (a  ~N  F Bool)
  642     skolem_eq _ (EqPred NomEq ty1 _) = isSkolemTy tc_lvl ty1
  643     skolem_eq _ _                    = False
  644 
  645     -- Things like (F a  ~N  Int)
  646     non_tv_eq _ (EqPred NomEq ty1 _) = not (isTyVarTy ty1)
  647     non_tv_eq _ _                    = False
  648 
  649     is_user_type_error ct _ = isUserTypeErrorCt ct
  650 
  651     is_homo_equality _ (EqPred _ ty1 ty2) = tcTypeKind ty1 `tcEqType` tcTypeKind ty2
  652     is_homo_equality _ _                  = False
  653 
  654     is_equality _ (EqPred {}) = True
  655     is_equality _ _           = False
  656 
  657     is_dict _ (ClassPred {}) = True
  658     is_dict _ _              = False
  659 
  660     is_ip _ (ClassPred cls _) = isIPClass cls
  661     is_ip _ _                 = False
  662 
  663     is_FRR ct (SpecialPred ConcretePrimPred _)
  664       | FixedRuntimeRepOrigin {} <- ctOrigin ct
  665       = True
  666     is_FRR _ _
  667       = False
  668 
  669     is_irred _ (IrredPred {}) = True
  670     is_irred _ _              = False
  671 
  672     given_eq_spec  -- See Note [Given errors]
  673       | has_gadt_match (cec_encl ctxt)
  674       = ("insoluble1a", is_given_eq, True,  mkGivenErrorReporter)
  675       | otherwise
  676       = ("insoluble1b", is_given_eq, False, ignoreErrorReporter)
  677           -- False means don't suppress subsequent errors
  678           -- Reason: we don't report all given errors
  679           --         (see mkGivenErrorReporter), and we should only suppress
  680           --         subsequent errors if we actually report this one!
  681           --         #13446 is an example
  682 
  683     -- See Note [Given errors]
  684     has_gadt_match [] = False
  685     has_gadt_match (implic : implics)
  686       | PatSkol {} <- ic_info implic
  687       , ic_given_eqs implic /= NoGivenEqs
  688       , ic_warn_inaccessible implic
  689           -- Don't bother doing this if -Winaccessible-code isn't enabled.
  690           -- See Note [Avoid -Winaccessible-code when deriving] in GHC.Tc.TyCl.Instance.
  691       = True
  692       | otherwise
  693       = has_gadt_match implics
  694 
  695 ---------------
  696 isSkolemTy :: TcLevel -> Type -> Bool
  697 -- The type is a skolem tyvar
  698 isSkolemTy tc_lvl ty
  699   | Just tv <- getTyVar_maybe ty
  700   =  isSkolemTyVar tv
  701   || (isTyVarTyVar tv && isTouchableMetaTyVar tc_lvl tv)
  702      -- The last case is for touchable TyVarTvs
  703      -- we postpone untouchables to a latter test (too obscure)
  704 
  705   | otherwise
  706   = False
  707 
  708 isTyFun_maybe :: Type -> Maybe TyCon
  709 isTyFun_maybe ty = case tcSplitTyConApp_maybe ty of
  710                       Just (tc,_) | isTypeFamilyTyCon tc -> Just tc
  711                       _ -> Nothing
  712 
  713 --------------------------------------------
  714 --      Reporters
  715 --------------------------------------------
  716 
  717 type Reporter
  718   = ReportErrCtxt -> [Ct] -> TcM ()
  719 type ReporterSpec
  720   = ( String                     -- Name
  721     , Ct -> Pred -> Bool         -- Pick these ones
  722     , Bool                       -- True <=> suppress subsequent reporters
  723     , Reporter)                  -- The reporter itself
  724 
  725 mkSkolReporter :: Reporter
  726 -- Suppress duplicates with either the same LHS, or same location
  727 mkSkolReporter ctxt cts
  728   = mapM_ (reportGroup mkEqErr ctxt) (group cts)
  729   where
  730      group [] = []
  731      group (ct:cts) = (ct : yeses) : group noes
  732         where
  733           (yeses, noes) = partition (group_with ct) cts
  734 
  735      group_with ct1 ct2
  736        | EQ <- cmp_loc ct1 ct2 = True
  737        | eq_lhs_type   ct1 ct2 = True
  738        | otherwise             = False
  739 
  740 reportHoles :: [Ct]  -- other (tidied) constraints
  741             -> ReportErrCtxt -> [Hole] -> TcM ()
  742 reportHoles tidy_cts ctxt holes
  743   = do
  744       diag_opts <- initDiagOpts <$> getDynFlags
  745       let severity = diagReasonSeverity diag_opts (cec_type_holes ctxt)
  746           holes'   = filter (keepThisHole severity) holes
  747       -- Zonk and tidy all the TcLclEnvs before calling `mkHoleError`
  748       -- because otherwise types will be zonked and tidied many times over.
  749       (tidy_env', lcl_name_cache) <- zonkTidyTcLclEnvs (cec_tidy ctxt) (map (ctl_env . hole_loc) holes')
  750       let ctxt' = ctxt { cec_tidy = tidy_env' }
  751       forM_ holes' $ \hole -> do { msg <- mkHoleError lcl_name_cache tidy_cts ctxt' hole
  752                                  ; reportDiagnostic msg }
  753 
  754 keepThisHole :: Severity -> Hole -> Bool
  755 -- See Note [Skip type holes rapidly]
  756 keepThisHole sev hole
  757   = case hole_sort hole of
  758        ExprHole {}    -> True
  759        TypeHole       -> keep_type_hole
  760        ConstraintHole -> keep_type_hole
  761   where
  762     keep_type_hole = case sev of
  763                          SevIgnore -> False
  764                          _         -> True
  765 
  766 -- | zonkTidyTcLclEnvs takes a bunch of 'TcLclEnv's, each from a Hole.
  767 -- It returns a ('Name' :-> 'Type') mapping which gives the zonked, tidied
  768 -- type for each Id in any of the binder stacks in the  'TcLclEnv's.
  769 -- Since there is a huge overlap between these stacks, is is much,
  770 -- much faster to do them all at once, avoiding duplication.
  771 zonkTidyTcLclEnvs :: TidyEnv -> [TcLclEnv] -> TcM (TidyEnv, NameEnv Type)
  772 zonkTidyTcLclEnvs tidy_env lcls = foldM go (tidy_env, emptyNameEnv) (concatMap tcl_bndrs lcls)
  773   where
  774     go envs tc_bndr = case tc_bndr of
  775           TcTvBndr {} -> return envs
  776           TcIdBndr id _top_lvl -> go_one (idName id) (idType id) envs
  777           TcIdBndr_ExpType name et _top_lvl ->
  778             do { mb_ty <- readExpType_maybe et
  779                    -- et really should be filled in by now. But there's a chance
  780                    -- it hasn't, if, say, we're reporting a kind error en route to
  781                    -- checking a term. See test indexed-types/should_fail/T8129
  782                    -- Or we are reporting errors from the ambiguity check on
  783                    -- a local type signature
  784                ; case mb_ty of
  785                    Just ty -> go_one name ty envs
  786                    Nothing -> return envs
  787                }
  788     go_one name ty (tidy_env, name_env) = do
  789             if name `elemNameEnv` name_env
  790               then return (tidy_env, name_env)
  791               else do
  792                 (tidy_env', tidy_ty) <- zonkTidyTcType tidy_env ty
  793                 return (tidy_env',  extendNameEnv name_env name tidy_ty)
  794 
  795 {- Note [Skip type holes rapidly]
  796 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  797 Suppose we have module with a /lot/ of partial type signatures, and we
  798 compile it while suppressing partial-type-signature warnings.  Then
  799 we don't want to spend ages constructing error messages and lists of
  800 relevant bindings that we never display! This happened in #14766, in
  801 which partial type signatures in a Happy-generated parser cause a huge
  802 increase in compile time.
  803 
  804 The function ignoreThisHole short-circuits the error/warning generation
  805 machinery, in cases where it is definitely going to be a no-op.
  806 -}
  807 
  808 mkUserTypeErrorReporter :: Reporter
  809 mkUserTypeErrorReporter ctxt
  810   = mapM_ $ \ct -> do { let err = mkUserTypeError ct
  811                       ; maybeReportError ctxt ct err
  812                       ; addDeferredBinding ctxt err ct }
  813 
  814 mkUserTypeError :: Ct -> Report
  815 mkUserTypeError ct = important
  816                    $ pprUserTypeErrorTy
  817                    $ case getUserTypeErrorMsg ct of
  818                        Just msg -> msg
  819                        Nothing  -> pprPanic "mkUserTypeError" (ppr ct)
  820 
  821 mkGivenErrorReporter :: Reporter
  822 -- See Note [Given errors]
  823 mkGivenErrorReporter ctxt cts
  824   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
  825        ; let (implic:_) = cec_encl ctxt
  826                  -- Always non-empty when mkGivenErrorReporter is called
  827              ct' = setCtLoc ct (setCtLocEnv (ctLoc ct) (ic_env implic))
  828                    -- For given constraints we overwrite the env (and hence src-loc)
  829                    -- with one from the immediately-enclosing implication.
  830                    -- See Note [Inaccessible code]
  831 
  832              inaccessible_msg = hang (text "Inaccessible code in")
  833                                    2 (ppr (ic_info implic))
  834              report = important inaccessible_msg `mappend`
  835                       mk_relevant_bindings binds_msg
  836 
  837        ; report <- mkEqErr_help ctxt report ct' ty1 ty2
  838        ; err <- mkErrorReport (WarningWithFlag Opt_WarnInaccessibleCode) ctxt
  839                               (ctLocEnv (ctLoc ct')) report
  840 
  841        ; traceTc "mkGivenErrorReporter" (ppr ct)
  842        ; reportDiagnostic err }
  843   where
  844     (ct : _ )  = cts    -- Never empty
  845     (ty1, ty2) = getEqPredTys (ctPred ct)
  846 
  847 ignoreErrorReporter :: Reporter
  848 -- Discard Given errors that don't come from
  849 -- a pattern match; maybe we should warn instead?
  850 ignoreErrorReporter ctxt cts
  851   = do { traceTc "mkGivenErrorReporter no" (ppr cts $$ ppr (cec_encl ctxt))
  852        ; return () }
  853 
  854 
  855 {- Note [Given errors]
  856 ~~~~~~~~~~~~~~~~~~~~~~
  857 Given constraints represent things for which we have (or will have)
  858 evidence, so they aren't errors.  But if a Given constraint is
  859 insoluble, this code is inaccessible, and we might want to at least
  860 warn about that.  A classic case is
  861 
  862    data T a where
  863      T1 :: T Int
  864      T2 :: T a
  865      T3 :: T Bool
  866 
  867    f :: T Int -> Bool
  868    f T1 = ...
  869    f T2 = ...
  870    f T3 = ...  -- We want to report this case as inaccessible
  871 
  872 We'd like to point out that the T3 match is inaccessible. It
  873 will have a Given constraint [G] Int ~ Bool.
  874 
  875 But we don't want to report ALL insoluble Given constraints.  See Trac
  876 #12466 for a long discussion.  For example, if we aren't careful
  877 we'll complain about
  878    f :: ((Int ~ Bool) => a -> a) -> Int
  879 which arguably is OK.  It's more debatable for
  880    g :: (Int ~ Bool) => Int -> Int
  881 but it's tricky to distinguish these cases so we don't report
  882 either.
  883 
  884 The bottom line is this: has_gadt_match looks for an enclosing
  885 pattern match which binds some equality constraints.  If we
  886 find one, we report the insoluble Given.
  887 -}
  888 
  889 mkGroupReporter :: (ReportErrCtxt -> [Ct] -> TcM Report)
  890                              -- Make error message for a group
  891                 -> Reporter  -- Deal with lots of constraints
  892 -- Group together errors from same location,
  893 -- and report only the first (to avoid a cascade)
  894 mkGroupReporter mk_err ctxt cts
  895   = mapM_ (reportGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
  896 
  897 -- Like mkGroupReporter, but doesn't actually print error messages
  898 mkSuppressReporter :: (ReportErrCtxt -> [Ct] -> TcM Report)
  899                    -> Reporter
  900 mkSuppressReporter mk_err ctxt cts
  901   = mapM_ (suppressGroup mk_err ctxt . toList) (equivClasses cmp_loc cts)
  902 
  903 eq_lhs_type :: Ct -> Ct -> Bool
  904 eq_lhs_type ct1 ct2
  905   = case (classifyPredType (ctPred ct1), classifyPredType (ctPred ct2)) of
  906        (EqPred eq_rel1 ty1 _, EqPred eq_rel2 ty2 _) ->
  907          (eq_rel1 == eq_rel2) && (ty1 `eqType` ty2)
  908        _ -> pprPanic "mkSkolReporter" (ppr ct1 $$ ppr ct2)
  909 
  910 cmp_loc :: Ct -> Ct -> Ordering
  911 cmp_loc ct1 ct2 = get ct1 `compare` get ct2
  912   where
  913     get ct = realSrcSpanStart (ctLocSpan (ctLoc ct))
  914              -- Reduce duplication by reporting only one error from each
  915              -- /starting/ location even if the end location differs
  916 
  917 reportGroup :: (ReportErrCtxt -> [Ct] -> TcM Report) -> Reporter
  918 reportGroup mk_err ctxt cts
  919   | ct1 : _ <- cts =
  920   do { err <- mk_err ctxt cts
  921      ; traceTc "About to maybeReportErr" $
  922        vcat [ text "Constraint:"             <+> ppr cts
  923             , text "cec_suppress ="          <+> ppr (cec_suppress ctxt)
  924             , text "cec_defer_type_errors =" <+> ppr (cec_defer_type_errors ctxt) ]
  925      ; maybeReportError ctxt ct1 err
  926          -- But see Note [Always warn with -fdefer-type-errors]
  927      ; traceTc "reportGroup" (ppr cts)
  928      ; mapM_ (addDeferredBinding ctxt err) cts }
  929          -- Add deferred bindings for all
  930          -- Redundant if we are going to abort compilation,
  931          -- but that's hard to know for sure, and if we don't
  932          -- abort, we need bindings for all (e.g. #12156)
  933   | otherwise = panic "empty reportGroup"
  934 
  935 -- like reportGroup, but does not actually report messages. It still adds
  936 -- -fdefer-type-errors bindings, though.
  937 suppressGroup :: (ReportErrCtxt -> [Ct] -> TcM Report) -> Reporter
  938 suppressGroup mk_err ctxt cts
  939  = do { err <- mk_err ctxt cts
  940       ; traceTc "Suppressing errors for" (ppr cts)
  941       ; mapM_ (addDeferredBinding ctxt err) cts }
  942 
  943 -- See Note [No deferring for multiplicity errors]
  944 nonDeferrableOrigin :: CtOrigin -> Bool
  945 nonDeferrableOrigin NonLinearPatternOrigin     = True
  946 nonDeferrableOrigin (UsageEnvironmentOf {})    = True
  947 nonDeferrableOrigin (FixedRuntimeRepOrigin {}) = True
  948 nonDeferrableOrigin _                          = False
  949 
  950 maybeReportError :: ReportErrCtxt -> Ct -> Report -> TcM ()
  951 maybeReportError ctxt ct report
  952   = unless (cec_suppress ctxt) $ -- Some worse error has occurred, so suppress this diagnostic
  953     do let reason | nonDeferrableOrigin (ctOrigin ct) = ErrorWithoutFlag
  954                   | otherwise                         = cec_defer_type_errors ctxt
  955                   -- See Note [No deferring for multiplicity errors]
  956        msg <- mkErrorReport reason ctxt (ctLocEnv (ctLoc ct)) report
  957        reportDiagnostic msg
  958 
  959 addDeferredBinding :: ReportErrCtxt -> Report -> Ct -> TcM ()
  960 -- See Note [Deferring coercion errors to runtime]
  961 addDeferredBinding ctxt err ct
  962   | deferringAnyBindings ctxt
  963   , CtWanted { ctev_pred = pred, ctev_dest = dest } <- ctEvidence ct
  964     -- Only add deferred bindings for Wanted constraints
  965   = do { err_tm <- mkErrorTerm ctxt (ctLoc ct) pred err
  966        ; let ev_binds_var = cec_binds ctxt
  967 
  968        ; case dest of
  969            EvVarDest evar
  970              -> addTcEvBind ev_binds_var $ mkWantedEvBind evar err_tm
  971            HoleDest hole
  972              -> do { -- See Note [Deferred errors for coercion holes]
  973                      let co_var = coHoleCoVar hole
  974                    ; addTcEvBind ev_binds_var $ mkWantedEvBind co_var err_tm
  975                    ; fillCoercionHole hole (mkTcCoVarCo co_var) }}
  976 
  977   | otherwise   -- Do not set any evidence for Given/Derived
  978   = return ()
  979 
  980 mkErrorTerm :: ReportErrCtxt -> CtLoc -> Type  -- of the error term
  981             -> Report -> TcM EvTerm
  982 mkErrorTerm ctxt ct_loc ty report
  983   = do { msg <- mkErrorReport ErrorWithoutFlag ctxt (ctLocEnv ct_loc) report
  984          -- This will be reported at runtime, so we always want "error:" in the report, never "warning:"
  985        ; dflags <- getDynFlags
  986        ; let err_msg = pprLocMsgEnvelope msg
  987              err_str = showSDoc dflags $
  988                        err_msg $$ text "(deferred type error)"
  989 
  990        ; return $ evDelayedError ty err_str }
  991 
  992 tryReporters :: ReportErrCtxt -> [ReporterSpec] -> [Ct] -> TcM (ReportErrCtxt, [Ct])
  993 -- Use the first reporter in the list whose predicate says True
  994 tryReporters ctxt reporters cts
  995   = do { let (vis_cts, invis_cts) = partition (isVisibleOrigin . ctOrigin) cts
  996        ; traceTc "tryReporters {" (ppr vis_cts $$ ppr invis_cts)
  997        ; (ctxt', cts') <- go ctxt reporters vis_cts invis_cts
  998        ; traceTc "tryReporters }" (ppr cts')
  999        ; return (ctxt', cts') }
 1000   where
 1001     go ctxt [] vis_cts invis_cts
 1002       = return (ctxt, vis_cts ++ invis_cts)
 1003 
 1004     go ctxt (r : rs) vis_cts invis_cts
 1005        -- always look at *visible* Origins before invisible ones
 1006        -- this is the whole point of isVisibleOrigin
 1007       = do { (ctxt', vis_cts') <- tryReporter ctxt r vis_cts
 1008            ; (ctxt'', invis_cts') <- tryReporter ctxt' r invis_cts
 1009            ; go ctxt'' rs vis_cts' invis_cts' }
 1010                 -- Carry on with the rest, because we must make
 1011                 -- deferred bindings for them if we have -fdefer-type-errors
 1012                 -- But suppress their error messages
 1013 
 1014 tryReporter :: ReportErrCtxt -> ReporterSpec -> [Ct] -> TcM (ReportErrCtxt, [Ct])
 1015 tryReporter ctxt (str, keep_me,  suppress_after, reporter) cts
 1016   | null yeses
 1017   = return (ctxt, cts)
 1018   | otherwise
 1019   = do { traceTc "tryReporter{ " (text str <+> ppr yeses)
 1020        ; (_, no_errs) <- askNoErrs (reporter ctxt yeses)
 1021        ; let suppress_now = not no_errs && suppress_after
 1022                             -- See Note [Suppressing error messages]
 1023              ctxt' = ctxt { cec_suppress = suppress_now || cec_suppress ctxt }
 1024        ; traceTc "tryReporter end }" (text str <+> ppr (cec_suppress ctxt) <+> ppr suppress_after)
 1025        ; return (ctxt', nos) }
 1026   where
 1027     (yeses, nos) = partition (\ct -> keep_me ct (classifyPredType (ctPred ct))) cts
 1028 
 1029 pprArising :: CtOrigin -> SDoc
 1030 -- Used for the main, top-level error message
 1031 -- We've done special processing for TypeEq, KindEq, Given
 1032 pprArising (TypeEqOrigin {}) = empty
 1033 pprArising (KindEqOrigin {}) = empty
 1034 pprArising (GivenOrigin {})  = empty
 1035 pprArising orig              = pprCtOrigin orig
 1036 
 1037 -- Add the "arising from..." part to a message about bunch of dicts
 1038 addArising :: CtOrigin -> SDoc -> SDoc
 1039 addArising orig msg = hang msg 2 (pprArising orig)
 1040 
 1041 pprWithArising :: [Ct] -> (CtLoc, SDoc)
 1042 -- Print something like
 1043 --    (Eq a) arising from a use of x at y
 1044 --    (Show a) arising from a use of p at q
 1045 -- Also return a location for the error message
 1046 -- Works for Wanted/Derived only
 1047 pprWithArising []
 1048   = panic "pprWithArising"
 1049 pprWithArising (ct:cts)
 1050   | null cts
 1051   = (loc, addArising (ctLocOrigin loc)
 1052                      (pprTheta [ctPred ct]))
 1053   | otherwise
 1054   = (loc, vcat (map ppr_one (ct:cts)))
 1055   where
 1056     loc = ctLoc ct
 1057     ppr_one ct' = hang (parens (pprType (ctPred ct')))
 1058                      2 (pprCtLoc (ctLoc ct'))
 1059 
 1060 mkErrorReport :: DiagnosticReason
 1061               -> ReportErrCtxt
 1062               -> TcLclEnv
 1063               -> Report
 1064               -> TcM (MsgEnvelope TcRnMessage)
 1065 mkErrorReport rea ctxt tcl_env (Report important relevant_bindings valid_subs)
 1066   = do { context <- mkErrInfo (cec_tidy ctxt) (tcl_ctxt tcl_env)
 1067        ; unit_state <- hsc_units <$> getTopEnv ;
 1068        ; let err_info = ErrInfo context (vcat $ relevant_bindings ++ valid_subs)
 1069        ; let msg = TcRnUnknownMessage $ mkPlainDiagnostic rea noHints (vcat important)
 1070        ; mkTcRnMessage
 1071            (RealSrcSpan (tcl_loc tcl_env) Strict.Nothing)
 1072            (TcRnMessageWithInfo unit_state $ TcRnMessageDetailed err_info msg)
 1073        }
 1074 
 1075 -- This version does not include the context
 1076 mkErrorReportNC :: DiagnosticReason
 1077                 -> TcLclEnv
 1078                 -> Report
 1079                 -> TcM (MsgEnvelope TcRnMessage)
 1080 mkErrorReportNC rea tcl_env (Report important relevant_bindings valid_subs)
 1081   = do { unit_state <- hsc_units <$> getTopEnv ;
 1082        ; let err_info = ErrInfo O.empty (vcat $ relevant_bindings ++ valid_subs)
 1083        ; let msg = TcRnUnknownMessage $ mkPlainDiagnostic rea noHints (vcat important)
 1084        ; mkTcRnMessage
 1085            (RealSrcSpan (tcl_loc tcl_env) Strict.Nothing)
 1086            (TcRnMessageWithInfo unit_state $ TcRnMessageDetailed err_info msg)
 1087        }
 1088 
 1089 type UserGiven = Implication
 1090 
 1091 getUserGivens :: ReportErrCtxt -> [UserGiven]
 1092 -- One item for each enclosing implication
 1093 getUserGivens (CEC {cec_encl = implics}) = getUserGivensFromImplics implics
 1094 
 1095 getUserGivensFromImplics :: [Implication] -> [UserGiven]
 1096 getUserGivensFromImplics implics
 1097   = reverse (filterOut (null . ic_given) implics)
 1098 
 1099 {- Note [Always warn with -fdefer-type-errors]
 1100 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1101 When -fdefer-type-errors is on we warn about *all* type errors, even
 1102 if cec_suppress is on.  This can lead to a lot more warnings than you
 1103 would get errors without -fdefer-type-errors, but if we suppress any of
 1104 them you might get a runtime error that wasn't warned about at compile
 1105 time.
 1106 
 1107 To be consistent, we should also report multiple warnings from a single
 1108 location in mkGroupReporter, when -fdefer-type-errors is on.  But that
 1109 is perhaps a bit *over*-consistent!
 1110 
 1111 With #10283, you can now opt out of deferred type error warnings.
 1112 
 1113 Note [No deferring for multiplicity errors]
 1114 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1115 As explained in Note [Wrapper returned from tcSubMult] in GHC.Tc.Utils.Unify,
 1116 linear types do not support casts and any nontrivial coercion will raise
 1117 an error during desugaring.
 1118 
 1119 This means that even if we defer a multiplicity mismatch during typechecking,
 1120 the desugarer will refuse to compile anyway. Worse: the error raised
 1121 by the desugarer would shadow the type mismatch warnings (#20083).
 1122 As a solution, we refuse to defer submultiplicity constraints. Test: T20083.
 1123 
 1124 To determine whether a constraint arose from a submultiplicity check, we
 1125 look at the CtOrigin. All calls to tcSubMult use one of two origins,
 1126 UsageEnvironmentOf and NonLinearPatternOrigin. Those origins are not
 1127 used outside of linear types.
 1128 
 1129 In the future, we should compile 'WpMultCoercion' to a runtime error with
 1130 -fdefer-type-errors, but the current implementation does not always
 1131 place the wrapper in the right place and the resulting program can fail Lint.
 1132 This plan is tracked in #20083.
 1133 
 1134 Note [Deferred errors for coercion holes]
 1135 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1136 Suppose we need to defer a type error where the destination for the evidence
 1137 is a coercion hole. We can't just put the error in the hole, because we can't
 1138 make an erroneous coercion. (Remember that coercions are erased for runtime.)
 1139 Instead, we invent a new EvVar, bind it to an error and then make a coercion
 1140 from that EvVar, filling the hole with that coercion. Because coercions'
 1141 types are unlifted, the error is guaranteed to be hit before we get to the
 1142 coercion.
 1143 
 1144 Note [Do not report derived but soluble errors]
 1145 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1146 The wc_simples include Derived constraints that have not been solved,
 1147 but are not insoluble (in that case they'd be reported by 'report1').
 1148 We do not want to report these as errors:
 1149 
 1150 * Superclass constraints. If we have an unsolved [W] Ord a, we'll also have
 1151   an unsolved [D] Eq a, and we do not want to report that; it's just noise.
 1152 
 1153 * Functional dependencies.  For givens, consider
 1154       class C a b | a -> b
 1155       data T a where
 1156          MkT :: C a d => [d] -> T a
 1157       f :: C a b => T a -> F Int
 1158       f (MkT xs) = length xs
 1159   Then we get a [D] b~d.  But there *is* a legitimate call to
 1160   f, namely   f (MkT [True]) :: T Bool, in which b=d.  So we should
 1161   not reject the program.
 1162 
 1163   For wanteds, something similar
 1164       data T a where
 1165         MkT :: C Int b => a -> b -> T a
 1166       g :: C Int c => c -> ()
 1167       f :: T a -> ()
 1168       f (MkT x y) = g x
 1169   Here we get [G] C Int b, [W] C Int a, hence [D] a~b.
 1170   But again f (MkT True True) is a legitimate call.
 1171 
 1172 (We leave the Deriveds in wc_simple until reportErrors, so that we don't lose
 1173 derived superclasses between iterations of the solver.)
 1174 
 1175 For functional dependencies, here is a real example,
 1176 stripped off from libraries/utf8-string/Codec/Binary/UTF8/Generic.hs
 1177 
 1178   class C a b | a -> b
 1179   g :: C a b => a -> b -> ()
 1180   f :: C a b => a -> b -> ()
 1181   f xa xb =
 1182       let loop = g xa
 1183       in loop xb
 1184 
 1185 We will first try to infer a type for loop, and we will succeed:
 1186     C a b' => b' -> ()
 1187 Subsequently, we will type check (loop xb) and all is good. But,
 1188 recall that we have to solve a final implication constraint:
 1189     C a b => (C a b' => .... cts from body of loop .... ))
 1190 And now we have a problem as we will generate an equality b ~ b' and fail to
 1191 solve it.
 1192 
 1193 
 1194 ************************************************************************
 1195 *                                                                      *
 1196                 Irreducible predicate errors
 1197 *                                                                      *
 1198 ************************************************************************
 1199 -}
 1200 
 1201 mkIrredErr :: ReportErrCtxt -> [Ct] -> TcM Report
 1202 mkIrredErr ctxt cts
 1203   = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
 1204        ; let orig = ctOrigin ct1
 1205              msg  = couldNotDeduce (getUserGivens ctxt) (map ctPred cts, orig)
 1206        ; return $ msg `mappend` mk_relevant_bindings binds_msg }
 1207   where
 1208     (ct1:_) = cts
 1209 
 1210 {- Note [Constructing Hole Errors]
 1211 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1212 
 1213 Whether or not 'mkHoleError' returns an error is not influenced by cec_suppress. In other terms,
 1214 these "hole" errors are /not/ suppressed by cec_suppress. We want to see them!
 1215 
 1216 There are two cases to consider:
 1217 
 1218 1. For out-of-scope variables we always report an error, unless -fdefer-out-of-scope-variables is on,
 1219    in which case the messages are discarded. See also #12170 and #12406. If deferring, report a warning
 1220    only if -Wout-of-scope-variables is on.
 1221 
 1222 2. For the general case, when -XPartialTypeSignatures is on, warnings (instead of errors) are generated
 1223    for holes in partial type signatures, unless -Wpartial-type-signatures is not on, in which case
 1224    the messages are discarded. If deferring, report a warning only if -Wtyped-holes is on.
 1225 
 1226 The above can be summarised into the following table:
 1227 
 1228 | Hole Type    | Active Flags                                             | Outcome          |
 1229 |--------------|----------------------------------------------------------|------------------|
 1230 | out-of-scope | None                                                     | Error            |
 1231 | out-of-scope | -fdefer-out-of-scope-variables, -Wout-of-scope-variables | Warning          |
 1232 | out-of-scope | -fdefer-out-of-scope-variables                           | Ignore (discard) |
 1233 | type         | None                                                     | Error            |
 1234 | type         | -XPartialTypeSignatures, -Wpartial-type-signatures       | Warning          |
 1235 | type         | -XPartialTypeSignatures                                  | Ignore (discard) |
 1236 | expression   | None                                                     | Error            |
 1237 | expression   | -Wdefer-typed-holes, -Wtyped-holes                       | Warning          |
 1238 | expression   | -Wdefer-typed-holes                                      | Ignore (discard) |
 1239 
 1240 See also 'reportUnsolved'.
 1241 
 1242 -}
 1243 
 1244 ----------------
 1245 -- | Constructs a new hole error, unless this is deferred. See Note [Constructing Hole Errors].
 1246 mkHoleError :: NameEnv Type -> [Ct] -> ReportErrCtxt -> Hole -> TcM (MsgEnvelope TcRnMessage)
 1247 mkHoleError _ _tidy_simples ctxt hole@(Hole { hole_occ = occ
 1248                                            , hole_ty = hole_ty
 1249                                            , hole_loc = ct_loc })
 1250   | isOutOfScopeHole hole
 1251   = do { dflags  <- getDynFlags
 1252        ; rdr_env <- getGlobalRdrEnv
 1253        ; imp_info <- getImports
 1254        ; curr_mod <- getModule
 1255        ; hpt <- getHpt
 1256        ; let err = important out_of_scope_msg `mappend`
 1257                    (mk_relevant_bindings $
 1258                      unknownNameSuggestions WL_Anything dflags hpt curr_mod rdr_env
 1259                        (tcl_rdr lcl_env) imp_info (mkRdrUnqual occ))
 1260 
 1261        ; maybeAddDeferredBindings ctxt hole err
 1262        ; mkErrorReportNC (cec_out_of_scope_holes ctxt) lcl_env err
 1263            -- Use NC variant: the context is generally not helpful here
 1264        }
 1265   where
 1266     herald | isDataOcc occ = text "Data constructor not in scope:"
 1267            | otherwise     = text "Variable not in scope:"
 1268 
 1269     out_of_scope_msg -- Print v :: ty only if the type has structure
 1270       | boring_type = hang herald 2 (ppr occ)
 1271       | otherwise   = hang herald 2 (pp_occ_with_type occ hole_ty)
 1272 
 1273     lcl_env     = ctLocEnv ct_loc
 1274     boring_type = isTyVarTy hole_ty
 1275 
 1276  -- general case: not an out-of-scope error
 1277 mkHoleError lcl_name_cache tidy_simples ctxt hole@(Hole { hole_occ = occ
 1278                                          , hole_ty = hole_ty
 1279                                          , hole_sort = sort
 1280                                          , hole_loc = ct_loc })
 1281   = do { binds_msg
 1282            <- relevant_bindings False lcl_env lcl_name_cache (tyCoVarsOfType hole_ty)
 1283                -- The 'False' means "don't filter the bindings"; see Trac #8191
 1284 
 1285        ; show_hole_constraints <- goptM Opt_ShowHoleConstraints
 1286        ; let constraints_msg
 1287                | ExprHole _ <- sort, show_hole_constraints
 1288                = givenConstraintsMsg ctxt
 1289                | otherwise
 1290                = empty
 1291 
 1292        ; show_valid_hole_fits <- goptM Opt_ShowValidHoleFits
 1293        ; (ctxt, sub_msg) <- if show_valid_hole_fits
 1294                             then validHoleFits ctxt tidy_simples hole
 1295                             else return (ctxt, empty)
 1296 
 1297        ; let err = important hole_msg `mappend`
 1298                    mk_relevant_bindings (binds_msg $$ constraints_msg) `mappend`
 1299                    valid_hole_fits sub_msg
 1300 
 1301        ; maybeAddDeferredBindings ctxt hole err
 1302 
 1303        ; let holes | ExprHole _ <- sort = cec_expr_holes ctxt
 1304                    | otherwise          = cec_type_holes ctxt
 1305        ; mkErrorReport holes ctxt lcl_env err
 1306        }
 1307 
 1308   where
 1309     lcl_env     = ctLocEnv ct_loc
 1310     hole_kind   = tcTypeKind hole_ty
 1311     tyvars      = tyCoVarsOfTypeList hole_ty
 1312 
 1313     hole_msg = case sort of
 1314       ExprHole _ -> vcat [ hang (text "Found hole:")
 1315                             2 (pp_occ_with_type occ hole_ty)
 1316                          , tyvars_msg, expr_hole_hint ]
 1317       TypeHole -> vcat [ hang (text "Found type wildcard" <+> quotes (ppr occ))
 1318                             2 (text "standing for" <+> quotes pp_hole_type_with_kind)
 1319                        , tyvars_msg, type_hole_hint ]
 1320       ConstraintHole -> vcat [ hang (text "Found extra-constraints wildcard standing for")
 1321                                   2 (quotes $ pprType hole_ty)  -- always kind constraint
 1322                              , tyvars_msg, type_hole_hint ]
 1323 
 1324     pp_hole_type_with_kind
 1325       | isLiftedTypeKind hole_kind
 1326         || isCoVarType hole_ty -- Don't print the kind of unlifted
 1327                                -- equalities (#15039)
 1328       = pprType hole_ty
 1329       | otherwise
 1330       = pprType hole_ty <+> dcolon <+> pprKind hole_kind
 1331 
 1332     tyvars_msg = ppUnless (null tyvars) $
 1333                  text "Where:" <+> (vcat (map loc_msg other_tvs)
 1334                                     $$ pprSkols ctxt skol_tvs)
 1335        where
 1336          (skol_tvs, other_tvs) = partition is_skol tyvars
 1337          is_skol tv = isTcTyVar tv && isSkolemTyVar tv
 1338                       -- Coercion variables can be free in the
 1339                       -- hole, via kind casts
 1340 
 1341     type_hole_hint
 1342          | ErrorWithoutFlag <- cec_type_holes ctxt
 1343          = text "To use the inferred type, enable PartialTypeSignatures"
 1344          | otherwise
 1345          = empty
 1346 
 1347     expr_hole_hint                       -- Give hint for, say,   f x = _x
 1348          | lengthFS (occNameFS occ) > 1  -- Don't give this hint for plain "_"
 1349          = text "Or perhaps" <+> quotes (ppr occ)
 1350            <+> text "is mis-spelled, or not in scope"
 1351          | otherwise
 1352          = empty
 1353 
 1354     loc_msg tv
 1355        | isTyVar tv
 1356        = case tcTyVarDetails tv of
 1357            MetaTv {} -> quotes (ppr tv) <+> text "is an ambiguous type variable"
 1358            _         -> empty  -- Skolems dealt with already
 1359        | otherwise  -- A coercion variable can be free in the hole type
 1360        = ppWhenOption sdocPrintExplicitCoercions $
 1361            quotes (ppr tv) <+> text "is a coercion variable"
 1362 
 1363 
 1364 {- Note [Adding deferred bindings]
 1365 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1366 
 1367 When working with typed holes we have to deal with the case where
 1368 we want holes to be reported as warnings to users during compile time but
 1369 as errors during runtime. Therefore, we have to call 'maybeAddDeferredBindings'
 1370 so that the correct 'Severity' can be computed out of that later on.
 1371 
 1372 -}
 1373 
 1374 
 1375 -- | Adds deferred bindings (as errors).
 1376 -- See Note [Adding deferred bindings].
 1377 maybeAddDeferredBindings :: ReportErrCtxt
 1378                          -> Hole
 1379                          -> Report
 1380                          -> TcM ()
 1381 maybeAddDeferredBindings ctxt hole report = do
 1382   case hole_sort hole of
 1383     ExprHole (HER ref ref_ty _) -> do
 1384       -- Only add bindings for holes in expressions
 1385       -- not for holes in partial type signatures
 1386       -- cf. addDeferredBinding
 1387       when (deferringAnyBindings ctxt) $ do
 1388         err_tm <- mkErrorTerm ctxt (hole_loc hole) ref_ty report
 1389           -- NB: ref_ty, not hole_ty. hole_ty might be rewritten.
 1390           -- See Note [Holes] in GHC.Tc.Types.Constraint
 1391         writeMutVar ref err_tm
 1392     _ -> pure ()
 1393 
 1394 pp_occ_with_type :: OccName -> Type -> SDoc
 1395 pp_occ_with_type occ hole_ty = hang (pprPrefixOcc occ) 2 (dcolon <+> pprType hole_ty)
 1396 
 1397 -- We unwrap the ReportErrCtxt here, to avoid introducing a loop in module
 1398 -- imports
 1399 validHoleFits :: ReportErrCtxt -- The context we're in, i.e. the
 1400                                         -- implications and the tidy environment
 1401                        -> [Ct]          -- Unsolved simple constraints
 1402                        -> Hole          -- The hole
 1403                        -> TcM (ReportErrCtxt, SDoc) -- We return the new context
 1404                                                     -- with a possibly updated
 1405                                                     -- tidy environment, and
 1406                                                     -- the message.
 1407 validHoleFits ctxt@(CEC {cec_encl = implics
 1408                              , cec_tidy = lcl_env}) simps hole
 1409   = do { (tidy_env, msg) <- findValidHoleFits lcl_env implics simps hole
 1410        ; return (ctxt {cec_tidy = tidy_env}, msg) }
 1411 
 1412 -- See Note [Constraints include ...]
 1413 givenConstraintsMsg :: ReportErrCtxt -> SDoc
 1414 givenConstraintsMsg ctxt =
 1415     let constraints :: [(Type, RealSrcSpan)]
 1416         constraints =
 1417           do { implic@Implic{ ic_given = given } <- cec_encl ctxt
 1418              ; constraint <- given
 1419              ; return (varType constraint, tcl_loc (ic_env implic)) }
 1420 
 1421         pprConstraint (constraint, loc) =
 1422           ppr constraint <+> nest 2 (parens (text "from" <+> ppr loc))
 1423 
 1424     in ppUnless (null constraints) $
 1425          hang (text "Constraints include")
 1426             2 (vcat $ map pprConstraint constraints)
 1427 
 1428 ----------------
 1429 mkIPErr :: ReportErrCtxt -> [Ct] -> TcM Report
 1430 mkIPErr ctxt cts
 1431   = do { (ctxt, binds_msg, ct1) <- relevantBindings True ctxt ct1
 1432        ; let orig    = ctOrigin ct1
 1433              preds   = map ctPred cts
 1434              givens  = getUserGivens ctxt
 1435              msg | null givens
 1436                  = important $ addArising orig $
 1437                    sep [ text "Unbound implicit parameter" <> plural cts
 1438                        , nest 2 (pprParendTheta preds) ]
 1439                  | otherwise
 1440                  = couldNotDeduce givens (preds, orig)
 1441 
 1442        ; return $ msg `mappend` mk_relevant_bindings binds_msg }
 1443   where
 1444     (ct1:_) = cts
 1445 
 1446 ----------------
 1447 
 1448 -- | Create a user-facing error message for unsolved @'Concrete#' ki@
 1449 -- Wanted constraints arising from representation-polymorphism checks.
 1450 --
 1451 -- See Note [Reporting representation-polymorphism errors] in GHC.Tc.Types.Origin.
 1452 mkFRRErr :: ReportErrCtxt -> [Ct] -> TcM Report
 1453 mkFRRErr ctxt cts
 1454   = do { -- Zonking/tidying.
 1455        ; origs <-
 1456            -- Zonk/tidy the 'CtOrigin's.
 1457            zonkTidyOrigins (cec_tidy ctxt) (map ctOrigin cts)
 1458              <&>
 1459            -- Then remove duplicates: only retain one 'CtOrigin' per representation-polymorphic type.
 1460           (nubOrdBy (nonDetCmpType `on` frr_type) . snd)
 1461 
 1462         -- Obtain all the errors we want to report (constraints with FixedRuntimeRep origin),
 1463         -- with the corresponding types:
 1464         --   ty1 :: TYPE rep1, ty2 :: TYPE rep2, ...
 1465        ; let tys = map frr_type origs
 1466              kis = map typeKind tys
 1467 
 1468         -- Assemble the error message: pair up each origin with the corresponding type, e.g.
 1469         --   • FixedRuntimeRep origin msg 1 ...
 1470         --       a :: TYPE r1
 1471         --   • FixedRuntimeRep origin msg 2 ...
 1472         --       b :: TYPE r2
 1473 
 1474              combine_origin_ty_ki :: CtOrigin -> Type -> Kind -> SDoc
 1475              combine_origin_ty_ki orig ty ki =
 1476                -- Add bullet points if there is more than one error.
 1477                (if length tys > 1 then (bullet <+>) else id) $
 1478                  vcat [pprArising orig <> colon
 1479                       ,nest 2 $ ppr ty <+> dcolon <+> pprWithTYPE ki]
 1480 
 1481              msg :: SDoc
 1482              msg = vcat $ zipWith3 combine_origin_ty_ki origs tys kis
 1483 
 1484        ; return $ important msg }
 1485   where
 1486 
 1487     frr_type :: CtOrigin -> Type
 1488     frr_type (FixedRuntimeRepOrigin ty _) = ty
 1489     frr_type orig
 1490       = pprPanic "mkFRRErr: not a FixedRuntimeRep origin"
 1491           (text "origin =" <+> ppr orig)
 1492 
 1493 {-
 1494 Note [Constraints include ...]
 1495 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1496 'givenConstraintsMsg' returns the "Constraints include ..." message enabled by
 1497 -fshow-hole-constraints. For example, the following hole:
 1498 
 1499     foo :: (Eq a, Show a) => a -> String
 1500     foo x = _
 1501 
 1502 would generate the message:
 1503 
 1504     Constraints include
 1505       Eq a (from foo.hs:1:1-36)
 1506       Show a (from foo.hs:1:1-36)
 1507 
 1508 Constraints are displayed in order from innermost (closest to the hole) to
 1509 outermost. There's currently no filtering or elimination of duplicates.
 1510 
 1511 ************************************************************************
 1512 *                                                                      *
 1513                 Equality errors
 1514 *                                                                      *
 1515 ************************************************************************
 1516 
 1517 Note [Inaccessible code]
 1518 ~~~~~~~~~~~~~~~~~~~~~~~~
 1519 Consider
 1520    data T a where
 1521      T1 :: T a
 1522      T2 :: T Bool
 1523 
 1524    f :: (a ~ Int) => T a -> Int
 1525    f T1 = 3
 1526    f T2 = 4   -- Unreachable code
 1527 
 1528 Here the second equation is unreachable. The original constraint
 1529 (a~Int) from the signature gets rewritten by the pattern-match to
 1530 (Bool~Int), so the danger is that we report the error as coming from
 1531 the *signature* (#7293).  So, for Given errors we replace the
 1532 env (and hence src-loc) on its CtLoc with that from the immediately
 1533 enclosing implication.
 1534 
 1535 Note [Error messages for untouchables]
 1536 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1537 Consider (#9109)
 1538   data G a where { GBool :: G Bool }
 1539   foo x = case x of GBool -> True
 1540 
 1541 Here we can't solve (t ~ Bool), where t is the untouchable result
 1542 meta-var 't', because of the (a ~ Bool) from the pattern match.
 1543 So we infer the type
 1544    f :: forall a t. G a -> t
 1545 making the meta-var 't' into a skolem.  So when we come to report
 1546 the unsolved (t ~ Bool), t won't look like an untouchable meta-var
 1547 any more.  So we don't assert that it is.
 1548 -}
 1549 
 1550 -- Don't have multiple equality errors from the same location
 1551 -- E.g.   (Int,Bool) ~ (Bool,Int)   one error will do!
 1552 mkEqErr :: ReportErrCtxt -> [Ct] -> TcM Report
 1553 mkEqErr ctxt (ct:_) = mkEqErr1 ctxt ct
 1554 mkEqErr _ [] = panic "mkEqErr"
 1555 
 1556 mkEqErr1 :: ReportErrCtxt -> Ct -> TcM Report
 1557 mkEqErr1 ctxt ct   -- Wanted or derived;
 1558                    -- givens handled in mkGivenErrorReporter
 1559   = do { (ctxt, binds_msg, ct) <- relevantBindings True ctxt ct
 1560        ; rdr_env <- getGlobalRdrEnv
 1561        ; fam_envs <- tcGetFamInstEnvs
 1562        ; let coercible_msg = case ctEqRel ct of
 1563                NomEq  -> empty
 1564                ReprEq -> mkCoercibleExplanation rdr_env fam_envs ty1 ty2
 1565        ; traceTc "mkEqErr1" (ppr ct $$ pprCtOrigin (ctOrigin ct))
 1566        ; let report = mconcat [ important coercible_msg
 1567                               , mk_relevant_bindings binds_msg]
 1568        ; mkEqErr_help ctxt report ct ty1 ty2 }
 1569   where
 1570     (ty1, ty2) = getEqPredTys (ctPred ct)
 1571 
 1572 -- | This function tries to reconstruct why a "Coercible ty1 ty2" constraint
 1573 -- is left over.
 1574 mkCoercibleExplanation :: GlobalRdrEnv -> FamInstEnvs
 1575                        -> TcType -> TcType -> SDoc
 1576 mkCoercibleExplanation rdr_env fam_envs ty1 ty2
 1577   | Just (tc, tys) <- tcSplitTyConApp_maybe ty1
 1578   , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
 1579   , Just msg <- coercible_msg_for_tycon rep_tc
 1580   = msg
 1581   | Just (tc, tys) <- splitTyConApp_maybe ty2
 1582   , (rep_tc, _, _) <- tcLookupDataFamInst fam_envs tc tys
 1583   , Just msg <- coercible_msg_for_tycon rep_tc
 1584   = msg
 1585   | Just (s1, _) <- tcSplitAppTy_maybe ty1
 1586   , Just (s2, _) <- tcSplitAppTy_maybe ty2
 1587   , s1 `eqType` s2
 1588   , has_unknown_roles s1
 1589   = hang (text "NB: We cannot know what roles the parameters to" <+>
 1590           quotes (ppr s1) <+> text "have;")
 1591        2 (text "we must assume that the role is nominal")
 1592   | otherwise
 1593   = empty
 1594   where
 1595     coercible_msg_for_tycon tc
 1596         | isAbstractTyCon tc
 1597         = Just $ hsep [ text "NB: The type constructor"
 1598                       , quotes (pprSourceTyCon tc)
 1599                       , text "is abstract" ]
 1600         | isNewTyCon tc
 1601         , [data_con] <- tyConDataCons tc
 1602         , let dc_name = dataConName data_con
 1603         , isNothing (lookupGRE_Name rdr_env dc_name)
 1604         = Just $ hang (text "The data constructor" <+> quotes (ppr dc_name))
 1605                     2 (sep [ text "of newtype" <+> quotes (pprSourceTyCon tc)
 1606                            , text "is not in scope" ])
 1607         | otherwise = Nothing
 1608 
 1609     has_unknown_roles ty
 1610       | Just (tc, tys) <- tcSplitTyConApp_maybe ty
 1611       = tys `lengthAtLeast` tyConArity tc  -- oversaturated tycon
 1612       | Just (s, _) <- tcSplitAppTy_maybe ty
 1613       = has_unknown_roles s
 1614       | isTyVarTy ty
 1615       = True
 1616       | otherwise
 1617       = False
 1618 
 1619 mkEqErr_help :: ReportErrCtxt -> Report
 1620              -> Ct
 1621              -> TcType -> TcType -> TcM Report
 1622 mkEqErr_help ctxt report ct ty1 ty2
 1623   | Just (tv1, _) <- tcGetCastedTyVar_maybe ty1
 1624   = mkTyVarEqErr ctxt report ct tv1 ty2
 1625   | Just (tv2, _) <- tcGetCastedTyVar_maybe ty2
 1626   = mkTyVarEqErr ctxt report ct tv2 ty1
 1627   | otherwise
 1628   = return $ reportEqErr ctxt report ct ty1 ty2
 1629 
 1630 reportEqErr :: ReportErrCtxt -> Report
 1631             -> Ct
 1632             -> TcType -> TcType -> Report
 1633 reportEqErr ctxt report ct ty1 ty2
 1634   = mconcat [misMatch, report, eqInfo]
 1635   where
 1636     misMatch = misMatchOrCND False ctxt ct ty1 ty2
 1637     eqInfo   = mkEqInfoMsg ct ty1 ty2
 1638 
 1639 mkTyVarEqErr :: ReportErrCtxt -> Report -> Ct
 1640              -> TcTyVar -> TcType -> TcM Report
 1641 -- tv1 and ty2 are already tidied
 1642 mkTyVarEqErr ctxt report ct tv1 ty2
 1643   = do { traceTc "mkTyVarEqErr" (ppr ct $$ ppr tv1 $$ ppr ty2)
 1644        ; dflags <- getDynFlags
 1645        ; return $ mkTyVarEqErr' dflags ctxt report ct tv1 ty2 }
 1646 
 1647 mkTyVarEqErr' :: DynFlags -> ReportErrCtxt -> Report -> Ct
 1648               -> TcTyVar -> TcType -> Report
 1649 mkTyVarEqErr' dflags ctxt report ct tv1 ty2
 1650      -- impredicativity is a simple error to understand; try it first
 1651   | check_eq_result `cterHasProblem` cteImpredicative
 1652   = let msg = vcat [ (if isSkolemTyVar tv1
 1653                       then text "Cannot equate type variable"
 1654                       else text "Cannot instantiate unification variable")
 1655                      <+> quotes (ppr tv1)
 1656                    , hang (text "with a" <+> what <+> text "involving polytypes:") 2 (ppr ty2) ]
 1657     in
 1658        -- Unlike the other reports, this discards the old 'report_important'
 1659        -- instead of augmenting it.  This is because the details are not likely
 1660        -- to be helpful since this is just an unimplemented feature.
 1661     mconcat [ headline_msg
 1662             , important msg
 1663             , if isSkolemTyVar tv1 then extraTyVarEqInfo ctxt tv1 ty2 else mempty
 1664             , report ]
 1665 
 1666   | isSkolemTyVar tv1  -- ty2 won't be a meta-tyvar; we would have
 1667                        -- swapped in Solver.Canonical.canEqTyVarHomo
 1668     || isTyVarTyVar tv1 && not (isTyVarTy ty2)
 1669     || ctEqRel ct == ReprEq
 1670      -- The cases below don't really apply to ReprEq (except occurs check)
 1671   = mconcat [ headline_msg
 1672             , extraTyVarEqInfo ctxt tv1 ty2
 1673             , suggestAddSig ctxt ty1 ty2
 1674             , report
 1675             ]
 1676 
 1677   | cterHasOccursCheck check_eq_result
 1678     -- We report an "occurs check" even for  a ~ F t a, where F is a type
 1679     -- function; it's not insoluble (because in principle F could reduce)
 1680     -- but we have certainly been unable to solve it
 1681   = let extra2   = mkEqInfoMsg ct ty1 ty2
 1682 
 1683         interesting_tyvars = filter (not . noFreeVarsOfType . tyVarKind) $
 1684                              filter isTyVar $
 1685                              fvVarList $
 1686                              tyCoFVsOfType ty1 `unionFV` tyCoFVsOfType ty2
 1687         extra3 = mk_relevant_bindings $
 1688                  ppWhen (not (null interesting_tyvars)) $
 1689                  hang (text "Type variable kinds:") 2 $
 1690                  vcat (map (tyvar_binding . tidyTyCoVarOcc (cec_tidy ctxt))
 1691                            interesting_tyvars)
 1692 
 1693         tyvar_binding tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv)
 1694     in
 1695     mconcat [headline_msg, extra2, extra3, report]
 1696 
 1697   -- If the immediately-enclosing implication has 'tv' a skolem, and
 1698   -- we know by now its an InferSkol kind of skolem, then presumably
 1699   -- it started life as a TyVarTv, else it'd have been unified, given
 1700   -- that there's no occurs-check or forall problem
 1701   | (implic:_) <- cec_encl ctxt
 1702   , Implic { ic_skols = skols } <- implic
 1703   , tv1 `elem` skols
 1704   = mconcat [ misMatchMsg ctxt ct ty1 ty2
 1705             , extraTyVarEqInfo ctxt tv1 ty2
 1706             , report
 1707             ]
 1708 
 1709   -- Check for skolem escape
 1710   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
 1711   , Implic { ic_skols = skols, ic_info = skol_info } <- implic
 1712   , let esc_skols = filter (`elemVarSet` (tyCoVarsOfType ty2)) skols
 1713   , not (null esc_skols)
 1714   = let msg = misMatchMsg ctxt ct ty1 ty2
 1715         esc_doc = sep [ text "because" <+> what <+> text "variable" <> plural esc_skols
 1716                         <+> pprQuotedList esc_skols
 1717                       , text "would escape" <+>
 1718                         if isSingleton esc_skols then text "its scope"
 1719                                                  else text "their scope" ]
 1720         tv_extra = important $
 1721                    vcat [ nest 2 $ esc_doc
 1722                         , sep [ (if isSingleton esc_skols
 1723                                  then text "This (rigid, skolem)" <+>
 1724                                       what <+> text "variable is"
 1725                                  else text "These (rigid, skolem)" <+>
 1726                                       what <+> text "variables are")
 1727                           <+> text "bound by"
 1728                         , nest 2 $ ppr skol_info
 1729                         , nest 2 $ text "at" <+>
 1730                           ppr (tcl_loc (ic_env implic)) ] ]
 1731     in
 1732     mconcat [msg, tv_extra, report]
 1733 
 1734   -- Nastiest case: attempt to unify an untouchable variable
 1735   -- So tv is a meta tyvar (or started that way before we
 1736   -- generalised it).  So presumably it is an *untouchable*
 1737   -- meta tyvar or a TyVarTv, else it'd have been unified
 1738   -- See Note [Error messages for untouchables]
 1739   | (implic:_) <- cec_encl ctxt   -- Get the innermost context
 1740   , Implic { ic_given = given, ic_tclvl = lvl, ic_info = skol_info } <- implic
 1741   = assertPpr (not (isTouchableMetaTyVar lvl tv1))
 1742               (ppr tv1 $$ ppr lvl) $  -- See Note [Error messages for untouchables]
 1743     let msg         = misMatchMsg ctxt ct ty1 ty2
 1744         tclvl_extra = important $
 1745              nest 2 $
 1746              sep [ quotes (ppr tv1) <+> text "is untouchable"
 1747                  , nest 2 $ text "inside the constraints:" <+> pprEvVarTheta given
 1748                  , nest 2 $ text "bound by" <+> ppr skol_info
 1749                  , nest 2 $ text "at" <+>
 1750                    ppr (tcl_loc (ic_env implic)) ]
 1751         tv_extra = extraTyVarEqInfo ctxt tv1 ty2
 1752         add_sig  = suggestAddSig ctxt ty1 ty2
 1753     in
 1754     mconcat [msg, tclvl_extra, tv_extra, add_sig, report]
 1755 
 1756   | otherwise
 1757   = reportEqErr ctxt report ct (mkTyVarTy tv1) ty2
 1758         -- This *can* happen (#6123)
 1759         -- Consider an ambiguous top-level constraint (a ~ F a)
 1760         -- Not an occurs check, because F is a type function.
 1761   where
 1762     headline_msg = misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2
 1763 
 1764     ty1 = mkTyVarTy tv1
 1765 
 1766     check_eq_result = case ct of
 1767       CIrredCan { cc_reason = NonCanonicalReason result } -> result
 1768       CIrredCan { cc_reason = HoleBlockerReason {} }      -> cteProblem cteHoleBlocker
 1769       _ -> checkTyVarEq dflags tv1 ty2
 1770         -- in T2627b, we report an error for F (F a0) ~ a0. Note that the type
 1771         -- variable is on the right, so we don't get useful info for the CIrredCan,
 1772         -- and have to compute the result of checkTyVarEq here.
 1773 
 1774 
 1775     insoluble_occurs_check = check_eq_result `cterHasProblem` cteInsolubleOccurs
 1776 
 1777     what = text $ levelString $
 1778            ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel
 1779 
 1780 levelString :: TypeOrKind -> String
 1781 levelString TypeLevel = "type"
 1782 levelString KindLevel = "kind"
 1783 
 1784 mkEqInfoMsg :: Ct -> TcType -> TcType -> Report
 1785 -- Report (a) ambiguity if either side is a type function application
 1786 --            e.g. F a0 ~ Int
 1787 --        (b) warning about injectivity if both sides are the same
 1788 --            type function application   F a ~ F b
 1789 --            See Note [Non-injective type functions]
 1790 mkEqInfoMsg ct ty1 ty2
 1791   = important (tyfun_msg $$ ambig_msg)
 1792   where
 1793     mb_fun1 = isTyFun_maybe ty1
 1794     mb_fun2 = isTyFun_maybe ty2
 1795 
 1796     ambig_msg | isJust mb_fun1 || isJust mb_fun2
 1797               = snd (mkAmbigMsg False ct)
 1798               | otherwise = empty
 1799 
 1800     tyfun_msg | Just tc1 <- mb_fun1
 1801               , Just tc2 <- mb_fun2
 1802               , tc1 == tc2
 1803               , not (isInjectiveTyCon tc1 Nominal)
 1804               = text "NB:" <+> quotes (ppr tc1)
 1805                 <+> text "is a non-injective type family"
 1806               | otherwise = empty
 1807 
 1808 misMatchOrCND :: Bool -> ReportErrCtxt -> Ct
 1809               -> TcType -> TcType -> Report
 1810 -- If oriented then ty1 is actual, ty2 is expected
 1811 misMatchOrCND insoluble_occurs_check ctxt ct ty1 ty2
 1812   | insoluble_occurs_check  -- See Note [Insoluble occurs check]
 1813     || (isRigidTy ty1 && isRigidTy ty2)
 1814     || isGivenCt ct
 1815     || null givens
 1816   = -- If the equality is unconditionally insoluble
 1817     -- or there is no context, don't report the context
 1818     misMatchMsg ctxt ct ty1 ty2
 1819 
 1820   | otherwise
 1821   = mconcat [ couldNotDeduce givens ([eq_pred], orig)
 1822             , important $ mk_supplementary_ea_msg ctxt level ty1 ty2 orig ]
 1823   where
 1824     ev      = ctEvidence ct
 1825     eq_pred = ctEvPred ev
 1826     orig    = ctEvOrigin ev
 1827     level   = ctLocTypeOrKind_maybe (ctEvLoc ev) `orElse` TypeLevel
 1828     givens  = [ given | given <- getUserGivens ctxt, ic_given_eqs given /= NoGivenEqs ]
 1829               -- Keep only UserGivens that have some equalities.
 1830               -- See Note [Suppress redundant givens during error reporting]
 1831 
 1832 couldNotDeduce :: [UserGiven] -> (ThetaType, CtOrigin) -> Report
 1833 couldNotDeduce givens (wanteds, orig)
 1834   = important $
 1835     vcat [ addArising orig (text "Could not deduce:" <+> pprTheta wanteds)
 1836          , vcat (pp_givens givens)]
 1837 
 1838 pp_givens :: [UserGiven] -> [SDoc]
 1839 pp_givens givens
 1840    = case givens of
 1841          []     -> []
 1842          (g:gs) ->      ppr_given (text "from the context:") g
 1843                  : map (ppr_given (text "or from:")) gs
 1844     where
 1845        ppr_given herald implic@(Implic { ic_given = gs, ic_info = skol_info })
 1846            = hang (herald <+> pprEvVarTheta (mkMinimalBySCs evVarPred gs))
 1847              -- See Note [Suppress redundant givens during error reporting]
 1848              -- for why we use mkMinimalBySCs above.
 1849                 2 (sep [ text "bound by" <+> ppr skol_info
 1850                        , text "at" <+> ppr (tcl_loc (ic_env implic)) ])
 1851 
 1852 -- These are for the "blocked" equalities, as described in TcCanonical
 1853 -- Note [Equalities with incompatible kinds], wrinkle (2). There should
 1854 -- always be another unsolved wanted around, which will ordinarily suppress
 1855 -- this message. But this can still be printed out with -fdefer-type-errors
 1856 -- (sigh), so we must produce a message.
 1857 mkBlockedEqErr :: ReportErrCtxt -> [Ct] -> TcM Report
 1858 mkBlockedEqErr _ (ct:_) = return $ important msg
 1859   where
 1860     msg = vcat [ hang (text "Cannot use equality for substitution:")
 1861                    2 (ppr (ctPred ct))
 1862                , text "Doing so would be ill-kinded." ]
 1863           -- This is a terrible message. Perhaps worse, if the user
 1864           -- has -fprint-explicit-kinds on, they will see that the two
 1865           -- sides have the same kind, as there is an invisible cast.
 1866           -- I really don't know how to do better.
 1867 mkBlockedEqErr _ [] = panic "mkBlockedEqErr no constraints"
 1868 
 1869 {-
 1870 Note [Suppress redundant givens during error reporting]
 1871 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 1872 When GHC is unable to solve a constraint and prints out an error message, it
 1873 will print out what given constraints are in scope to provide some context to
 1874 the programmer. But we shouldn't print out /every/ given, since some of them
 1875 are not terribly helpful to diagnose type errors. Consider this example:
 1876 
 1877   foo :: Int :~: Int -> a :~: b -> a :~: c
 1878   foo Refl Refl = Refl
 1879 
 1880 When reporting that GHC can't solve (a ~ c), there are two givens in scope:
 1881 (Int ~ Int) and (a ~ b). But (Int ~ Int) is trivially soluble (i.e.,
 1882 redundant), so it's not terribly useful to report it in an error message.
 1883 To accomplish this, we discard any Implications that do not bind any
 1884 equalities by filtering the `givens` selected in `misMatchOrCND` (based on
 1885 the `ic_given_eqs` field of the Implication). Note that we discard givens
 1886 that have no equalities whatsoever, but we want to keep ones with only *local*
 1887 equalities, as these may be helpful to the user in understanding what went
 1888 wrong.
 1889 
 1890 But this is not enough to avoid all redundant givens! Consider this example,
 1891 from #15361:
 1892 
 1893   goo :: forall (a :: Type) (b :: Type) (c :: Type).
 1894          a :~~: b -> a :~~: c
 1895   goo HRefl = HRefl
 1896 
 1897 Matching on HRefl brings the /single/ given (* ~ *, a ~ b) into scope.
 1898 The (* ~ *) part arises due the kinds of (:~~:) being unified. More
 1899 importantly, (* ~ *) is redundant, so we'd like not to report it. However,
 1900 the Implication (* ~ *, a ~ b) /does/ bind an equality (as reported by its
 1901 ic_given_eqs field), so the test above will keep it wholesale.
 1902 
 1903 To refine this given, we apply mkMinimalBySCs on it to extract just the (a ~ b)
 1904 part. This works because mkMinimalBySCs eliminates reflexive equalities in
 1905 addition to superclasses (see Note [Remove redundant provided dicts]
 1906 in GHC.Tc.TyCl.PatSyn).
 1907 -}
 1908 
 1909 extraTyVarEqInfo :: ReportErrCtxt -> TcTyVar -> TcType -> Report
 1910 -- Add on extra info about skolem constants
 1911 -- NB: The types themselves are already tidied
 1912 extraTyVarEqInfo ctxt tv1 ty2
 1913   = important (extraTyVarInfo ctxt tv1 $$ ty_extra ty2)
 1914   where
 1915     ty_extra ty = case tcGetCastedTyVar_maybe ty of
 1916                     Just (tv, _) -> extraTyVarInfo ctxt tv
 1917                     Nothing      -> empty
 1918 
 1919 extraTyVarInfo :: ReportErrCtxt -> TcTyVar -> SDoc
 1920 extraTyVarInfo ctxt tv
 1921   = assertPpr (isTyVar tv) (ppr tv) $
 1922     case tcTyVarDetails tv of
 1923           SkolemTv {}   -> pprSkols ctxt [tv]
 1924           RuntimeUnk {} -> quotes (ppr tv) <+> text "is an interactive-debugger skolem"
 1925           MetaTv {}     -> empty
 1926 
 1927 suggestAddSig :: ReportErrCtxt -> TcType -> TcType -> Report
 1928 -- See Note [Suggest adding a type signature]
 1929 suggestAddSig ctxt ty1 _ty2
 1930   | null inferred_bndrs   -- No let-bound inferred binders in context
 1931   = mempty
 1932   | [bndr] <- inferred_bndrs
 1933   = important $ text "Possible fix: add a type signature for" <+> quotes (ppr bndr)
 1934   | otherwise
 1935   = important $ text "Possible fix: add type signatures for some or all of" <+> (ppr inferred_bndrs)
 1936   where
 1937     inferred_bndrs = case tcGetTyVar_maybe ty1 of
 1938                        Just tv | isSkolemTyVar tv -> find (cec_encl ctxt) False tv
 1939                        _                          -> []
 1940 
 1941     -- 'find' returns the binders of an InferSkol for 'tv',
 1942     -- provided there is an intervening implication with
 1943     -- ic_given_eqs /= NoGivenEqs (i.e. a GADT match)
 1944     find [] _ _ = []
 1945     find (implic:implics) seen_eqs tv
 1946        | tv `elem` ic_skols implic
 1947        , InferSkol prs <- ic_info implic
 1948        , seen_eqs
 1949        = map fst prs
 1950        | otherwise
 1951        = find implics (seen_eqs || ic_given_eqs implic /= NoGivenEqs) tv
 1952 
 1953 --------------------
 1954 misMatchMsg :: ReportErrCtxt -> Ct -> TcType -> TcType -> Report
 1955 -- Types are already tidy
 1956 -- If oriented then ty1 is actual, ty2 is expected
 1957 misMatchMsg ctxt ct ty1 ty2
 1958   = important $
 1959     addArising orig $
 1960     pprWithExplicitKindsWhenMismatch ty1 ty2 orig $
 1961     sep [ case orig of
 1962             TypeEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig
 1963             KindEqOrigin {} -> tk_eq_msg ctxt ct ty1 ty2 orig
 1964             _ -> headline_eq_msg False ct ty1 ty2
 1965         , sameOccExtra ty2 ty1 ]
 1966   where
 1967     orig = ctOrigin ct
 1968 
 1969 headline_eq_msg :: Bool -> Ct -> Type -> Type -> SDoc
 1970 -- Generates the main "Could't match 't1' against 't2'
 1971 -- headline message
 1972 headline_eq_msg add_ea ct ty1 ty2
 1973 
 1974   | (isLiftedRuntimeRep ty1 && isUnliftedRuntimeRep ty2) ||
 1975     (isLiftedRuntimeRep ty2 && isUnliftedRuntimeRep ty1) ||
 1976     (isLiftedLevity ty1 && isUnliftedLevity ty2) ||
 1977     (isLiftedLevity ty2 && isUnliftedLevity ty1)
 1978   = text "Couldn't match a lifted type with an unlifted type"
 1979 
 1980   | isAtomicTy ty1 || isAtomicTy ty2
 1981   = -- Print with quotes
 1982     sep [ text herald1 <+> quotes (ppr ty1)
 1983         , nest padding $
 1984           text herald2 <+> quotes (ppr ty2) ]
 1985 
 1986   | otherwise
 1987   = -- Print with vertical layout
 1988     vcat [ text herald1 <> colon <+> ppr ty1
 1989          , nest padding $
 1990            text herald2 <> colon <+> ppr ty2 ]
 1991   where
 1992     herald1 = conc [ "Couldn't match"
 1993                    , if is_repr then "representation of" else ""
 1994                    , if add_ea then "expected"          else ""
 1995                    , what ]
 1996     herald2 = conc [ "with"
 1997                    , if is_repr then "that of"          else ""
 1998                    , if add_ea then ("actual " ++ what) else "" ]
 1999 
 2000     padding = length herald1 - length herald2
 2001 
 2002     is_repr = case ctEqRel ct of { ReprEq -> True; NomEq -> False }
 2003 
 2004     what = levelString (ctLocTypeOrKind_maybe (ctLoc ct) `orElse` TypeLevel)
 2005 
 2006     conc :: [String] -> String
 2007     conc = foldr1 add_space
 2008 
 2009     add_space :: String -> String -> String
 2010     add_space s1 s2 | null s1   = s2
 2011                     | null s2   = s1
 2012                     | otherwise = s1 ++ (' ' : s2)
 2013 
 2014 
 2015 tk_eq_msg :: ReportErrCtxt
 2016           -> Ct -> Type -> Type -> CtOrigin -> SDoc
 2017 tk_eq_msg ctxt ct ty1 ty2 orig@(TypeEqOrigin { uo_actual = act
 2018                                              , uo_expected = exp
 2019                                              , uo_thing = mb_thing })
 2020   -- We can use the TypeEqOrigin to
 2021   -- improve the error message quite a lot
 2022 
 2023   | isUnliftedTypeKind act, isLiftedTypeKind exp
 2024   = sep [ text "Expecting a lifted type, but"
 2025         , thing_msg mb_thing (text "an") (text "unlifted") ]
 2026 
 2027   | isLiftedTypeKind act, isUnliftedTypeKind exp
 2028   = sep [ text "Expecting an unlifted type, but"
 2029         , thing_msg mb_thing (text "a") (text "lifted") ]
 2030 
 2031   | tcIsLiftedTypeKind exp
 2032   = maybe_num_args_msg $$
 2033     sep [ text "Expected a type, but"
 2034         , case mb_thing of
 2035             Nothing    -> text "found something with kind"
 2036             Just thing -> quotes thing <+> text "has kind"
 2037         , quotes (pprWithTYPE act) ]
 2038 
 2039   | Just nargs_msg <- num_args_msg
 2040   = nargs_msg $$
 2041     mk_ea_msg ctxt (Just ct) level orig
 2042 
 2043   | -- pprTrace "check" (ppr ea_looks_same $$ ppr exp $$ ppr act $$ ppr ty1 $$ ppr ty2) $
 2044     ea_looks_same ty1 ty2 exp act
 2045   = mk_ea_msg ctxt (Just ct) level orig
 2046 
 2047   | otherwise  -- The mismatched types are /inside/ exp and act
 2048   = vcat [ headline_eq_msg False ct ty1 ty2
 2049          , mk_ea_msg ctxt Nothing level orig ]
 2050 
 2051   where
 2052     ct_loc = ctLoc ct
 2053     level  = ctLocTypeOrKind_maybe ct_loc `orElse` TypeLevel
 2054 
 2055     thing_msg (Just thing) _  levity = quotes thing <+> text "is" <+> levity
 2056     thing_msg Nothing      an levity = text "got" <+> an <+> levity <+> text "type"
 2057 
 2058     num_args_msg = case level of
 2059       KindLevel
 2060         | not (isMetaTyVarTy exp) && not (isMetaTyVarTy act)
 2061            -- if one is a meta-tyvar, then it's possible that the user
 2062            -- has asked for something impredicative, and we couldn't unify.
 2063            -- Don't bother with counting arguments.
 2064         -> let n_act = count_args act
 2065                n_exp = count_args exp in
 2066            case n_act - n_exp of
 2067              n | n > 0   -- we don't know how many args there are, so don't
 2068                          -- recommend removing args that aren't
 2069                , Just thing <- mb_thing
 2070                -> Just $ text "Expecting" <+> speakN (abs n) <+>
 2071                          more <+> quotes thing
 2072                where
 2073                  more
 2074                   | n == 1    = text "more argument to"
 2075                   | otherwise = text "more arguments to"  -- n > 1
 2076              _ -> Nothing
 2077 
 2078       _ -> Nothing
 2079 
 2080     maybe_num_args_msg = num_args_msg `orElse` empty
 2081 
 2082     count_args ty = count isVisibleBinder $ fst $ splitPiTys ty
 2083 
 2084 tk_eq_msg ctxt ct ty1 ty2
 2085           (KindEqOrigin cty1 cty2 sub_o mb_sub_t_or_k)
 2086   = vcat [ headline_eq_msg False ct ty1 ty2
 2087          , supplementary_msg ]
 2088   where
 2089     sub_t_or_k = mb_sub_t_or_k `orElse` TypeLevel
 2090     sub_whats  = text (levelString sub_t_or_k) <> char 's'
 2091                  -- "types" or "kinds"
 2092 
 2093     supplementary_msg
 2094       = sdocOption sdocPrintExplicitCoercions $ \printExplicitCoercions ->
 2095         if printExplicitCoercions
 2096            || not (cty1 `pickyEqType` cty2)
 2097           then vcat [ hang (text "When matching" <+> sub_whats)
 2098                           2 (vcat [ ppr cty1 <+> dcolon <+>
 2099                                    ppr (tcTypeKind cty1)
 2100                                  , ppr cty2 <+> dcolon <+>
 2101                                    ppr (tcTypeKind cty2) ])
 2102                     , mk_supplementary_ea_msg ctxt sub_t_or_k cty1 cty2 sub_o ]
 2103           else text "When matching the kind of" <+> quotes (ppr cty1)
 2104 
 2105 tk_eq_msg _ _ _ _ _ = panic "typeeq_mismatch_msg"
 2106 
 2107 ea_looks_same :: Type -> Type -> Type -> Type -> Bool
 2108 -- True if the faulting types (ty1, ty2) look the same as
 2109 -- the expected/actual types (exp, act).
 2110 -- If so, we don't want to redundantly report the latter
 2111 ea_looks_same ty1 ty2 exp act
 2112   = (act `looks_same` ty1 && exp `looks_same` ty2) ||
 2113     (exp `looks_same` ty1 && act `looks_same` ty2)
 2114   where
 2115     looks_same t1 t2 = t1 `pickyEqType` t2
 2116                     || t1 `eqType` liftedTypeKind && t2 `eqType` liftedTypeKind
 2117       -- pickyEqType is sensitive to synonyms, so only replies True
 2118       -- when the types really look the same.  However,
 2119       -- (TYPE 'LiftedRep) and Type both print the same way.
 2120 
 2121 mk_supplementary_ea_msg :: ReportErrCtxt -> TypeOrKind
 2122                         -> Type -> Type -> CtOrigin -> SDoc
 2123 mk_supplementary_ea_msg ctxt level ty1 ty2 orig
 2124   | TypeEqOrigin { uo_expected = exp, uo_actual = act } <- orig
 2125   , not (ea_looks_same ty1 ty2 exp act)
 2126   = mk_ea_msg ctxt Nothing level orig
 2127   | otherwise
 2128   = empty
 2129 
 2130 mk_ea_msg :: ReportErrCtxt -> Maybe Ct -> TypeOrKind -> CtOrigin -> SDoc
 2131 -- Constructs a "Couldn't match" message
 2132 -- The (Maybe Ct) says whether this is the main top-level message (Just)
 2133 --     or a supplementary message (Nothing)
 2134 mk_ea_msg ctxt at_top level
 2135           (TypeEqOrigin { uo_actual = act, uo_expected = exp, uo_thing = mb_thing })
 2136   | Just thing <- mb_thing
 2137   , KindLevel <- level
 2138   = hang (text "Expected" <+> kind_desc <> comma)
 2139        2 (text "but" <+> quotes thing <+> text "has kind" <+>
 2140           quotes (ppr act))
 2141 
 2142   | otherwise
 2143   = vcat [ case at_top of
 2144               Just ct -> headline_eq_msg True ct exp act
 2145               Nothing -> supplementary_ea_msg
 2146          , ppWhen expand_syns expandedTys ]
 2147 
 2148   where
 2149     supplementary_ea_msg = vcat [ text "Expected:" <+> ppr exp
 2150                                 , text "  Actual:" <+> ppr act ]
 2151 
 2152     kind_desc | tcIsConstraintKind exp = text "a constraint"
 2153               | Just arg <- kindRep_maybe exp  -- TYPE t0
 2154               , tcIsTyVarTy arg = sdocOption sdocPrintExplicitRuntimeReps $ \case
 2155                                    True  -> text "kind" <+> quotes (ppr exp)
 2156                                    False -> text "a type"
 2157               | otherwise       = text "kind" <+> quotes (ppr exp)
 2158 
 2159     expand_syns = cec_expand_syns ctxt
 2160 
 2161     expandedTys = ppUnless (expTy1 `pickyEqType` exp && expTy2 `pickyEqType` act) $ vcat
 2162                   [ text "Type synonyms expanded:"
 2163                   , text "Expected type:" <+> ppr expTy1
 2164                   , text "  Actual type:" <+> ppr expTy2 ]
 2165 
 2166     (expTy1, expTy2) = expandSynonymsToMatch exp act
 2167 
 2168 mk_ea_msg _ _ _ _ = empty
 2169 
 2170 -- | Prints explicit kinds (with @-fprint-explicit-kinds@) in an 'SDoc' when a
 2171 -- type mismatch occurs to due invisible kind arguments.
 2172 --
 2173 -- This function first checks to see if the 'CtOrigin' argument is a
 2174 -- 'TypeEqOrigin', and if so, uses the expected/actual types from that to
 2175 -- check for a kind mismatch (as these types typically have more surrounding
 2176 -- types and are likelier to be able to glean information about whether a
 2177 -- mismatch occurred in an invisible argument position or not). If the
 2178 -- 'CtOrigin' is not a 'TypeEqOrigin', fall back on the actual mismatched types
 2179 -- themselves.
 2180 pprWithExplicitKindsWhenMismatch :: Type -> Type -> CtOrigin
 2181                                  -> SDoc -> SDoc
 2182 pprWithExplicitKindsWhenMismatch ty1 ty2 ct
 2183   = pprWithExplicitKindsWhen show_kinds
 2184   where
 2185     (act_ty, exp_ty) = case ct of
 2186       TypeEqOrigin { uo_actual = act
 2187                    , uo_expected = exp } -> (act, exp)
 2188       _                                  -> (ty1, ty2)
 2189     show_kinds = tcEqTypeVis act_ty exp_ty
 2190                  -- True when the visible bit of the types look the same,
 2191                  -- so we want to show the kinds in the displayed type
 2192 
 2193 {- Note [Insoluble occurs check]
 2194 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2195 Consider [G] a ~ [a],  [W] a ~ [a] (#13674).  The Given is insoluble
 2196 so we don't use it for rewriting.  The Wanted is also insoluble, and
 2197 we don't solve it from the Given.  It's very confusing to say
 2198     Cannot solve a ~ [a] from given constraints a ~ [a]
 2199 
 2200 And indeed even thinking about the Givens is silly; [W] a ~ [a] is
 2201 just as insoluble as Int ~ Bool.
 2202 
 2203 Conclusion: if there's an insoluble occurs check (cteInsolubleOccurs)
 2204 then report it directly, not in the "cannot deduce X from Y" form.
 2205 This is done in misMatchOrCND (via the insoluble_occurs_check arg)
 2206 
 2207 (NB: there are potentially-soluble ones, like (a ~ F a b), and we don't
 2208 want to be as draconian with them.)
 2209 
 2210 Note [Expanding type synonyms to make types similar]
 2211 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2212 
 2213 In type error messages, if -fprint-expanded-types is used, we want to expand
 2214 type synonyms to make expected and found types as similar as possible, but we
 2215 shouldn't expand types too much to make type messages even more verbose and
 2216 harder to understand. The whole point here is to make the difference in expected
 2217 and found types clearer.
 2218 
 2219 `expandSynonymsToMatch` does this, it takes two types, and expands type synonyms
 2220 only as much as necessary. Given two types t1 and t2:
 2221 
 2222   * If they're already same, it just returns the types.
 2223 
 2224   * If they're in form `C1 t1_1 .. t1_n` and `C2 t2_1 .. t2_m` (C1 and C2 are
 2225     type constructors), it expands C1 and C2 if they're different type synonyms.
 2226     Then it recursively does the same thing on expanded types. If C1 and C2 are
 2227     same, then it applies the same procedure to arguments of C1 and arguments of
 2228     C2 to make them as similar as possible.
 2229 
 2230     Most important thing here is to keep number of synonym expansions at
 2231     minimum. For example, if t1 is `T (T3, T5, Int)` and t2 is `T (T5, T3,
 2232     Bool)` where T5 = T4, T4 = T3, ..., T1 = X, it returns `T (T3, T3, Int)` and
 2233     `T (T3, T3, Bool)`.
 2234 
 2235   * Otherwise types don't have same shapes and so the difference is clearly
 2236     visible. It doesn't do any expansions and show these types.
 2237 
 2238 Note that we only expand top-layer type synonyms. Only when top-layer
 2239 constructors are the same we start expanding inner type synonyms.
 2240 
 2241 Suppose top-layer type synonyms of t1 and t2 can expand N and M times,
 2242 respectively. If their type-synonym-expanded forms will meet at some point (i.e.
 2243 will have same shapes according to `sameShapes` function), it's possible to find
 2244 where they meet in O(N+M) top-layer type synonym expansions and O(min(N,M))
 2245 comparisons. We first collect all the top-layer expansions of t1 and t2 in two
 2246 lists, then drop the prefix of the longer list so that they have same lengths.
 2247 Then we search through both lists in parallel, and return the first pair of
 2248 types that have same shapes. Inner types of these two types with same shapes
 2249 are then expanded using the same algorithm.
 2250 
 2251 In case they don't meet, we return the last pair of types in the lists, which
 2252 has top-layer type synonyms completely expanded. (in this case the inner types
 2253 are not expanded at all, as the current form already shows the type error)
 2254 -}
 2255 
 2256 -- | Expand type synonyms in given types only enough to make them as similar as
 2257 -- possible. Returned types are the same in terms of used type synonyms.
 2258 --
 2259 -- To expand all synonyms, see 'Type.expandTypeSynonyms'.
 2260 --
 2261 -- See `ExpandSynsFail` tests in tests testsuite/tests/typecheck/should_fail for
 2262 -- some examples of how this should work.
 2263 expandSynonymsToMatch :: Type -> Type -> (Type, Type)
 2264 expandSynonymsToMatch ty1 ty2 = (ty1_ret, ty2_ret)
 2265   where
 2266     (ty1_ret, ty2_ret) = go ty1 ty2
 2267 
 2268     -- | Returns (type synonym expanded version of first type,
 2269     --            type synonym expanded version of second type)
 2270     go :: Type -> Type -> (Type, Type)
 2271     go t1 t2
 2272       | t1 `pickyEqType` t2 =
 2273         -- Types are same, nothing to do
 2274         (t1, t2)
 2275 
 2276     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
 2277       | tc1 == tc2
 2278       , tys1 `equalLength` tys2 =
 2279         -- Type constructors are same. They may be synonyms, but we don't
 2280         -- expand further. The lengths of tys1 and tys2 must be equal;
 2281         -- for example, with type S a = a, we don't want
 2282         -- to zip (S Monad Int) and (S Bool).
 2283         let (tys1', tys2') =
 2284               unzip (zipWithEqual "expandSynonymsToMatch" go tys1 tys2)
 2285          in (TyConApp tc1 tys1', TyConApp tc2 tys2')
 2286 
 2287     go (AppTy t1_1 t1_2) (AppTy t2_1 t2_2) =
 2288       let (t1_1', t2_1') = go t1_1 t2_1
 2289           (t1_2', t2_2') = go t1_2 t2_2
 2290        in (mkAppTy t1_1' t1_2', mkAppTy t2_1' t2_2')
 2291 
 2292     go ty1@(FunTy _ w1 t1_1 t1_2) ty2@(FunTy _ w2 t2_1 t2_2) | w1 `eqType` w2 =
 2293       let (t1_1', t2_1') = go t1_1 t2_1
 2294           (t1_2', t2_2') = go t1_2 t2_2
 2295        in ( ty1 { ft_arg = t1_1', ft_res = t1_2' }
 2296           , ty2 { ft_arg = t2_1', ft_res = t2_2' })
 2297 
 2298     go (ForAllTy b1 t1) (ForAllTy b2 t2) =
 2299       -- NOTE: We may have a bug here, but we just can't reproduce it easily.
 2300       -- See D1016 comments for details and our attempts at producing a test
 2301       -- case. Short version: We probably need RnEnv2 to really get this right.
 2302       let (t1', t2') = go t1 t2
 2303        in (ForAllTy b1 t1', ForAllTy b2 t2')
 2304 
 2305     go (CastTy ty1 _) ty2 = go ty1 ty2
 2306     go ty1 (CastTy ty2 _) = go ty1 ty2
 2307 
 2308     go t1 t2 =
 2309       -- See Note [Expanding type synonyms to make types similar] for how this
 2310       -- works
 2311       let
 2312         t1_exp_tys = t1 : tyExpansions t1
 2313         t2_exp_tys = t2 : tyExpansions t2
 2314         t1_exps    = length t1_exp_tys
 2315         t2_exps    = length t2_exp_tys
 2316         dif        = abs (t1_exps - t2_exps)
 2317       in
 2318         followExpansions $
 2319           zipEqual "expandSynonymsToMatch.go"
 2320             (if t1_exps > t2_exps then drop dif t1_exp_tys else t1_exp_tys)
 2321             (if t2_exps > t1_exps then drop dif t2_exp_tys else t2_exp_tys)
 2322 
 2323     -- | Expand the top layer type synonyms repeatedly, collect expansions in a
 2324     -- list. The list does not include the original type.
 2325     --
 2326     -- Example, if you have:
 2327     --
 2328     --   type T10 = T9
 2329     --   type T9  = T8
 2330     --   ...
 2331     --   type T0  = Int
 2332     --
 2333     -- `tyExpansions T10` returns [T9, T8, T7, ... Int]
 2334     --
 2335     -- This only expands the top layer, so if you have:
 2336     --
 2337     --   type M a = Maybe a
 2338     --
 2339     -- `tyExpansions (M T10)` returns [Maybe T10] (T10 is not expanded)
 2340     tyExpansions :: Type -> [Type]
 2341     tyExpansions = unfoldr (\t -> (\x -> (x, x)) `fmap` tcView t)
 2342 
 2343     -- | Drop the type pairs until types in a pair look alike (i.e. the outer
 2344     -- constructors are the same).
 2345     followExpansions :: [(Type, Type)] -> (Type, Type)
 2346     followExpansions [] = pprPanic "followExpansions" empty
 2347     followExpansions [(t1, t2)]
 2348       | sameShapes t1 t2 = go t1 t2 -- expand subtrees
 2349       | otherwise        = (t1, t2) -- the difference is already visible
 2350     followExpansions ((t1, t2) : tss)
 2351       -- Traverse subtrees when the outer shapes are the same
 2352       | sameShapes t1 t2 = go t1 t2
 2353       -- Otherwise follow the expansions until they look alike
 2354       | otherwise = followExpansions tss
 2355 
 2356     sameShapes :: Type -> Type -> Bool
 2357     sameShapes AppTy{}          AppTy{}          = True
 2358     sameShapes (TyConApp tc1 _) (TyConApp tc2 _) = tc1 == tc2
 2359     sameShapes (FunTy {})       (FunTy {})       = True
 2360     sameShapes (ForAllTy {})    (ForAllTy {})    = True
 2361     sameShapes (CastTy ty1 _)   ty2              = sameShapes ty1 ty2
 2362     sameShapes ty1              (CastTy ty2 _)   = sameShapes ty1 ty2
 2363     sameShapes _                _                = False
 2364 
 2365 sameOccExtra :: TcType -> TcType -> SDoc
 2366 -- See Note [Disambiguating (X ~ X) errors]
 2367 sameOccExtra ty1 ty2
 2368   | Just (tc1, _) <- tcSplitTyConApp_maybe ty1
 2369   , Just (tc2, _) <- tcSplitTyConApp_maybe ty2
 2370   , let n1 = tyConName tc1
 2371         n2 = tyConName tc2
 2372         same_occ = nameOccName n1                   == nameOccName n2
 2373         same_pkg = moduleUnit (nameModule n1) == moduleUnit (nameModule n2)
 2374   , n1 /= n2   -- Different Names
 2375   , same_occ   -- but same OccName
 2376   = text "NB:" <+> (ppr_from same_pkg n1 $$ ppr_from same_pkg n2)
 2377   | otherwise
 2378   = empty
 2379   where
 2380     ppr_from same_pkg nm
 2381       | isGoodSrcSpan loc
 2382       = hang (quotes (ppr nm) <+> text "is defined at")
 2383            2 (ppr loc)
 2384       | otherwise  -- Imported things have an UnhelpfulSrcSpan
 2385       = hang (quotes (ppr nm))
 2386            2 (sep [ text "is defined in" <+> quotes (ppr (moduleName mod))
 2387                   , ppUnless (same_pkg || pkg == mainUnit) $
 2388                     nest 4 $ text "in package" <+> quotes (ppr pkg) ])
 2389        where
 2390          pkg = moduleUnit mod
 2391          mod = nameModule nm
 2392          loc = nameSrcSpan nm
 2393 
 2394 {- Note [Suggest adding a type signature]
 2395 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2396 The OutsideIn algorithm rejects GADT programs that don't have a principal
 2397 type, and indeed some that do.  Example:
 2398    data T a where
 2399      MkT :: Int -> T Int
 2400 
 2401    f (MkT n) = n
 2402 
 2403 Does this have type f :: T a -> a, or f :: T a -> Int?
 2404 The error that shows up tends to be an attempt to unify an
 2405 untouchable type variable.  So suggestAddSig sees if the offending
 2406 type variable is bound by an *inferred* signature, and suggests
 2407 adding a declared signature instead.
 2408 
 2409 More specifically, we suggest adding a type sig if we have p ~ ty, and
 2410 p is a skolem bound by an InferSkol.  Those skolems were created from
 2411 unification variables in simplifyInfer.  Why didn't we unify?  It must
 2412 have been because of an intervening GADT or existential, making it
 2413 untouchable. Either way, a type signature would help.  For GADTs, it
 2414 might make it typeable; for existentials the attempt to write a
 2415 signature will fail -- or at least will produce a better error message
 2416 next time
 2417 
 2418 This initially came up in #8968, concerning pattern synonyms.
 2419 
 2420 Note [Disambiguating (X ~ X) errors]
 2421 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2422 See #8278
 2423 
 2424 Note [Reporting occurs-check errors]
 2425 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2426 Given (a ~ [a]), if 'a' is a rigid type variable bound by a user-supplied
 2427 type signature, then the best thing is to report that we can't unify
 2428 a with [a], because a is a skolem variable.  That avoids the confusing
 2429 "occur-check" error message.
 2430 
 2431 But nowadays when inferring the type of a function with no type signature,
 2432 even if there are errors inside, we still generalise its signature and
 2433 carry on. For example
 2434    f x = x:x
 2435 Here we will infer something like
 2436    f :: forall a. a -> [a]
 2437 with a deferred error of (a ~ [a]).  So in the deferred unsolved constraint
 2438 'a' is now a skolem, but not one bound by the programmer in the context!
 2439 Here we really should report an occurs check.
 2440 
 2441 So isUserSkolem distinguishes the two.
 2442 
 2443 Note [Non-injective type functions]
 2444 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2445 It's very confusing to get a message like
 2446      Couldn't match expected type `Depend s'
 2447             against inferred type `Depend s1'
 2448 so mkTyFunInfoMsg adds:
 2449        NB: `Depend' is type function, and hence may not be injective
 2450 
 2451 Warn of loopy local equalities that were dropped.
 2452 
 2453 
 2454 ************************************************************************
 2455 *                                                                      *
 2456                  Type-class errors
 2457 *                                                                      *
 2458 ************************************************************************
 2459 -}
 2460 
 2461 mkDictErr :: HasDebugCallStack => ReportErrCtxt -> [Ct] -> TcM Report
 2462 mkDictErr ctxt cts
 2463   = assert (not (null cts)) $
 2464     do { inst_envs <- tcGetInstEnvs
 2465        ; let min_cts = elim_superclasses cts
 2466              lookups = map (lookup_cls_inst inst_envs) min_cts
 2467              (no_inst_cts, overlap_cts) = partition is_no_inst lookups
 2468 
 2469        -- Report definite no-instance errors,
 2470        -- or (iff there are none) overlap errors
 2471        -- But we report only one of them (hence 'head') because they all
 2472        -- have the same source-location origin, to try avoid a cascade
 2473        -- of error from one location
 2474        ; err <- mk_dict_err ctxt (head (no_inst_cts ++ overlap_cts))
 2475        ; return $ important err }
 2476   where
 2477     no_givens = null (getUserGivens ctxt)
 2478 
 2479     is_no_inst (ct, (matches, unifiers, _))
 2480       =  no_givens
 2481       && null matches
 2482       && (null unifiers || all (not . isAmbiguousTyVar) (tyCoVarsOfCtList ct))
 2483 
 2484     lookup_cls_inst inst_envs ct
 2485       = (ct, lookupInstEnv True inst_envs clas tys)
 2486       where
 2487         (clas, tys) = getClassPredTys (ctPred ct)
 2488 
 2489 
 2490     -- When simplifying [W] Ord (Set a), we need
 2491     --    [W] Eq a, [W] Ord a
 2492     -- but we really only want to report the latter
 2493     elim_superclasses cts = mkMinimalBySCs ctPred cts
 2494 
 2495 -- [Note: mk_dict_err]
 2496 -- ~~~~~~~~~~~~~~~~~~~
 2497 -- Different dictionary error messages are reported depending on the number of
 2498 -- matches and unifiers:
 2499 --
 2500 --   - No matches, regardless of unifiers: report "No instance for ...".
 2501 --   - Two or more matches, regardless of unifiers: report "Overlapping instances for ...",
 2502 --     and show the matching and unifying instances.
 2503 --   - One match, one or more unifiers: report "Overlapping instances for", show the
 2504 --     matching and unifying instances, and say "The choice depends on the instantion of ...,
 2505 --     and the result of evaluating ...".
 2506 mk_dict_err :: HasCallStack => ReportErrCtxt -> (Ct, ClsInstLookupResult)
 2507             -> TcM SDoc
 2508 -- Report an overlap error if this class constraint results
 2509 -- from an overlap (returning Left clas), otherwise return (Right pred)
 2510 mk_dict_err ctxt@(CEC {cec_encl = implics}) (ct, (matches, unifiers, unsafe_overlapped))
 2511   | null matches  -- No matches but perhaps several unifiers
 2512   = do { (_, binds_msg, ct) <- relevantBindings True ctxt ct
 2513        ; candidate_insts <- get_candidate_instances
 2514        ; field_suggestions <- record_field_suggestions
 2515        ; return (cannot_resolve_msg ct candidate_insts binds_msg field_suggestions) }
 2516 
 2517   | null unsafe_overlapped   -- Some matches => overlap errors
 2518   = return overlap_msg
 2519 
 2520   | otherwise
 2521   = return safe_haskell_msg
 2522   where
 2523     orig          = ctOrigin ct
 2524     pred          = ctPred ct
 2525     (clas, tys)   = getClassPredTys pred
 2526     ispecs        = [ispec | (ispec, _) <- matches]
 2527     unsafe_ispecs = [ispec | (ispec, _) <- unsafe_overlapped]
 2528     useful_givens = discardProvCtxtGivens orig (getUserGivensFromImplics implics)
 2529          -- useful_givens are the enclosing implications with non-empty givens,
 2530          -- modulo the horrid discardProvCtxtGivens
 2531 
 2532     get_candidate_instances :: TcM [ClsInst]
 2533     -- See Note [Report candidate instances]
 2534     get_candidate_instances
 2535       | [ty] <- tys   -- Only try for single-parameter classes
 2536       = do { instEnvs <- tcGetInstEnvs
 2537            ; return (filter (is_candidate_inst ty)
 2538                             (classInstances instEnvs clas)) }
 2539       | otherwise = return []
 2540 
 2541     is_candidate_inst ty inst -- See Note [Report candidate instances]
 2542       | [other_ty] <- is_tys inst
 2543       , Just (tc1, _) <- tcSplitTyConApp_maybe ty
 2544       , Just (tc2, _) <- tcSplitTyConApp_maybe other_ty
 2545       = let n1 = tyConName tc1
 2546             n2 = tyConName tc2
 2547             different_names = n1 /= n2
 2548             same_occ_names = nameOccName n1 == nameOccName n2
 2549         in different_names && same_occ_names
 2550       | otherwise = False
 2551 
 2552     -- See Note [Out-of-scope fields with -XOverloadedRecordDot]
 2553     record_field_suggestions :: TcM SDoc
 2554     record_field_suggestions = flip (maybe $ return empty) record_field $ \name ->
 2555        do { glb_env <- getGlobalRdrEnv
 2556           ; lcl_env <- getLocalRdrEnv
 2557           ; if occ_name_in_scope glb_env lcl_env name
 2558               then return empty
 2559               else do { dflags   <- getDynFlags
 2560                       ; imp_info <- getImports
 2561                       ; curr_mod <- getModule
 2562                       ; hpt      <- getHpt
 2563                       ; return (unknownNameSuggestions WL_RecField dflags hpt curr_mod
 2564                           glb_env emptyLocalRdrEnv imp_info (mkRdrUnqual name)) } }
 2565 
 2566     occ_name_in_scope glb_env lcl_env occ_name = not $
 2567       null (lookupGlobalRdrEnv glb_env occ_name) &&
 2568       isNothing (lookupLocalRdrOcc lcl_env occ_name)
 2569 
 2570     record_field = case orig of
 2571       HasFieldOrigin name -> Just (mkVarOccFS name)
 2572       _                   -> Nothing
 2573 
 2574     cannot_resolve_msg :: Ct -> [ClsInst] -> SDoc -> SDoc -> SDoc
 2575     cannot_resolve_msg ct candidate_insts binds_msg field_suggestions
 2576       = vcat [ no_inst_msg
 2577              , nest 2 extra_note
 2578              , vcat (pp_givens useful_givens)
 2579              , mb_patsyn_prov `orElse` empty
 2580              , ppWhen (has_ambig_tvs && not (null unifiers && null useful_givens))
 2581                (vcat [ ppUnless lead_with_ambig ambig_msg, binds_msg, potential_msg ])
 2582 
 2583              , ppWhen (isNothing mb_patsyn_prov) $
 2584                    -- Don't suggest fixes for the provided context of a pattern
 2585                    -- synonym; the right fix is to bind more in the pattern
 2586                show_fixes (ctxtFixes has_ambig_tvs pred implics
 2587                            ++ drv_fixes)
 2588              , ppWhen (not (null candidate_insts))
 2589                (hang (text "There are instances for similar types:")
 2590                    2 (vcat (map ppr candidate_insts)))
 2591                    -- See Note [Report candidate instances]
 2592              , field_suggestions ]
 2593       where
 2594         orig = ctOrigin ct
 2595         -- See Note [Highlighting ambiguous type variables]
 2596         lead_with_ambig = has_ambig_tvs && not (any isRuntimeUnkSkol ambig_tvs)
 2597                         && not (null unifiers) && null useful_givens
 2598 
 2599         (has_ambig_tvs, ambig_msg) = mkAmbigMsg lead_with_ambig ct
 2600         ambig_tvs = uncurry (++) (getAmbigTkvs ct)
 2601 
 2602         no_inst_msg
 2603           | lead_with_ambig
 2604           = ambig_msg <+> pprArising orig
 2605               $$ text "prevents the constraint" <+>  quotes (pprParendType pred)
 2606               <+> text "from being solved."
 2607 
 2608           | null useful_givens
 2609           = addArising orig $ text "No instance for"
 2610             <+> pprParendType pred
 2611 
 2612           | otherwise
 2613           = addArising orig $ text "Could not deduce"
 2614             <+> pprParendType pred
 2615 
 2616         potential_msg
 2617           = ppWhen (not (null unifiers) && want_potential orig) $
 2618             sdocOption sdocPrintPotentialInstances $ \print_insts ->
 2619             getPprStyle $ \sty ->
 2620             pprPotentials (PrintPotentialInstances print_insts) sty potential_hdr unifiers
 2621 
 2622         potential_hdr
 2623           = vcat [ ppWhen lead_with_ambig $
 2624                      text "Probable fix: use a type annotation to specify what"
 2625                      <+> pprQuotedList ambig_tvs <+> text "should be."
 2626                  , thisOrThese unifiers <+> text "potential instance" <> plural unifiers
 2627                    <+> text "exist" <> singular unifiers <> text ":"]
 2628 
 2629         mb_patsyn_prov :: Maybe SDoc
 2630         mb_patsyn_prov
 2631           | not lead_with_ambig
 2632           , ProvCtxtOrigin PSB{ psb_def = L _ pat } <- orig
 2633           = Just (vcat [ text "In other words, a successful match on the pattern"
 2634                        , nest 2 $ ppr pat
 2635                        , text "does not provide the constraint" <+> pprParendType pred ])
 2636           | otherwise = Nothing
 2637 
 2638     -- Report "potential instances" only when the constraint arises
 2639     -- directly from the user's use of an overloaded function
 2640     want_potential (TypeEqOrigin {}) = False
 2641     want_potential _                 = True
 2642 
 2643     extra_note | any isFunTy (filterOutInvisibleTypes (classTyCon clas) tys)
 2644                = text "(maybe you haven't applied a function to enough arguments?)"
 2645                | className clas == typeableClassName  -- Avoid mysterious "No instance for (Typeable T)
 2646                , [_,ty] <- tys                        -- Look for (Typeable (k->*) (T k))
 2647                , Just (tc,_) <- tcSplitTyConApp_maybe ty
 2648                , not (isTypeFamilyTyCon tc)
 2649                = hang (text "GHC can't yet do polykinded")
 2650                     2 (text "Typeable" <+>
 2651                        parens (ppr ty <+> dcolon <+> ppr (tcTypeKind ty)))
 2652                | otherwise
 2653                = empty
 2654 
 2655     drv_fixes = case orig of
 2656                    DerivClauseOrigin                  -> [drv_fix False]
 2657                    StandAloneDerivOrigin              -> [drv_fix True]
 2658                    DerivOriginDC _ _       standalone -> [drv_fix standalone]
 2659                    DerivOriginCoerce _ _ _ standalone -> [drv_fix standalone]
 2660                    _                -> []
 2661 
 2662     drv_fix standalone_wildcard
 2663       | standalone_wildcard
 2664       = text "fill in the wildcard constraint yourself"
 2665       | otherwise
 2666       = hang (text "use a standalone 'deriving instance' declaration,")
 2667            2 (text "so you can specify the instance context yourself")
 2668 
 2669     -- Normal overlap error
 2670     overlap_msg
 2671       = assert (not (null matches)) $
 2672         vcat [  addArising orig (text "Overlapping instances for"
 2673                                 <+> pprType (mkClassPred clas tys))
 2674 
 2675              ,  ppUnless (null matching_givens) $
 2676                   sep [text "Matching givens (or their superclasses):"
 2677                       , nest 2 (vcat matching_givens)]
 2678 
 2679              ,  sdocOption sdocPrintPotentialInstances $ \print_insts ->
 2680                 getPprStyle $ \sty ->
 2681                 pprPotentials (PrintPotentialInstances print_insts) sty (text "Matching instances:") $
 2682                 ispecs ++ unifiers
 2683 
 2684              ,  ppWhen (null matching_givens && isSingleton matches && null unifiers) $
 2685                 -- Intuitively, some given matched the wanted in their
 2686                 -- flattened or rewritten (from given equalities) form
 2687                 -- but the matcher can't figure that out because the
 2688                 -- constraints are non-flat and non-rewritten so we
 2689                 -- simply report back the whole given
 2690                 -- context. Accelerate Smart.hs showed this problem.
 2691                   sep [ text "There exists a (perhaps superclass) match:"
 2692                       , nest 2 (vcat (pp_givens useful_givens))]
 2693 
 2694              ,  ppWhen (isSingleton matches) $
 2695                 parens (vcat [ ppUnless (null tyCoVars) $
 2696                                  text "The choice depends on the instantiation of" <+>
 2697                                    quotes (pprWithCommas ppr tyCoVars)
 2698                              , ppUnless (null famTyCons) $
 2699                                  if (null tyCoVars)
 2700                                    then
 2701                                      text "The choice depends on the result of evaluating" <+>
 2702                                        quotes (pprWithCommas ppr famTyCons)
 2703                                    else
 2704                                      text "and the result of evaluating" <+>
 2705                                        quotes (pprWithCommas ppr famTyCons)
 2706                              , ppWhen (null (matching_givens)) $
 2707                                vcat [ text "To pick the first instance above, use IncoherentInstances"
 2708                                     , text "when compiling the other instance declarations"]
 2709                         ])]
 2710       where
 2711         tyCoVars = tyCoVarsOfTypesList tys
 2712         famTyCons = filter isFamilyTyCon $ concatMap (nonDetEltsUniqSet . tyConsOfType) tys
 2713 
 2714     matching_givens = mapMaybe matchable useful_givens
 2715 
 2716     matchable implic@(Implic { ic_given = evvars, ic_info = skol_info })
 2717       = case ev_vars_matching of
 2718              [] -> Nothing
 2719              _  -> Just $ hang (pprTheta ev_vars_matching)
 2720                             2 (sep [ text "bound by" <+> ppr skol_info
 2721                                    , text "at" <+>
 2722                                      ppr (tcl_loc (ic_env implic)) ])
 2723         where ev_vars_matching = [ pred
 2724                                  | ev_var <- evvars
 2725                                  , let pred = evVarPred ev_var
 2726                                  , any can_match (pred : transSuperClasses pred) ]
 2727               can_match pred
 2728                  = case getClassPredTys_maybe pred of
 2729                      Just (clas', tys') -> clas' == clas
 2730                                           && isJust (tcMatchTys tys tys')
 2731                      Nothing -> False
 2732 
 2733     -- Overlap error because of Safe Haskell (first
 2734     -- match should be the most specific match)
 2735     safe_haskell_msg
 2736      = assert (matches `lengthIs` 1 && not (null unsafe_ispecs)) $
 2737        vcat [ addArising orig (text "Unsafe overlapping instances for"
 2738                        <+> pprType (mkClassPred clas tys))
 2739             , sep [text "The matching instance is:",
 2740                    nest 2 (pprInstance $ head ispecs)]
 2741             , vcat [ text "It is compiled in a Safe module and as such can only"
 2742                    , text "overlap instances from the same module, however it"
 2743                    , text "overlaps the following instances from different" <+>
 2744                      text "modules:"
 2745                    , nest 2 (vcat [pprInstances $ unsafe_ispecs])
 2746                    ]
 2747             ]
 2748 
 2749 
 2750 ctxtFixes :: Bool -> PredType -> [Implication] -> [SDoc]
 2751 ctxtFixes has_ambig_tvs pred implics
 2752   | not has_ambig_tvs
 2753   , isTyVarClassPred pred
 2754   , (skol:skols) <- usefulContext implics pred
 2755   , let what | null skols
 2756              , SigSkol (PatSynCtxt {}) _ _ <- skol
 2757              = text "\"required\""
 2758              | otherwise
 2759              = empty
 2760   = [sep [ text "add" <+> pprParendType pred
 2761            <+> text "to the" <+> what <+> text "context of"
 2762          , nest 2 $ ppr_skol skol $$
 2763                     vcat [ text "or" <+> ppr_skol skol
 2764                          | skol <- skols ] ] ]
 2765   | otherwise = []
 2766   where
 2767     ppr_skol (PatSkol (RealDataCon dc) _) = text "the data constructor" <+> quotes (ppr dc)
 2768     ppr_skol (PatSkol (PatSynCon ps)   _) = text "the pattern synonym"  <+> quotes (ppr ps)
 2769     ppr_skol skol_info = ppr skol_info
 2770 
 2771 discardProvCtxtGivens :: CtOrigin -> [UserGiven] -> [UserGiven]
 2772 discardProvCtxtGivens orig givens  -- See Note [discardProvCtxtGivens]
 2773   | ProvCtxtOrigin (PSB {psb_id = L _ name}) <- orig
 2774   = filterOut (discard name) givens
 2775   | otherwise
 2776   = givens
 2777   where
 2778     discard n (Implic { ic_info = SigSkol (PatSynCtxt n') _ _ }) = n == n'
 2779     discard _ _                                                  = False
 2780 
 2781 usefulContext :: [Implication] -> PredType -> [SkolemInfo]
 2782 -- usefulContext picks out the implications whose context
 2783 -- the programmer might plausibly augment to solve 'pred'
 2784 usefulContext implics pred
 2785   = go implics
 2786   where
 2787     pred_tvs = tyCoVarsOfType pred
 2788     go [] = []
 2789     go (ic : ics)
 2790        | implausible ic = rest
 2791        | otherwise      = ic_info ic : rest
 2792        where
 2793           -- Stop when the context binds a variable free in the predicate
 2794           rest | any (`elemVarSet` pred_tvs) (ic_skols ic) = []
 2795                | otherwise                                 = go ics
 2796 
 2797     implausible ic
 2798       | null (ic_skols ic)            = True
 2799       | implausible_info (ic_info ic) = True
 2800       | otherwise                     = False
 2801 
 2802     implausible_info (SigSkol (InfSigCtxt {}) _ _) = True
 2803     implausible_info _                             = False
 2804     -- Do not suggest adding constraints to an *inferred* type signature
 2805 
 2806 {- Note [Report candidate instances]
 2807 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2808 If we have an unsolved (Num Int), where `Int` is not the Prelude Int,
 2809 but comes from some other module, then it may be helpful to point out
 2810 that there are some similarly named instances elsewhere.  So we get
 2811 something like
 2812     No instance for (Num Int) arising from the literal ‘3’
 2813     There are instances for similar types:
 2814       instance Num GHC.Types.Int -- Defined in ‘GHC.Num’
 2815 Discussion in #9611.
 2816 
 2817 Note [Highlighting ambiguous type variables]
 2818 ~-------------------------------------------
 2819 When we encounter ambiguous type variables (i.e. type variables
 2820 that remain metavariables after type inference), we need a few more
 2821 conditions before we can reason that *ambiguity* prevents constraints
 2822 from being solved:
 2823   - We can't have any givens, as encountering a typeclass error
 2824     with given constraints just means we couldn't deduce
 2825     a solution satisfying those constraints and as such couldn't
 2826     bind the type variable to a known type.
 2827   - If we don't have any unifiers, we don't even have potential
 2828     instances from which an ambiguity could arise.
 2829   - Lastly, I don't want to mess with error reporting for
 2830     unknown runtime types so we just fall back to the old message there.
 2831 Once these conditions are satisfied, we can safely say that ambiguity prevents
 2832 the constraint from being solved.
 2833 
 2834 Note [discardProvCtxtGivens]
 2835 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2836 In most situations we call all enclosing implications "useful". There is one
 2837 exception, and that is when the constraint that causes the error is from the
 2838 "provided" context of a pattern synonym declaration:
 2839 
 2840   pattern Pat :: (Num a, Eq a) => Show a   => a -> Maybe a
 2841              --  required      => provided => type
 2842   pattern Pat x <- (Just x, 4)
 2843 
 2844 When checking the pattern RHS we must check that it does actually bind all
 2845 the claimed "provided" constraints; in this case, does the pattern (Just x, 4)
 2846 bind the (Show a) constraint.  Answer: no!
 2847 
 2848 But the implication we generate for this will look like
 2849    forall a. (Num a, Eq a) => [W] Show a
 2850 because when checking the pattern we must make the required
 2851 constraints available, since they are needed to match the pattern (in
 2852 this case the literal '4' needs (Num a, Eq a)).
 2853 
 2854 BUT we don't want to suggest adding (Show a) to the "required" constraints
 2855 of the pattern synonym, thus:
 2856   pattern Pat :: (Num a, Eq a, Show a) => Show a => a -> Maybe a
 2857 It would then typecheck but it's silly.  We want the /pattern/ to bind
 2858 the alleged "provided" constraints, Show a.
 2859 
 2860 So we suppress that Implication in discardProvCtxtGivens.  It's
 2861 painfully ad-hoc but the truth is that adding it to the "required"
 2862 constraints would work.  Suppressing it solves two problems.  First,
 2863 we never tell the user that we could not deduce a "provided"
 2864 constraint from the "required" context. Second, we never give a
 2865 possible fix that suggests to add a "provided" constraint to the
 2866 "required" context.
 2867 
 2868 For example, without this distinction the above code gives a bad error
 2869 message (showing both problems):
 2870 
 2871   error: Could not deduce (Show a) ... from the context: (Eq a)
 2872          ... Possible fix: add (Show a) to the context of
 2873          the signature for pattern synonym `Pat' ...
 2874 
 2875 Note [Out-of-scope fields with -XOverloadedRecordDot]
 2876 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2877 With -XOverloadedRecordDot, when a field isn't in scope, the error that appears
 2878 is produces here, and it says
 2879     No instance for (GHC.Record.HasField "<fieldname>" ...).
 2880 
 2881 Additionally, though, we want to suggest similar field names that are in scope
 2882 or could be in scope with different import lists.
 2883 
 2884 However, we can still get an error about a missing HasField instance when a
 2885 field is in scope (if the types are wrong), and so it's important that we don't
 2886 suggest similar names here if the record field is in scope, either qualified or
 2887 unqualified, since qualification doesn't matter for -XOverloadedRecordDot.
 2888 
 2889 Example:
 2890 
 2891     import Data.Monoid (Alt(..))
 2892 
 2893     foo = undefined.getAll
 2894 
 2895 results in
 2896 
 2897      No instance for (GHC.Records.HasField "getAll" r0 a0)
 2898         arising from selecting the field ‘getAll’
 2899       Perhaps you meant ‘getAlt’ (imported from Data.Monoid)
 2900       Perhaps you want to add ‘getAll’ to the import list
 2901       in the import of ‘Data.Monoid’
 2902 -}
 2903 
 2904 show_fixes :: [SDoc] -> SDoc
 2905 show_fixes []     = empty
 2906 show_fixes (f:fs) = sep [ text "Possible fix:"
 2907                         , nest 2 (vcat (f : map (text "or" <+>) fs))]
 2908 
 2909 
 2910 -- Avoid boolean blindness
 2911 newtype PrintPotentialInstances = PrintPotentialInstances Bool
 2912 
 2913 pprPotentials :: PrintPotentialInstances -> PprStyle -> SDoc -> [ClsInst] -> SDoc
 2914 -- See Note [Displaying potential instances]
 2915 pprPotentials (PrintPotentialInstances show_potentials) sty herald insts
 2916   | null insts
 2917   = empty
 2918 
 2919   | null show_these
 2920   = hang herald
 2921        2 (vcat [ not_in_scope_msg empty
 2922                , flag_hint ])
 2923 
 2924   | otherwise
 2925   = hang herald
 2926        2 (vcat [ pprInstances show_these
 2927                , ppWhen (n_in_scope_hidden > 0) $
 2928                  text "...plus"
 2929                    <+> speakNOf n_in_scope_hidden (text "other")
 2930                , not_in_scope_msg (text "...plus")
 2931                , flag_hint ])
 2932   where
 2933     n_show = 3 :: Int
 2934 
 2935     (in_scope, not_in_scope) = partition inst_in_scope insts
 2936     sorted = sortBy fuzzyClsInstCmp in_scope
 2937     show_these | show_potentials = sorted
 2938                | otherwise       = take n_show sorted
 2939     n_in_scope_hidden = length sorted - length show_these
 2940 
 2941        -- "in scope" means that all the type constructors
 2942        -- are lexically in scope; these instances are likely
 2943        -- to be more useful
 2944     inst_in_scope :: ClsInst -> Bool
 2945     inst_in_scope cls_inst = nameSetAll name_in_scope $
 2946                              orphNamesOfTypes (is_tys cls_inst)
 2947 
 2948     name_in_scope name
 2949       | pretendNameIsInScope name
 2950       = True -- E.g. (->); see Note [pretendNameIsInScope] in GHC.Builtin.Names
 2951       | Just mod <- nameModule_maybe name
 2952       = qual_in_scope (qualName sty mod (nameOccName name))
 2953       | otherwise
 2954       = True
 2955 
 2956     qual_in_scope :: QualifyName -> Bool
 2957     qual_in_scope NameUnqual    = True
 2958     qual_in_scope (NameQual {}) = True
 2959     qual_in_scope _             = False
 2960 
 2961     not_in_scope_msg herald
 2962       | null not_in_scope
 2963       = empty
 2964       | otherwise
 2965       = hang (herald <+> speakNOf (length not_in_scope) (text "instance")
 2966                      <+> text "involving out-of-scope types")
 2967            2 (ppWhen show_potentials (pprInstances not_in_scope))
 2968 
 2969     flag_hint = ppUnless (show_potentials || equalLength show_these insts) $
 2970                 text "(use -fprint-potential-instances to see them all)"
 2971 
 2972 {- Note [Displaying potential instances]
 2973 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2974 When showing a list of instances for
 2975   - overlapping instances (show ones that match)
 2976   - no such instance (show ones that could match)
 2977 we want to give it a bit of structure.  Here's the plan
 2978 
 2979 * Say that an instance is "in scope" if all of the
 2980   type constructors it mentions are lexically in scope.
 2981   These are the ones most likely to be useful to the programmer.
 2982 
 2983 * Show at most n_show in-scope instances,
 2984   and summarise the rest ("plus N others")
 2985 
 2986 * Summarise the not-in-scope instances ("plus 4 not in scope")
 2987 
 2988 * Add the flag -fshow-potential-instances which replaces the
 2989   summary with the full list
 2990 -}
 2991 
 2992 {-
 2993 Note [Kind arguments in error messages]
 2994 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 2995 It can be terribly confusing to get an error message like (#9171)
 2996 
 2997     Couldn't match expected type ‘GetParam Base (GetParam Base Int)’
 2998                 with actual type ‘GetParam Base (GetParam Base Int)’
 2999 
 3000 The reason may be that the kinds don't match up.  Typically you'll get
 3001 more useful information, but not when it's as a result of ambiguity.
 3002 
 3003 To mitigate this, GHC attempts to enable the -fprint-explicit-kinds flag
 3004 whenever any error message arises due to a kind mismatch. This means that
 3005 the above error message would instead be displayed as:
 3006 
 3007     Couldn't match expected type
 3008                   ‘GetParam @* @k2 @* Base (GetParam @* @* @k2 Base Int)’
 3009                 with actual type
 3010                   ‘GetParam @* @k20 @* Base (GetParam @* @* @k20 Base Int)’
 3011 
 3012 Which makes it clearer that the culprit is the mismatch between `k2` and `k20`.
 3013 -}
 3014 
 3015 mkAmbigMsg :: Bool -- True when message has to be at beginning of sentence
 3016            -> Ct -> (Bool, SDoc)
 3017 mkAmbigMsg prepend_msg ct
 3018   | null ambig_kvs && null ambig_tvs = (False, empty)
 3019   | otherwise                        = (True,  msg)
 3020   where
 3021     (ambig_kvs, ambig_tvs) = getAmbigTkvs ct
 3022 
 3023     msg |  any isRuntimeUnkSkol ambig_kvs  -- See Note [Runtime skolems]
 3024         || any isRuntimeUnkSkol ambig_tvs
 3025         = vcat [ text "Cannot resolve unknown runtime type"
 3026                  <> plural ambig_tvs <+> pprQuotedList ambig_tvs
 3027                , text "Use :print or :force to determine these types"]
 3028 
 3029         | not (null ambig_tvs)
 3030         = pp_ambig (text "type") ambig_tvs
 3031 
 3032         | otherwise
 3033         = pp_ambig (text "kind") ambig_kvs
 3034 
 3035     pp_ambig what tkvs
 3036       | prepend_msg -- "Ambiguous type variable 't0'"
 3037       = text "Ambiguous" <+> what <+> text "variable"
 3038         <> plural tkvs <+> pprQuotedList tkvs
 3039 
 3040       | otherwise -- "The type variable 't0' is ambiguous"
 3041       = text "The" <+> what <+> text "variable" <> plural tkvs
 3042         <+> pprQuotedList tkvs <+> isOrAre tkvs <+> text "ambiguous"
 3043 
 3044 pprSkols :: ReportErrCtxt -> [TcTyVar] -> SDoc
 3045 pprSkols ctxt tvs
 3046   = vcat (map pp_one (getSkolemInfo (cec_encl ctxt) tvs))
 3047   where
 3048     pp_one (UnkSkol, tvs)
 3049       = vcat [ hang (pprQuotedList tvs)
 3050                  2 (is_or_are tvs "a" "(rigid, skolem)")
 3051              , nest 2 (text "of unknown origin")
 3052              , nest 2 (text "bound at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs)))
 3053              ]
 3054     pp_one (RuntimeUnkSkol, tvs)
 3055       = hang (pprQuotedList tvs)
 3056            2 (is_or_are tvs "an" "unknown runtime")
 3057     pp_one (skol_info, tvs)
 3058       = vcat [ hang (pprQuotedList tvs)
 3059                   2 (is_or_are tvs "a"  "rigid" <+> text "bound by")
 3060              , nest 2 (pprSkolInfo skol_info)
 3061              , nest 2 (text "at" <+> ppr (foldr1 combineSrcSpans (map getSrcSpan tvs))) ]
 3062 
 3063     is_or_are [_] article adjective = text "is" <+> text article <+> text adjective
 3064                                       <+> text "type variable"
 3065     is_or_are _   _       adjective = text "are" <+> text adjective
 3066                                       <+> text "type variables"
 3067 
 3068 getAmbigTkvs :: Ct -> ([Var],[Var])
 3069 getAmbigTkvs ct
 3070   = partition (`elemVarSet` dep_tkv_set) ambig_tkvs
 3071   where
 3072     tkvs       = tyCoVarsOfCtList ct
 3073     ambig_tkvs = filter isAmbiguousTyVar tkvs
 3074     dep_tkv_set = tyCoVarsOfTypes (map tyVarKind tkvs)
 3075 
 3076 getSkolemInfo :: [Implication] -> [TcTyVar]
 3077               -> [(SkolemInfo, [TcTyVar])]                    -- #14628
 3078 -- Get the skolem info for some type variables
 3079 -- from the implication constraints that bind them.
 3080 --
 3081 -- In the returned (skolem, tvs) pairs, the 'tvs' part is non-empty
 3082 getSkolemInfo _ []
 3083   = []
 3084 
 3085 getSkolemInfo [] tvs
 3086   | all isRuntimeUnkSkol tvs = [(RuntimeUnkSkol, tvs)]        -- #14628
 3087   | otherwise = -- See https://gitlab.haskell.org/ghc/ghc/-/issues?label_name[]=No%20skolem%20info
 3088       pprTraceUserWarning msg [(UnkSkol,tvs)]
 3089   where
 3090     msg = text "No skolem info - we could not find the origin of the following variables" <+> ppr tvs
 3091        $$ text "This should not happen, please report it as a bug following the instructions at:"
 3092        $$ text "https://gitlab.haskell.org/ghc/ghc/wikis/report-a-bug"
 3093 
 3094 
 3095 getSkolemInfo (implic:implics) tvs
 3096   | null tvs_here =                            getSkolemInfo implics tvs
 3097   | otherwise   = (ic_info implic, tvs_here) : getSkolemInfo implics tvs_other
 3098   where
 3099     (tvs_here, tvs_other) = partition (`elem` ic_skols implic) tvs
 3100 
 3101 -----------------------
 3102 -- relevantBindings looks at the value environment and finds values whose
 3103 -- types mention any of the offending type variables.  It has to be
 3104 -- careful to zonk the Id's type first, so it has to be in the monad.
 3105 -- We must be careful to pass it a zonked type variable, too.
 3106 --
 3107 -- We always remove closed top-level bindings, though,
 3108 -- since they are never relevant (cf #8233)
 3109 
 3110 relevantBindings :: Bool  -- True <=> filter by tyvar; False <=> no filtering
 3111                           -- See #8191
 3112                  -> ReportErrCtxt -> Ct
 3113                  -> TcM (ReportErrCtxt, SDoc, Ct)
 3114 -- Also returns the zonked and tidied CtOrigin of the constraint
 3115 relevantBindings want_filtering ctxt ct
 3116   = do { traceTc "relevantBindings" (ppr ct)
 3117        ; (env1, tidy_orig) <- zonkTidyOrigin (cec_tidy ctxt) (ctLocOrigin loc)
 3118 
 3119              -- For *kind* errors, report the relevant bindings of the
 3120              -- enclosing *type* equality, because that's more useful for the programmer
 3121        ; let extra_tvs = case tidy_orig of
 3122                              KindEqOrigin t1 t2 _ _ -> tyCoVarsOfTypes [t1,t2]
 3123                              _                      -> emptyVarSet
 3124              ct_fvs = tyCoVarsOfCt ct `unionVarSet` extra_tvs
 3125 
 3126              -- Put a zonked, tidied CtOrigin into the Ct
 3127              loc'   = setCtLocOrigin loc tidy_orig
 3128              ct'    = setCtLoc ct loc'
 3129 
 3130        ; (env2, lcl_name_cache) <- zonkTidyTcLclEnvs env1 [lcl_env]
 3131 
 3132        ; doc <- relevant_bindings want_filtering lcl_env lcl_name_cache ct_fvs
 3133        ; let ctxt'  = ctxt { cec_tidy = env2 }
 3134        ; return (ctxt', doc, ct') }
 3135   where
 3136     loc     = ctLoc ct
 3137     lcl_env = ctLocEnv loc
 3138 
 3139 -- slightly more general version, to work also with holes
 3140 relevant_bindings :: Bool
 3141                   -> TcLclEnv
 3142                   -> NameEnv Type -- Cache of already zonked and tidied types
 3143                   -> TyCoVarSet
 3144                   -> TcM SDoc
 3145 relevant_bindings want_filtering lcl_env lcl_name_env ct_tvs
 3146   = do { dflags <- getDynFlags
 3147        ; traceTc "relevant_bindings" $
 3148            vcat [ ppr ct_tvs
 3149                 , pprWithCommas id [ ppr id <+> dcolon <+> ppr (idType id)
 3150                                    | TcIdBndr id _ <- tcl_bndrs lcl_env ]
 3151                 , pprWithCommas id
 3152                     [ ppr id | TcIdBndr_ExpType id _ _ <- tcl_bndrs lcl_env ] ]
 3153 
 3154        ; (docs, discards)
 3155               <- go dflags (maxRelevantBinds dflags)
 3156                     emptyVarSet [] False
 3157                     (removeBindingShadowing $ tcl_bndrs lcl_env)
 3158          -- tcl_bndrs has the innermost bindings first,
 3159          -- which are probably the most relevant ones
 3160 
 3161        ; let doc = ppUnless (null docs) $
 3162                    hang (text "Relevant bindings include")
 3163                       2 (vcat docs $$ ppWhen discards discardMsg)
 3164 
 3165        ; return doc }
 3166   where
 3167     run_out :: Maybe Int -> Bool
 3168     run_out Nothing = False
 3169     run_out (Just n) = n <= 0
 3170 
 3171     dec_max :: Maybe Int -> Maybe Int
 3172     dec_max = fmap (\n -> n - 1)
 3173 
 3174 
 3175     go :: DynFlags -> Maybe Int -> TcTyVarSet -> [SDoc]
 3176        -> Bool                          -- True <=> some filtered out due to lack of fuel
 3177        -> [TcBinder]
 3178        -> TcM ([SDoc], Bool)   -- The bool says if we filtered any out
 3179                                         -- because of lack of fuel
 3180     go _ _ _ docs discards []
 3181       = return (reverse docs, discards)
 3182     go dflags n_left tvs_seen docs discards (tc_bndr : tc_bndrs)
 3183       = case tc_bndr of
 3184           TcTvBndr {} -> discard_it
 3185           TcIdBndr id top_lvl -> go2 (idName id) top_lvl
 3186           TcIdBndr_ExpType name et top_lvl ->
 3187             do { mb_ty <- readExpType_maybe et
 3188                    -- et really should be filled in by now. But there's a chance
 3189                    -- it hasn't, if, say, we're reporting a kind error en route to
 3190                    -- checking a term. See test indexed-types/should_fail/T8129
 3191                    -- Or we are reporting errors from the ambiguity check on
 3192                    -- a local type signature
 3193                ; case mb_ty of
 3194                    Just _ty -> go2 name top_lvl
 3195                    Nothing -> discard_it  -- No info; discard
 3196                }
 3197       where
 3198         discard_it = go dflags n_left tvs_seen docs
 3199                         discards tc_bndrs
 3200         go2 id_name top_lvl
 3201           = do { let tidy_ty = case lookupNameEnv lcl_name_env id_name of
 3202                                   Just tty -> tty
 3203                                   Nothing -> pprPanic "relevant_bindings" (ppr id_name)
 3204                ; traceTc "relevantBindings 1" (ppr id_name <+> dcolon <+> ppr tidy_ty)
 3205                ; let id_tvs = tyCoVarsOfType tidy_ty
 3206                      doc = sep [ pprPrefixOcc id_name <+> dcolon <+> ppr tidy_ty
 3207                                , nest 2 (parens (text "bound at"
 3208                                     <+> ppr (getSrcLoc id_name)))]
 3209                      new_seen = tvs_seen `unionVarSet` id_tvs
 3210 
 3211                ; if (want_filtering && not (hasPprDebug dflags)
 3212                                     && id_tvs `disjointVarSet` ct_tvs)
 3213                           -- We want to filter out this binding anyway
 3214                           -- so discard it silently
 3215                  then discard_it
 3216 
 3217                  else if isTopLevel top_lvl && not (isNothing n_left)
 3218                           -- It's a top-level binding and we have not specified
 3219                           -- -fno-max-relevant-bindings, so discard it silently
 3220                  then discard_it
 3221 
 3222                  else if run_out n_left && id_tvs `subVarSet` tvs_seen
 3223                           -- We've run out of n_left fuel and this binding only
 3224                           -- mentions already-seen type variables, so discard it
 3225                  then go dflags n_left tvs_seen docs
 3226                          True      -- Record that we have now discarded something
 3227                          tc_bndrs
 3228 
 3229                           -- Keep this binding, decrement fuel
 3230                  else go dflags (dec_max n_left) new_seen
 3231                          (doc:docs) discards tc_bndrs }
 3232 
 3233 
 3234 discardMsg :: SDoc
 3235 discardMsg = text "(Some bindings suppressed;" <+>
 3236              text "use -fmax-relevant-binds=N or -fno-max-relevant-binds)"
 3237 
 3238 -----------------------
 3239 warnDefaulting :: TcTyVar -> [Ct] -> Type -> TcM ()
 3240 warnDefaulting the_tv wanteds default_ty
 3241   = do { warn_default <- woptM Opt_WarnTypeDefaults
 3242        ; env0 <- tcInitTidyEnv
 3243        ; let tidy_env = tidyFreeTyCoVars env0 $
 3244                         tyCoVarsOfCtsList (listToBag wanteds)
 3245              tidy_wanteds = map (tidyCt tidy_env) wanteds
 3246              tidy_tv = lookupVarEnv (snd tidy_env) the_tv
 3247              (loc, ppr_wanteds) = pprWithArising tidy_wanteds
 3248              warn_msg =
 3249                 hang (hsep $ [ text "Defaulting" ]
 3250                              ++
 3251                              (case tidy_tv of
 3252                                  Nothing -> []
 3253                                  Just tv -> [text "the type variable"
 3254                                             , quotes (ppr tv)])
 3255                              ++
 3256                              [ text "to type"
 3257                              , quotes (ppr default_ty)
 3258                              , text "in the following constraint" <> plural tidy_wanteds ])
 3259                      2
 3260                      ppr_wanteds
 3261        ; let diag = TcRnUnknownMessage $
 3262                mkPlainDiagnostic (WarningWithFlag Opt_WarnTypeDefaults) noHints warn_msg
 3263        ; setCtLocM loc $ diagnosticTc warn_default diag }
 3264 
 3265 {-
 3266 Note [Runtime skolems]
 3267 ~~~~~~~~~~~~~~~~~~~~~~
 3268 We want to give a reasonably helpful error message for ambiguity
 3269 arising from *runtime* skolems in the debugger.  These
 3270 are created by in GHC.Runtime.Heap.Inspect.zonkRTTIType.
 3271 
 3272 ************************************************************************
 3273 *                                                                      *
 3274                  Error from the canonicaliser
 3275          These ones are called *during* constraint simplification
 3276 *                                                                      *
 3277 ************************************************************************
 3278 -}
 3279 
 3280 solverDepthErrorTcS :: CtLoc -> TcType -> TcM a
 3281 solverDepthErrorTcS loc ty
 3282   = setCtLocM loc $
 3283     do { ty <- zonkTcType ty
 3284        ; env0 <- tcInitTidyEnv
 3285        ; let tidy_env     = tidyFreeTyCoVars env0 (tyCoVarsOfTypeList ty)
 3286              tidy_ty      = tidyType tidy_env ty
 3287              msg = TcRnUnknownMessage $ mkPlainError noHints $
 3288                  vcat [ text "Reduction stack overflow; size =" <+> ppr depth
 3289                       , hang (text "When simplifying the following type:")
 3290                            2 (ppr tidy_ty)
 3291                       , note ]
 3292        ; failWithTcM (tidy_env, msg) }
 3293   where
 3294     depth = ctLocDepth loc
 3295     note = vcat
 3296       [ text "Use -freduction-depth=0 to disable this check"
 3297       , text "(any upper bound you could choose might fail unpredictably with"
 3298       , text " minor updates to GHC, so disabling the check is recommended if"
 3299       , text " you're sure that type checking should terminate)" ]