mk_spec_body fn_body = mkLets (rn_binds ++ picked_binds)  $

                                     mkApps fn_body rule_lhs_args

              poly_name  = idName poly_id

              spec_occ   = mkSpecOcc (getOccName poly_name)

     -- report2: we suppress these if there are insolubles elsewhere in the tree

     report2 = [ ("Implicit params", is_ip,           False, mkGroupReporter mkIPErr)

               , ("Irreds",          is_irred,        False, mkGroupReporter mkIrredErr)

     -- report3: suppressed errors should be reported as categorized by either report1

     -- or report2. Keep this in sync with the suppress function above

     is_irred _ (IrredPred {}) = True

     is_irred _ _              = False

      -- See situation (1) of Note [Suppressing confusing errors]

     is_ww_fundep item _ = is_ww_fundep_item item

     is_ww_fundep_item = isWantedWantedFunDepOrigin . errorItemOrigin

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

 -}

 mkDictErr :: HasDebugCallStack => SolverReportErrCtxt -> NonEmpty ErrorItem -> TcM SolverReport

 mkDictErr ctxt orig_items

   = do { inst_envs <- tcGetInstEnvs

        ; return $

            SolverReport

              { sr_important_msg = SolverReportWithCtxt ctxt err

              , sr_hints = hints

              }

         }

 tryInertDicts :: DictCt -> SolverStage ()

 tryInertDicts dict_ct

   = Stage $ do { inerts <- getInertCans

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

 try_inert_dicts inerts dict_w@(DictCt { di_ev = ev_w, di_cls = cls, di_tys = tys })

               -- Enabled by the -fsolve-constant-dicts flag

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

                setTcSMode TcSSpecPrag $

             | otherwise

             -> return False }

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

 *                                                                    *

     foldTyEqs, delEq, findEq,

     partitionInertEqs, partitionFunEqs,

     filterInertEqs, filterFunEqs,

     foldFunEqs, addEqToCans,

     -- * Inert Dicts

               -- Canonical Given, Wanted

               -- Sometimes called "the inert set"

        , inert_cycle_breakers :: CycleBreakerVarStack

        , inert_famapp_cache :: FunEqMap Reduction

 emptyInertSet :: TcLevel -> InertSet

 emptyInertSet given_eq_lvl

        , inert_cycle_breakers = emptyBag :| []

        , inert_famapp_cache   = emptyFunEqs

        , inert_solved_dicts   = emptyDictMap

 {- Note [Solved dictionaries]

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

 that this chain of events won't happen, but that's very fragile.)

 -}

               -> TcLevel -> TcS a

               -> TcS a

 nestImplicTcS ref inner_tclvl (TcS thing_inside)

     do { inerts <- TcM.readTcRef old_inert_var

        ; let nest_inert = inerts { inert_cycle_breakers = pushCycleBreakerVarStack

                                                             (inert_cycle_breakers inerts)

                                                    { inert_given_eqs = False } }

                  -- All other InertSet fields are inherited

        ; new_inert_var <- TcM.newTcRef nest_inert

        ; new_wl_var    <- TcM.newTcRef emptyWorkList

        ; res <- TcM.setTcLevel inner_tclvl $

                 thing_inside nest_env

        ; new_wl_var    <- TcM.newTcRef emptyWorkList

        ; let nest_env = env { tcs_inerts   = new_inert_var

                             , tcs_worklist = new_wl_var }

        ; res <- thing_inside nest_env

        ; return res }

 -- Like nestTcS, but

 --   (a) be a no-op if the nested computation returns Nothing

 --   (b) if (but only if) success, propagate nested bindings to the caller

 tryTcS (TcS thing_inside)

   = TcS $ \ env@(TcSEnv { tcs_inerts = inerts_var

     do { old_inerts       <- TcM.readTcRef inerts_var

        ; new_inert_var    <- TcM.newTcRef old_inerts

        ; new_wl_var       <- TcM.newTcRef emptyWorkList

        ; let nest_env = env { tcs_ev_binds = new_ev_binds_var

                             , tcs_inerts   = new_inert_var

                             , tcs_worklist = new_wl_var }

          vcat [ text "old_ev_binds:" <+> ppr old_ev_binds_var

               , text "new_ev_binds:" <+> ppr new_ev_binds_var

               , ppr old_inerts ]

          then return False

          else do {  -- Successfully solved

                    -- Add the new bindings to the existing ones

                  ; TcM.traceTc "tryTcS update" (ppr (inert_solved_dicts new_inerts))

                  ; return True } }

 updateInertsWith :: InertSet -> InertSet -> InertSet

 -- Update the current inert set with bits from a nested solve,

 -- that finished with a new inert set

 --    - solved dictionaires; see Note [Propagate the solved dictionaries]

 --    - Safe Haskell failures

 updateInertsWith current_inerts

        ; return unsolved_implics }

 solveImplication :: Implication     -- Wanted

                  -> TcS Implication -- Simplified implication

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

                              , ic_given  = given_ids

                              , ic_wanted = wanteds

                              , ic_info   = info

                              , ic_status = status })

   | isSolvedStatus status

   = return imp  -- Do nothing

          -- Solve the nested constraints

        ; (has_given_eqs, given_insols, residual_wanted)

             <- nestImplicTcS ev_binds_var tclvl $

                         givens = mkGivens loc given_ids

                   ; solveSimpleGivens givens

   | otherwise

   = do { traceTcS "solveSimpleGivens {" (ppr givens)

        ; go givens

        ; traceTcS "End solveSimpleGivens }" empty }

   where

     go givens = do { solveSimples (listToBag givens)

                     ; return ( wantedCtEvEvId wanted_ev

                              , unitBag (mkNonCanonical $ CtWanted wanted_ev)) }

        ; ev_binds_var <- TcS.newTcEvBinds

        ; solved <- trySolveImplication $

                    (implicationPrototype loc_env)

                       , 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" }

                       ClassPred cls tys -> pSizeClassPred cls tys

                       _                 -> pSizeType pred

 {- Note [Solving a Wanted forall-constraint]

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

 Solving a wanted forall (quantified) constraint

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

 Finding the free vars of an EvFun is made tricky by the fact the

 bindings et_binds may be a mutable variable.  Fortunately, we

 * evVarsOfTerm is used only by GHC.Tc.Solver.neededEvVars.

 * Each EvBindsVar in an et_binds field of an EvFun is /also/ in the