-- See Note [CoercionHoles and coercion free variables]

                  , ch_ref :: IORef (Maybe (Coercion, RewriterSet))

                  }

 coHoleCoVar :: CoercionHole -> CoVar

        ; empty_ec_id <- lookupId emptyExceptionContextName

        ; let ev = ctEvidence ct

              ev_tm = EvExpr (evWrapIPE (ctEvPred ev) (Var empty_ec_id))

          -- EvCanonical: see Note [CallStack and ExceptionContext hack]

          --              in GHC.Tc.Solver.Dict

        ; return True }

           = do { traceTcS "defaultEquality success:" (ppr rhs_ty)

                ; unifyTyVar lhs_tv rhs_ty  -- NB: unifyTyVar adds to the

                                            -- TcS unification counter

                ; return True

                }

             -- See Note [Defaulting representational equalities].

            ; if null new_eqs

              then do { traceTcS "defaultEquality ReprEq } (yes)" empty

                      ; return True }

              else do { traceTcS "defaultEquality ReprEq } (no)" empty

                      ; return False } }

   -- `IP ip CallStack`. See Note [Overview of implicit CallStacks]

   = do { inner_stk <- evCallStack pred ev_cs

        ; let ev_tm = EvExpr (evWrapIPE pred inner_stk)

          -- EvCanonical: see Note [CallStack and ExceptionContext hack]

   where

     pred = ctEvPred ev

   * Coercible   coercibleTyCon

 (See Note [The equality types story] in GHC.Builtin.Types.Prim.)

   Consider T17836, which has a constraint like

       forall b,c. a ~ (b,c) =>

         forall d,e. c ~ (d,e) =>

   pattern matching. Its compile-time allocation decreased by 40% when

   I added the "replace" rather than "add" semantics.)

 (EQC2) Faced with [W] t1 ~ t2, it's always OK to reduce it to [W] t1 ~# t2,

   without worrying about Note [Instance and Given overlap].  Why?  Because

   if we had [G] s1 ~ s2, then we'd get the superclass [G] s1 ~# s2, and

 -- See Note [Solving equality classes]

 -- Precondition: (isEqualityClass cls) True, so cls is (~), (~~), or Coercible

 solveEqualityDict ev cls tys

   | CtWanted (WantedCt { ctev_dest = dest }) <- ev

   = Stage $

     do { let (role, t1, t2) = matchEqualityInst cls tys

          -- Unify t1~t2, putting anything that can't be solved

          -- immediately into the work list

          -- Set  d :: (t1~t2) = Eq# co

        ; setWantedDict dest EvCanonical $

          evDictApp cls tys [Coercion co]

        ; stopWith ev "Solved wanted lifted equality" }

   | otherwise

   = pprPanic "solveEqualityDict" (ppr cls)

             | otherwise -- We can either solve the inert from the work-item or vice-versa.

             -> case solveOneFromTheOther (CDictCan dict_i) (CDictCan dict_w) of

                  KeepInert -> do { traceTcS "lookupInertDict:KeepInert" (ppr dict_w)

                                  ; return $ Stop ev_w (text "Dict equal" <+> ppr dict_w) }

                  KeepWork  -> do { traceTcS "lookupInertDict:KeepWork" (ppr dict_w)

                                  ; updInertCans (updDicts $ delDict dict_w)

                                  ; continueWith () } }

      -- See Note [No Given/Given fundeps]

   | Just solved_ev <- lookupSolvedDict inerts cls xis   -- Cached

        ; stopWith ev "Dict/Top (cached)" }

   | otherwise  -- Wanted, but not cached

        ; assertPprM (getTcEvBindsVar >>= return . not . isCoEvBindsVar)

                     (ppr work_item)

        ; evc_vars <- mapM (newWanted deeper_loc (ctEvRewriters work_item)) theta

        ; emitWorkNC (map CtWanted $ freshGoals evc_vars)

        ; stopWith work_item "Dict/Top (solved wanted)" }

   where

 import GHC.Prelude

 import GHC.Tc.Solver.Irred( solveIrred )

 import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )

 -- Literals

 can_eq_nc _rewritten _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _

  | l1 == l2

        ; stopWith ev "Equal LitTy" }

 -- Decompose FunTy: (s -> t) and (c => t)

 -- See Note [Solving forall equalities]

 can_eq_nc_forall ev eq_rel s1 s2

  = do { let (bndrs1, phi1, bndrs2, phi2) = split_foralls s1 s2

             flags1 = binderFlags bndrs1

             flags2 = binderFlags bndrs2

       ; traceTcS "Generating wanteds" (ppr s1 $$ ppr s2)

       -- Kick out any inerts constraints that mention unified type variables

       ; kickOutAfterUnification unifs

       ; if solved

                 ; stopWith ev "Polytype equality: solved" }

         else canEqSoftFailure IrredShapeReason ev s1 s2 } }

  | otherwise

         in (bndr1:bndrs1, phi1, bndr2:bndrs2, phi2)

     split_foralls s1 s2 = ([], s1, [], s2)

 {- Note [Solving forall equalities]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

 To solve an equality between foralls

    [W] (forall a. t1) ~ (forall b. t2)

 implication constraint

    [W] forall a. { t1 ~ (t2[a/b]) }

    because we want to /gather/ the equality constraint (to put in the implication)

    rather than /emit/ them into the monad, as `wrapUnifierAndEmit` does.

    is insoluble than it is to understand a message about matching `a` with `Int`.

 -}

 -- to an irreducible constraint; see typecheck/should_compile/T10494

 -- See Note [Decomposing AppTy equalities]

 can_eq_app ev s1 t1 s2 t2

   = do { traceTcS "can_eq_app" (vcat [ text "s1:" <+> ppr s1, text "t1:" <+> ppr t1

                                      , text "s2:" <+> ppr s2, text "t2:" <+> ppr t2

                                      , text "vis:" <+> ppr (isNextArgVisible s1) ])

             -- Unify arguments t1/t2 before function s1/s2, because

             -- the former have smaller kinds, and hence simpler error messages

             -- c.f. GHC.Tc.Utils.Unify.uType (go_app)

     do { traceTcS "canDecomposableTyConAppOK"

                   (ppr ev $$ ppr eq_rel $$ ppr tc $$ ppr tys1 $$ ppr tys2)

        ; case ev of

              -- new_locs and tc_roles are both infinite, so we are

              -- guaranteed that cos has the same length as tys1 and tys2

              -- See Note [Fast path when decomposing TyConApps]

                         do { cos <- zipWith4M (u_arg uenv) new_locs tc_roles tys1 tys2

                                     -- zipWith4M: see Note [Work-list ordering]

                            ; return (mkTyConAppCo role tc cos) }

   = do { traceTcS "canDecomposableFunTy"

                   (ppr ev $$ ppr eq_rel $$ ppr f1 $$ ppr f2)

        ; case ev of

                         do { let mult_env = uenv `updUEnvLoc` toInvisibleLoc InvisibleMultiplicity

                                                  `setUEnvRole` funRole role SelMult

                            ; mult <- uType mult_env m1 m2

                      then return ev

                      else rewriteEqEvidence emptyRewriterSet ev swapped

                               (mkReflRedn Nominal (mkTyVarTy tv)) rhs_redn

          ; let tv_ty     = mkTyVarTy tv

                final_rhs = reductionReducedType rhs_redn

          -- Provide Refl evidence for the constraint

          -- Ignore 'swapped' because it's Refl!

          -- Kick out any constraints that can now be rewritten

          ; kickOutAfterUnification (unitVarSet tv)

                -> TcType        -- ty

                -> TcS (StopOrContinue a)   -- always Stop

 canEqReflexive ev eq_rel ty

        ; stopWith ev "Solved by reflexivity" }

 {- Note [Equalities with heterogeneous kinds]

   | CtWanted (WantedCt { ctev_dest = dest, ctev_rewriters = rewriters }) <- old_ev

   = do { let rewriters' = rewriters S.<> new_rewriters

        ; let co = maybeSymCo swapped $

        ; traceTcS "rewriteEqEvidence" (vcat [ ppr old_ev

                                             , ppr nlhs

                                             , ppr nrhs

   = Stage $

     do { inerts <- getInertCans

        ; if | Just (ev_i, swapped) <- inertsEqsCanDischarge inerts work_item

                   ; stopWith ev "Solved from inert" }

             | otherwise

 import GHC.Tc.Solver.Monad

 import GHC.Tc.Types.Evidence

 import GHC.Types.Basic( SwapFlag(..) )

 import GHC.Utils.Outputable

 import GHC.Data.Bag

          vcat [ text "wanted:" <+> (ppr ct_w $$ ppr (ctOrigin ct_w))

               , text "inert: " <+> (ppr ct_i $$ ppr (ctOrigin ct_i)) ]

        ; case solveOneFromTheOther ct_i ct_w of

                             ; return (Stop ev_w (text "Irred equal:KeepInert" <+> ppr ct_w)) }

                             ; updInertCans (updIrreds (\_ -> others))

                             ; continueWith () } }

   where

     ct_w = CIrredCan irred_w

 {- Note [Multiple matching irreds]

 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

     CanonicalEvidence(..),

     newTcEvBinds, newNoTcEvBinds,

     newWanted,

     newWantedNC, newWantedEvVarNC,

     newBoundEvVarId,

     unifyTyVar, reportFineGrainUnifications, reportCoarseGrainUnifications,

     newEvVar, newGivenEv, emitNewGivens,

     emitChildEqs, checkReductionDepth,

 setTcLevelTcS lvl (TcS thing_inside)

  = TcS $ \ env -> TcM.setTcLevel lvl (thing_inside env)

 nestImplicTcS :: SkolemInfoAnon -> EvBindsVar

               -> TcLevel -> TcS a

               -> TcS a

 nestImplicTcS skol_info ev_binds_var inner_tclvl (TcS thing_inside)

   = TcS $ \ env@(TcSEnv { tcs_inerts = old_inert_var }) ->

        ; new_inert_var <- TcM.newTcRef nest_inert

        ; new_wl_var    <- TcM.newTcRef emptyWorkList

        ; let nest_env = env { tcs_ev_binds = ev_binds_var

 #endif

        ; return res }

   where

       -- For an implication that comes from a static form (static e),

       -- start with a completely empty inert set; in particular, no Givens

       -- See (SF3) in Note [Grand plan for static forms]

       -- in GHC.Iface.Tidy.StaticPtrTable

       | StaticFormSkol <- skol_info

       | otherwise

 nestFunDepsTcS :: TcS a -> TcS a

 nestFunDepsTcS (TcS thing_inside)

   = do { ev_binds_var <- getTcEvBindsVar

        ; wrapTcS (TcM.updTcRef (ebv_tcvs ev_binds_var) (co :)) }

 setWantedEq :: HasDebugCallStack => TcEvDest -> RewriterSet -> TcCoercion -> TcS ()

 -- ^ Equalities only

 setWantedDict :: TcEvDest -> CanonicalEvidence -> EvTerm -> TcS ()

 -- ^ Dictionaries only

 fillCoercionHole :: CoercionHole -> RewriterSet -> Coercion -> TcS ()

 fillCoercionHole hole rewriters co

        ; kickOutAfterFillingCoercionHole hole rewriters }

 newTcEvBinds :: TcS EvBindsVar

 newTcEvBinds = wrapTcS TcM.newTcEvBinds

 newGivenEv :: CtLoc -> (TcPredType, EvTerm) -> TcS GivenCtEvidence

 -- Make a new variable of the given PredType,

 -- See Note [Bind new Givens immediately] in GHC.Tc.Types.Constraint

 newGivenEv loc (pred, rhs)

   = do { new_ev <- newBoundEvVarId pred rhs

        ; return $ GivenCt { ctev_pred = pred, ctev_evar = new_ev, ctev_loc = loc } }

                 , not (ty1 `tcEqType` ty2) ] -- Kill reflexive Givens at birth

        ; emitWorkNC (map CtGiven gs) }

 emitChildEqs :: CtEvidence -> Cts -> TcS ()

 -- Emit a bunch of equalities into the work list

 -- See Note [Work-list ordering] in GHC.Tc.Solver.Equality

 -- | Create a new Wanted constraint holding a coercion hole

 -- for an equality between the two types at the given 'Role'.

 newWantedEq :: CtLoc -> RewriterSet -> Role -> TcType -> TcType

 newWantedEq loc rewriters role ty1 ty2

   = do { hole <- wrapTcS $ TcM.newCoercionHole pty

        ; let wtd = WantedCt { ctev_pred      = pty

                             , ctev_dest      = HoleDest hole

                             , ctev_loc       = loc

                             , ctev_rewriters = rewriters }

   where

     pty = mkEqPredRole role ty1 ty2

 wrapUnifierAndEmit :: CtEvidence -> Role

                    -> (UnifyEnv -> TcM a)  -- Some calls to uType

 -- Like wrapUnifier, but

 --    emits any unsolved equalities into the work-list

 --    kicks out any inert constraints that mention unified variables

 wrapUnifierAndEmit ev role do_unifications

   = do { (unifs, (res, eqs)) <- reportFineGrainUnifications $

                                 wrapUnifier ev role do_unifications

        -- Kick out any inert constraints mentioning the unified variables

        ; kickOutAfterUnification unifs

 wrapUnifier :: CtEvidence -> Role

              -> (UnifyEnv -> TcM a)  -- Some calls to uType

      solveWanteds,        -- Solves WantedConstraints

      solveSimpleGivens,   -- Solves [Ct]

      solveSimpleWanteds,  -- Solves Cts

      setImplicationStatus

   ) where

        ; return unsolved_implics }

 solveImplication :: Implication     -- Wanted

                  -> TcS Implication -- Simplified implication

 -- Precondition: The TcS monad contains an empty worklist and given-only inerts

        -- Capture the Givens in the inert_givens of the inert set

        -- for use by subsequent calls of nestImplicTcS

        ; updInertSet (\is -> is { inert_givens = inert_cans is })

        ; cans <- getInertCans

   = solveEquality ev eq_rel (canEqLHSType lhs) rhs

 solveCt (CQuantCan qci@(QCI { qci_ev = ev }))

          -- It is (much) easier to rewrite and re-classify than to

          -- rewrite the pieces and build a Reduction that will rewrite

          -- the whole constraint

            _ -> pprPanic "SolveCt" (ppr ev) }

 solveCt (CDictCan (DictCt { di_ev = ev, di_pend_sc = pend_sc }))

          -- It is easier to rewrite and re-classify than to rewrite

          -- the pieces and build a Reduction that will rewrite the

          -- whole constraint

         _ ->

     -- Do rewriting on the constraint, especially zonking

     -- And then re-classify

        ; case classifyPredType (ctEvPred ev) of

              ; continueWith () }

     ev_i:_ ->

       do { traceTcS "tryInertQCs:KeepInert" (ppr ev_i)

          ; stopWith ev_w "Solved Wanted forall-constraint from inert" }

   where

     matching_inert (QCI { qci_ev = ev_i })

 ************************************************************************

 -}

 -- Main purpose: create new evidence for new_pred;

 --                 unless new_pred is cached already

 -- * Calls do_next with (new_ev :: new_pred), with same wanted/given flag as old_ev