-> mkSimpleDecorated $ pprSolverReportWithCtxt msg

     TcRnSolverDepthError ty depth -> mkSimpleDecorated msg

       where

         msg =

           vcat [ text "Reduction stack overflow; size =" <+> ppr depth

                     2 (ppr ty) ]

     TcRnRedundantConstraints redundants (info, show_info)

       -> mkSimpleDecorated $

 can_eq_nc _rewritten rdr_env envs ev eq_rel ty1 ps_ty1 ty2 ps_ty2

   | ReprEq <- eq_rel

   , Just stuff1 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty1

   | ReprEq <- eq_rel

   , Just stuff2 <- tcTopNormaliseNewTypeTF_maybe envs rdr_env ty2

 -- Then, get rid of casts

 can_eq_nc rewritten rdr_env envs ev eq_rel (CastTy ty1 co1) _ ty2 ps_ty2

 can_eq_newtype_nc :: GlobalRdrEnv -> FamInstEnvs

                   -> CtEvidence           -- ^ :: ty1 ~ ty2

                   -> SwapFlag

                   -> ((Bag GlobalRdrElt, TcCoercion), TcType)  -- ^ :: ty1 ~ ty1'

                   -> TcType               -- ^ ty2

                   -> TcType               -- ^ ty2, with type synonyms

                   -> TcS (StopOrContinue (Either IrredCt EqCt))

   = do { traceTcS "can_eq_newtype_nc" $

          vcat [ ppr ev, ppr swapped, ppr co1, ppr gres, ppr ty1', ppr ty2 ]

          -- Check for blowing our stack, and increase the depth

          -- See Note [Newtypes can blow the stack]

        ; let ev' = ev `setCtEvLoc` loc'

          -- Next, we record uses of newtype constructors, since coercing

 import GHC.Data.Pair

 import Data.Maybe( isNothing, isJust, mapMaybe )

 {- Note [Overview of functional dependencies in type inference]

 tryDictFunDeps dict_ct

   = do { -- Note [Do local fundeps before top-level instances]

 -- Using functional dependencies, interact the DictCt with the

 -- inert Givens and Wanteds, to produce new equalities

 tryDictFunDepsLocal dict_ct@(DictCt { di_cls = cls, di_ev = work_ev })

   | isGiven work_ev

   = -- If work_ev is Given, there could in principle be some inert Wanteds

     -- but in practice there never are because we solve Givens first

   | otherwise

   = Stage $

        ; let eqns :: [FunDepEqns]

              eqns = foldr ((++) . do_interaction) [] $

                     findDictsByClass (inert_dicts inerts) cls

        ; traceTcS "tryDictFunDepsLocal }" $

   where

     work_pred     = ctEvPred work_ev

     work_is_given = isGiven work_ev

        ; traceTcS "tryDictFunDepsTop {" (ppr dict_ct)

        ; let eqns :: [FunDepEqns]

              eqns = improveFromInstEnv inst_envs cls xis

 {- Note [No Given/Given fundeps]

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

   = if isGiven ev

     then tryGivenBuiltinFamEqFDs eqs_for_me fam_tc ops work_args work_item

     else do { -- Note [Do local fundeps before top-level instances]

             ; then nopStage ()

                    mkTopBuiltinFamEqFDs fam_tc ops work_args work_rhs }

   | isGiven ev    -- See (INJFAM:Given)

   | otherwise   -- Wanted, user-defined type families

   = do { -- Note [Do local fundeps before top-level instances]

            Injective inj -> tryFDEqns fam_tc work_args work_item $

                             mkLocalFamEqFDs eqs_for_me fam_tc inj work_args work_rhs

          then nopStage ()

 mkTopFamEqFDs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqns]

 mkTopFamEqFDs fam_tc work_args work_rhs

     -- closed type families with no equations (isClosedFamilyTyCon_maybe returns Nothing)

     return []

 tryFDEqns fam_tc work_args work_item@(EqCt { eq_ev = ev, eq_rhs= rhs }) mk_fd_eqns

   = Stage $

     do { fd_eqns <- mk_fd_eqns

        ; traceTcS "tryFDEqns" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr work_args

                                     , text "rhs:" <+> ppr rhs

                                     , text "eqns:" <+> ppr fd_eqns ])

 -----------------------------------------

 --  User-defined type families

 solveFunDeps :: CtEvidence  -- The work item

              -> [FunDepEqns]

 -- Solve a bunch of type-equality equations, generated by functional dependencies

 -- By "solve" we mean: (only) do unifications.  We do not generate evidence, and

 -- other than unifications there should be no effects whatsoever

 -- See (SOLVE-FD) in Note [Overview of functional dependencies in type inference]

 solveFunDeps work_ev fd_eqns

   | null fd_eqns

   | otherwise

              <- reportFineGrainUnifications $

                 nestFunDepsTcS              $

                 TcS.pushTcLevelM_           $

        -- that were unified by the fundep

        ; kickOutAfterUnification unifs

   where

     do_fundeps :: UnifyEnv -> TcM ()

     do_fundeps env = mapM_ (do_one env) fd_eqns

 -- | Checks if the depth of the given location is too much. Fails if

 -- it's too big, with an appropriate error message.

                    -> TcS CtLoc

 bumpReductionDepth loc ty

   = do { dflags <- getDynFlags

                       RewriteEnv(..),

                       runTcPluginM )

 import GHC.Tc.Types.Constraint

 import GHC.Core.Predicate

 import GHC.Tc.Utils.TcType

 import GHC.Core.Type

 runRewrite :: CtLoc -> CtFlavour -> EqRel -> RewriteM a -> TcS (a, CoHoleSet)

 runRewrite loc flav eq_rel thing_inside

   = do { rewriters_ref <- newTcRef emptyCoHoleSet

                         , re_flavour   = flav

                         , re_eq_rel    = eq_rel

                         , re_rewriters = rewriters_ref }

 -- See Note [How to normalise a family application]

 rewrite_exact_fam_app :: TyCon -> [TcType] -> RewriteM Reduction

 rewrite_exact_fam_app tc tys

          -- which apply to a type family application headed by the TyCon 'tc'.

        ; tc_rewriters <- getTcPluginRewritersForTyCon tc

            -> Reduction -> RewriteM Reduction

     finish use_cache redn

       = do { -- rewrite the result: FINISH 1

            ; eq_rel <- getEqRel

              -- extend the cache: FINISH 2

   -- * CtLoc

   CtLoc(..), ctLocSpan, ctLocEnv, ctLocLevel, ctLocOrigin,

   ctLocTypeOrKind_maybe, toInvisibleLoc,

   setCtLocOrigin, updateCtLocOrigin, setCtLocEnv, setCtLocSpan,

   pprCtLoc, adjustCtLoc, adjustCtLocTyConBinder,

 bumpCtLocDepth :: CtLoc -> CtLoc

 bumpCtLocDepth loc@(CtLoc { ctl_depth = d }) = loc { ctl_depth = bumpSubGoalDepth d }

 setCtLocOrigin :: CtLoc -> CtOrigin -> CtLoc

 setCtLocOrigin ctl orig = ctl { ctl_origin = orig }