ppr_termM y p Term{dc=Left dc_tag, subTerms=tt} = do

   tt_docs <- mapM (y app_prec) tt

   return $ cparen (not (null tt) && p >= app_prec)

 ppr_termM y p Term{dc=Right dc, subTerms=tt}

 {-  | dataConIsInfix dc, (t1:t2:tt') <- tt  --TODO fixity

     show_tm tt_docs

       | null tt_docs = ppr dc

       | otherwise    = cparen (p >= app_prec) $

 ppr_termM y p t@NewtypeWrap{} = pprNewtypeWrap y p t

 ppr_termM y p RefWrap{wrapped_term=t}  = do

 solveFunDeps :: CtEvidence  -- The work item

              -> [FunDepEqn (CtLoc, RewriterSet)]

              -> TcS Bool

 -- See Note [FunDep and implicit parameter reactions]

 solveFunDeps work_ev fd_eqns

   | null fd_eqns

     -- * The inert set

     InertSet(..),

     InertCans(..),

     noGivenNewtypeReprEqs, updGivenEqs,

     prohibitedSuperClassSolve,

 import GHC.Data.Bag

 import Control.Monad      ( forM_ )

 import Data.Function      ( on )

 {-

 *                                                                      *

 ********************************************************************* -}

    -- ^ a stack of (CycleBreakerTv, original family applications) lists

    -- first element in the stack corresponds to current implication;

    --   later elements correspond to outer implications

        , inert_givens :: InertCans

               -- A subset of inert_cans, containing only Givens

               -- Used to initialise inert_cans when recursing inside implications

        , inert_cycle_breakers :: CycleBreakerVarStack

 emptyInertSet given_eq_lvl

   = IS { inert_cans           = empty_cans

        , inert_givens         = empty_cans

        , inert_famapp_cache   = emptyFunEqs

        , inert_solved_dicts   = emptyDictMap

        , inert_safehask       = emptyDictMap }

   where

     empty_cans = emptyInertCans given_eq_lvl

 {- Note [Solved dictionaries]

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

 When we apply a top-level instance declaration, we add the "solved"

 -- | Push a fresh environment onto the cycle-breaker var stack. Useful

 -- when entering a nested implication.

 -- | Add a new cycle-breaker binding to the top environment on the stack.

 addCycleBreakerBindings :: Bag (TcTyVar, Type)   -- ^ (cbv,expansion) pairs

   = assertPpr (all (isCycleBreakerTyVar . fst) prs) (ppr prs) $

     ics { inert_cycle_breakers = add_to (inert_cycle_breakers ics) }

   where

 -- | Perform a monadic operation on all pairs in the top environment

 -- in the stack.

 forAllCycleBreakerBindings_ :: Monad m

                             => CycleBreakerVarStack

                             -> (TcTyVar -> TcType -> m ()) -> m ()

   = forM_ top_env (uncurry action)

 {-# INLINABLE forAllCycleBreakerBindings_ #-}  -- to allow SPECIALISE later

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

     do { inerts <- TcM.readTcRef old_inert_var

        -- See Note [trySolveImplication] in GHC.Tc.Solver.Solve

        -- All other InertSet fields are inherited

        ; 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 }

 nestTcS :: TcS a -> TcS a

 -- Use the current untouchables, augmenting the current

 -- evidence bindings, and solved dictionaries

                  ; return True } }

 updateInertsWith :: InertSet -> InertSet -> InertSet

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

 -- that finished with a new inert set

   | null ds   = f []

   | otherwise = SDoc work

  where

    = let   -- Only do this depth-limitation in User style

         go _ [] = []

         go i (d:ds) | i >= default_depth = [text "...."]

                     | otherwise     = d : go (i+1) ds