dsEvTerm (EvTypeable ty ev)  = dsEvTypeable ty ev

 dsEvTerm (EvFun { et_tvs = tvs, et_given = given

                 , et_binds = ev_binds, et_body = wanted_id })

                    mkCoreLets ds_ev_binds $

 {-**********************************************************************

 import GHC.Tc.Solver( reportUnsolvedEqualities, pushLevelAndSolveEqualitiesX

                     , emitResidualConstraints )

 import GHC.Tc.Solver.Solve( solveWanteds )

 import GHC.Tc.Validity ( checkValidType )

 import GHC.Tc.Utils.Monad

          -- (2) Solve the resulting wanteds in TcSSpecPrag mode.

        ; ev_binds_var <- newTcEvBinds

        ; spec_e_wanted <- setTcLevel rhs_tclvl $

                           solveWanteds spec_e_wanted

        ; spec_e_wanted <- liftZonkM $ zonkWC spec_e_wanted

          -- See `Note [Quantification and partial signatures]` Wrinkle 2

        ; return (map (box_pred . ctPred) $

   where

      box_pred :: PredType -> PredType

      box_pred pred = case classifyPredType pred of

                ; new_wanteds <- sequence [ new_wtd_ct wtd

                                          | CtWanted wtd <- map ctEvidence wanteds

                                          ]

           | otherwise

           = return Nothing

 tryInertDicts dict_ct

   = Stage $ do { inerts <- getInertCans

                ; mode   <- getTcSMode

                -- Looking at Wanteds would be OK but no real benefit

                ; case mode of

                    _other      -> try_inert_dicts inerts dict_ct }

 try_inert_dicts :: InertCans -> DictCt -> TcS (StopOrContinue ())

             -> tryTcS $  -- tryTcS tries to completely solve some contraints

                -- Inherit the current solved_dicts, so that one invocation of

                -- tryShortCutSolver can benefit from the work of earlier invocations

             | otherwise

             -> return False }

     extendWorkListEq, extendWorkListChildEqs,

     extendWorkListRewrittenEqs,

     appendWorkList,

     workListSize,

     -- * The inert set

   NB: since we do not currently apply the substitution to the

   inert_solved_dicts, the knot-tying still seems a bit fragile.

   But this makes it better.

 -}

 -- See Note [WorkList priorities]

          -- in GHC.Tc.Types.Constraint for more details.

        , wl_rest :: [Ct]

     }

 isNominalEqualityCt :: Ct -> Bool

 appendWorkList :: WorkList -> WorkList -> WorkList

 appendWorkList

    = WL { wl_eqs_N   = eqs1_N   ++ eqs2_N

         , wl_eqs_X   = eqs1_X   ++ eqs2_X

         , wl_rw_eqs  = rw_eqs1  ++ rw_eqs2

 workListSize :: WorkList -> Int

 workListSize (WL { wl_eqs_N = eqs_N, wl_eqs_X = eqs_X, wl_rw_eqs = rw_eqs, wl_rest = rest })

 -- Extension by non equality

 extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }

 extendWorkListCt :: Ct -> WorkList -> WorkList

 -- Agnostic about what kind of constraint

 extendWorkListCt ct wl

 extendWorkListCts cts wl = foldr extendWorkListCt wl cts

 isEmptyWorkList :: WorkList -> Bool

 emptyWorkList :: WorkList

 emptyWorkList = WL { wl_eqs_N = [], wl_eqs_X = []

 -- Pretty printing

 instance Outputable WorkList where

    = text "WL" <+> (braces $

      vcat [ ppUnless (null eqs_N) $

             text "Eqs_N =" <+> vcat (map ppr eqs_N)

             text "RwEqs =" <+> vcat (map ppr rw_eqs)

           , ppUnless (null rest) $

             text "Non-eqs =" <+> vcat (map ppr rest)

           ])

 {- *********************************************************************

     -- The TcS monad

     TcS(..), TcSEnv(..),

     runTcS, runTcSEarlyAbort, runTcSWithEvBinds, runTcSInerts,

     failTcS, warnTcS, addErrTcS, wrapTcS, ctLocWarnTcS,

     runTcSEqualities,

     nestTcS, nestImplicTcS, tryTcS,

     setEvBindsTcS, setTcLevelTcS,

     emitFunDepWanteds,

     selectNextWorkItem,

     -- We only want Givens from this level; see (3a) in

     -- Note [The superclass story] in GHC.Tc.Solver.Dict

 -- Return all the unsolved [Wanted] constraints

 --

 -- Post-condition: the returned simple constraints are all fully zonked

             unsolved_dicts   = foldDicts  (add_if_unsolved CDictCan)  idicts emptyCts

             unsolved_qcis    = foldr      (add_if_unsolved CQuantCan) emptyCts qcis

       ; traceTcS "getUnsolvedInerts" $

         vcat [ text " tv eqs =" <+> ppr unsolved_tv_eqs

              , text "fun eqs =" <+> ppr unsolved_fun_eqs

              , text "dicts =" <+> ppr unsolved_dicts

   where

     add_if_unsolved :: (a -> Ct) -> a -> Cts -> Cts

     add_if_unsolved mk_ct thing cts

   = TcSVanilla    -- ^ Normal constraint solving

   | TcSPMCheck    -- ^ Used when doing patterm match overlap checks

   | TcSEarlyAbort -- ^ Abort early on insoluble constraints

   deriving (Eq)

 {- Note [TcSMode]

 -- | Run the 'TcS' monad in 'TcSSpecPrag' mode, which either fully solves

 -- individual Wanted quantified constraints or leaves them alone.

 --

 {- Note [TcSSpecPrag]

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

   = current_inerts { inert_solved_dicts = new_solved

                    , inert_safehask     = new_safehask }

 {- Note [Propagate the solved dictionaries]

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

 It's really quite important that nestTcS does not discard the solved

 getWorkList = do { wl_var <- getTcSWorkListRef

                  ; readTcRef wl_var }

 updWorkListTcS :: (WorkList -> WorkList) -> TcS ()

 updWorkListTcS f

   = do { wl_var <- getTcSWorkListRef

 matchGlobalInst :: DynFlags -> Class -> [Type] -> CtLoc -> TcS TcM.ClsInstResult

 matchGlobalInst dflags cls tys loc

   = do { mode <- getTcSMode

        ; wrapTcS $ TcM.matchGlobalInst dflags short_cut cls tys (Just loc) }

 tcInstSkolTyVarsX :: SkolemInfo -> Subst -> [TyVar] -> TcS (Subst, [TcTyVar])

        ; bb <- TcS.getTcEvBindsMap ev_binds_var

        ; traceTcS "solveWanteds }" $

                  vcat [ text "final wc =" <+> ppr final_wc

                       , text "current evbinds  =" <+> ppr (evBindMapBinds bb) ]

        ; return final_wc }

                             , int (lengthBag simples) <+> text "simples to solve" ])

        ; traceTcS "simplify_loop: wc =" (ppr wc)

                 -- Any insoluble constraints are in 'simples' and so get rewritten

                 -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet

        ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]

                    && unifs1 == 0                    -- for this conditional

        ; unif_happened <- resetUnificationFlag

        ; csTraceTcS $ text "unif_happened" <+> ppr unif_happened

        -- for use by subsequent calls of nestImplicTcS

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

   where

     go givens = do { solveSimples (listToBag givens)

                    ; new_givens <- runTcPluginsGiven

                    ; when (notNull new_givens) $

                      go new_givens }

 -- The result is not necessarily zonked

 solveSimpleWanteds simples

   = do { traceTcS "solveSimpleWanteds {" (ppr simples)

        ; dflags <- getDynFlags

        ; traceTcS "solveSimpleWanteds end }" $

              vcat [ text "iterations =" <+> ppr n

                   , text "residual =" <+> ppr wc ]

        ; return wc }

   where

     -- See Note [The solveSimpleWanteds loop]

     go n limit wc

       | n `intGtLimit` limit

       = return (n,wc)

       | otherwise

       = do { -- Solve

              else return (n, wc2) }           -- Done

 -- Try solving these constraints

 -- Affects the unification state (of course) but not the inert set

 -- The result is not necessarily zonked

 {- Note [The solveSimpleWanteds loop]

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

                       , ic_skols = skol_tvs

                       , ic_given = given_ev_vars

                       , ic_wanted = emptyWC { wc_simple = wanteds } }

        ; if not solved

          then do { addInertForAll qci

                  ; stopWith (CtWanted wtd) "Wanted forall-constraint:unsolved" }

          else do { setWantedEvTerm dest EvCanonical $

                    EvFun { et_tvs = skol_tvs, et_given = given_ev_vars

                  ; stopWith (CtWanted wtd) "Wanted forall-constraint:solved" } }

   where

     loc_env = ctLocEnv ct_loc

 -- work) and a bag of insolubles.  The boolean indicates whether

 -- 'solveSimpleWanteds' should feed the updated wanteds back into the

 -- main solver.

   | isEmptyBag simples1

   | otherwise

   = do { solvers <- getTcPluginSolvers

     do { given <- getInertGivens

        ; wanted <- TcS.zonkSimples simples1    -- Plugin requires zonked inputs

        ; mapM_ setEv solved_wanted

        ; traceTcS "Finished plugins }" (ppr new_wanted)

   where

     setEv :: (EvTerm,Ct) -> TcS ()

     setEv (ev,ct) = case ctEvidence ct of

 import Prelude( Bool )

 import GHC.Tc.Solver.Monad( TcS )

 trySolveImplication :: Implication -> TcS Bool

   | EvFun     -- /\as \ds. let binds in v

       { et_tvs   :: [TyVar]

       , et_given :: [EvVar]

       , et_body  :: EvVar }

   deriving Data.Data

 evVarsOfTerm :: EvTerm -> VarSet

 evVarsOfTerm (EvExpr e)         = exprSomeFreeVars relevantEvVar e

 evVarsOfTerm (EvTypeable _ ev)  = evVarsOfTypeable ev

 evVarsOfTerms :: [EvTerm] -> VarSet

 evVarsOfTerms = mapUnionVarSet evVarsOfTerm

                   , et_binds = ev_binds, et_body = body_id })

   = runZonkBndrT (zonkTyBndrsX tvs)       $ \ new_tvs      ->

     runZonkBndrT (zonkEvBndrsX evs)       $ \ new_evs      ->

   do { new_body_id  <- zonkIdOcc body_id

      ; return (EvFun { et_tvs = new_tvs, et_given = new_evs

                      , et_binds = new_ev_binds, et_body = new_body_id }) }

 tried = try @e

 -- From the call to "try", we get [W] D (T e).

 --

 -- The Given "[G] C3 m" thus arises from superclass expansion

 -- from "D (T e)", which contains a type family application, T.

 -- expanding the superclasses of C3 (in this case, C2); in particular

 -- ltPatersonSize needs to handle a type family in its second argument.