-- Look up the predicate in Given quantified constraints,

 -- which are effectively just local instance declarations.

 matchLocalInst body_pred loc

        ; case match_local_inst inerts (inert_insts ics) of

           { ([], []) -> do { traceTcS "No local instance for" (ppr body_pred)

                            ; return NoInstance }

           ; (matches, unifs) ->

          -- See Note [Use only the best matching quantified constraint]

        ; case dominatingMatch matches of

           { Just (dfun_id, tys, theta)

             | all ((theta `impliedBySCs`) . thdOf3) unifs

                          , text "matches:" <+> ppr matches

                          , text "unifs:" <+> ppr unifs

                          , text "best_match:" <+> ppr mb_best ]

   where

     body_pred_tv_set = tyCoVarsOfType body_pred

                       , ic_wanted = emptyWC { wc_simple = wanteds } }

       ; if solved

                 ; stopWith ev "Polytype equality: solved" }

         else canEqSoftFailure IrredShapeReason ev s1 s2 } }

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

 To solve an equality between foralls

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

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

 The evidence we produce is a ForAllCo; see the typing rule for

 getTcLevel :: TcS TcLevel

 getTcLevel = wrapTcS TcM.getTcLevel

 getTcEvTyCoVars ev_binds_var

   = wrapTcS $ TcM.getTcEvTyCoVars ev_binds_var

        ; wrapTcS $ TcM.addTcEvBind evb ev_bind }

 -- | Mark variables as used filling a coercion hole

   = do { ev_binds_var <- getTcEvBindsVar

 -- | Equalities only

 setWantedEq (HoleDest hole) co

        ; fillCoercionHole hole co }

 setWantedEq (EvVarDest ev) _ = pprPanic "setWantedEq: EvVarDest" (ppr ev)

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

 setWantedEvTerm (HoleDest hole) _canonical tm

   | Just co <- evTermCoercion_maybe tm

        ; fillCoercionHole hole co }

   | otherwise

   = -- See Note [Yukky eq_sel for a HoleDest]

 import GHC.Core.Predicate

 import GHC.Core.Reduction

 import GHC.Core.Coercion

 import GHC.Core.Class( classHasSCs )

 import GHC.Types.Id(  idType )

                             , ic_need_implic = old_need_implic    -- See (TRC1)

                     })

  = do { ev_binds <- TcS.getTcEvBindsMap ev_binds_var

       ; let -- Find the variables needed by `implics`

             new_need_implic@(ENS { ens_dms = dm_seeds, ens_fvs = other_seeds })

             -- Get the variables needed by the solved bindings

             -- (It's OK to use a non-deterministic fold here

             --  because add_wanted is commutative.)

             need_ignoring_dms = findNeededGivenEvVars ev_binds (other_seeds `unionVarSet` seeds_w)

             need_from_dms     = findNeededGivenEvVars ev_binds dm_seeds

       ; traceTcS "neededEvVars" $

         vcat [ text "old_need_implic:" <+> ppr old_need_implic

              , text "new_need_implic:" <+> ppr new_need_implic

              , text "need_ignoring_dms:" <+> ppr need_ignoring_dms

              , text "need_from_dms:"     <+> ppr need_from_dms

              , text "need:" <+> ppr need

       --     (dictionaries etc)

       -- Some Given, some Wanted

       -- See Note [Tracking redundant constraints] in GHC.Tc.Solver

     }

       -- See above for comments on ebv_uniq, ebv_tcvs

       ebv_uniq :: Unique,

     }

 instance Data.Data TcEvBinds where

 newTcEvBinds :: TcM EvBindsVar

 newTcEvBinds = do { binds_ref <- newTcRef emptyEvBindMap

                   ; uniq <- newUnique

                   ; traceTc "newTcEvBinds" (text "unique =" <+> ppr uniq)

                   ; return (EvBindsVar { ebv_binds = binds_ref

 -- must be made monadically

 newNoTcEvBinds :: TcM EvBindsVar

 newNoTcEvBinds

        ; uniq <- newUnique

        ; traceTc "newNoTcEvBinds" (text "unique =" <+> ppr uniq)

        ; return (CoEvBindsVar { ebv_tcvs = tcvs_ref

 -- solving don't pollute the original

 cloneEvBindsVar ebv@(EvBindsVar {})

   = do { binds_ref <- newTcRef emptyEvBindMap

        ; return (ebv { ebv_binds = binds_ref

                      , ebv_tcvs = tcvs_ref }) }

 cloneEvBindsVar ebv@(CoEvBindsVar {})

        ; return (ebv { ebv_tcvs = tcvs_ref }) }

 getTcEvTyCoVars ev_binds_var

   = readTcRef (ebv_tcvs ev_binds_var)

   = do { new_ebvs <- readTcRef new_ebv_ref

        ; updTcRef old_ebv_ref (`unionEvBindMap` new_ebvs)

        ; new_tcvs <- readTcRef new_tcv_ref

 updTcEvBinds (EvBindsVar { ebv_tcvs = old_tcv_ref })

              (CoEvBindsVar { ebv_tcvs = new_tcv_ref })

   = do { new_tcvs <- readTcRef new_tcv_ref

 updTcEvBinds (CoEvBindsVar { ebv_tcvs = old_tcv_ref })

              (CoEvBindsVar { ebv_tcvs = new_tcv_ref })

   = do { new_tcvs <- readTcRef new_tcv_ref

 updTcEvBinds old_var new_var

   = pprPanic "updTcEvBinds" (ppr old_var $$ ppr new_var)

     -- Terms inside types, no good

   unless (typeHasFixedRuntimeRep ty)

     (addDetailedDiagnostic $ TcRnTypeDoesNotHaveFixedRuntimeRep ty prov)

              Error messages

 *                                                                       *

 -- See Note [Naughty quantification candidates]

 naughtyQuantification :: TcType   -- original type user wanted to quantify