-import GHC.Tc.Solver.FunDeps( doDictFunDepImprovement )

-       ; doDictFunDepImprovement dict_ct

-import GHC.Tc.Solver.FunDeps( unifyAndEmitFunDepWanteds )

-import GHC.Tc.Solver.Types( findFunEqsByTyCon )

-import GHC.Tc.Instance.FunDeps( FunDepEqn(..) )

-import GHC.Core.Coercion.Axiom

-import GHC.Core.Unify( tcUnifyTyForInjectivity )

-import GHC.Core.FamInstEnv ( FamInstEnvs, FamInst(..), apartnessCheck

-                           , lookupFamInstEnvByTyCon )

-

-import GHC.Builtin.Types.Literals ( tryInteractTopFam, tryInteractInertFam )

-

-            Right eq_ct   -> do { tryInertEqs eq_ct

-                                ; tryFunDeps  eq_ct

-                                ; tryQCsEqCt  eq_ct

-         ; kickOutAfterUnification [tv]

-

-

-{-

-**********************************************************************

-*                                                                    *

-    Functional dependencies for type families

-*                                                                    *

-**********************************************************************

-

-Note [Reverse order of fundep equations]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-Consider this scenario (from dependent/should_fail/T13135_simple):

-

-  type Sig :: Type -> Type

-  data Sig a = SigFun a (Sig a)

-

-  type SmartFun :: forall (t :: Type). Sig t -> Type

-  type family SmartFun sig = r | r -> sig where

-    SmartFun @Type (SigFun @Type a sig) = a -> SmartFun @Type sig

-

-  [W] SmartFun @kappa sigma ~ (Int -> Bool)

-

-The injectivity of SmartFun allows us to produce two new equalities:

-

-  [W] w1 :: Type ~ kappa

-  [W] w2 :: SigFun @Type Int beta ~ sigma

-

-for some fresh (beta :: SigType). The second Wanted here is actually

-heterogeneous: the LHS has type Sig Type while the RHS has type Sig kappa.

-Of course, if we solve the first wanted first, the second becomes homogeneous.

-

-When looking for injectivity-inspired equalities, we work left-to-right,

-producing the two equalities in the order written above. However, these

-equalities are then passed into wrapUnifierTcS, which will fail, adding these

-to the work list. However, crucially, the work list operates like a *stack*.

-So, because we add w1 and then w2, we process w2 first. This is silly: solving

-w1 would unlock w2. So we make sure to add equalities to the work

-list in left-to-right order, which requires a few key calls to 'reverse'.

-

-This treatment is also used for class-based functional dependencies, although

-we do not have a program yet known to exhibit a loop there. It just seems

-like the right thing to do.

-

-When this was originally conceived, it was necessary to avoid a loop in T13135.

-That loop is now avoided by continuing with the kind equality (not the type

-equality) in canEqCanLHSHetero (see Note [Equalities with heterogeneous kinds]).

-However, the idea of working left-to-right still seems worthwhile, and so the calls

-to 'reverse' remain.

-

-Note [Improvement orientation]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-See also Note [Fundeps with instances, and equality orientation], which describes

-the Exact Same Problem, with the same solution, but for functional dependencies.

-

-A very delicate point is the orientation of equalities

-arising from injectivity improvement (#12522).  Suppose we have

-  type family F x = t | t -> x

-  type instance F (a, Int) = (Int, G a)

-where G is injective; and wanted constraints

-

-  [W] F (alpha, beta) ~ (Int, <some type>)

-

-The injectivity will give rise to constraints

-

-  [W] gamma1 ~ alpha

-  [W] Int ~ beta

-

-The fresh unification variable gamma1 comes from the fact that we

-can only do "partial improvement" here; see Section 5.2 of

-"Injective type families for Haskell" (HS'15).

-

-Now, it's very important to orient the equations this way round,

-so that the fresh unification variable will be eliminated in

-favour of alpha.  If we instead had

-   [W] alpha ~ gamma1

-then we would unify alpha := gamma1; and kick out the wanted

-constraint.  But when we substitute it back in, it'd look like

-   [W] F (gamma1, beta) ~ fuv

-and exactly the same thing would happen again!  Infinite loop.

-

-This all seems fragile, and it might seem more robust to avoid

-introducing gamma1 in the first place, in the case where the

-actual argument (alpha, beta) partly matches the improvement

-template.  But that's a bit tricky, esp when we remember that the

-kinds much match too; so it's easier to let the normal machinery

-handle it.  Instead we are careful to orient the new

-equality with the template on the left.  Delicate, but it works.

-

--}

-

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

-

-tryFunDeps :: EqCt -> SolverStage ()

-tryFunDeps work_item@(EqCt { eq_lhs = lhs, eq_ev = ev, eq_eq_rel = eq_rel })

-  | NomEq <- eq_rel

-  , TyFamLHS tc args <- lhs

-  = Stage $

-    do { inerts <- getInertCans

-       ; imp1 <- improveLocalFunEqs inerts tc args work_item

-       ; imp2 <- improveTopFunEqs tc args work_item

-       ; if (imp1 || imp2)

-         then startAgainWith (mkNonCanonical ev)

-         else continueWith () }

-  | otherwise

-  = nopStage ()

-

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

-improveTopFunEqs :: TyCon -> [TcType] -> EqCt -> TcS Bool

--- TyCon is definitely a type family

--- See Note [FunDep and implicit parameter reactions]

-improveTopFunEqs fam_tc args (EqCt { eq_ev = ev, eq_rhs = rhs_ty })

-  | isGiven ev = improveGivenTopFunEqs  fam_tc args ev rhs_ty

-  | otherwise  = improveWantedTopFunEqs fam_tc args ev rhs_ty

-

-improveGivenTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool

--- TyCon is definitely a type family

--- Work-item is a Given

-improveGivenTopFunEqs fam_tc args ev rhs_ty

-  | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc

-  = do { traceTcS "improveGivenTopFunEqs" (ppr fam_tc <+> ppr args $$ ppr ev $$ ppr rhs_ty)

-       ; emitNewGivens (ctEvLoc ev) $

-           [ (Nominal, new_co)

-           | (ax, _) <- tryInteractTopFam ops fam_tc args rhs_ty

-           , let new_co = mkAxiomCo ax [given_co] ]

-       ; return False }  -- False: no unifications

-  | otherwise

-  = return False

-  where

-    given_co :: Coercion = ctEvCoercion ev

-

-improveWantedTopFunEqs :: TyCon -> [TcType] -> CtEvidence -> Xi -> TcS Bool

--- TyCon is definitely a type family

--- Work-item is a Wanted

-improveWantedTopFunEqs fam_tc args ev rhs_ty

-  = do { eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty

-       ; traceTcS "improveTopFunEqs" (vcat [ text "lhs:" <+> ppr fam_tc <+> ppr args

-                                           , text "rhs:" <+> ppr rhs_ty

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

-       ; unifyFunDeps ev Nominal $ \uenv ->

-         uPairsTcM (bump_depth uenv) (reverse eqns) }

-         -- Missing that `reverse` causes T13135 and T13135_simple to loop.

-         -- See Note [Reverse order of fundep equations]

-

-  where

-    bump_depth env = env { u_loc = bumpCtLocDepth (u_loc env) }

-        -- ToDo: this location is wrong; it should be FunDepOrigin2

-        -- See #14778

-

-improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi

-                           -> TcS [TypeEqn]

--- TyCon is definitely a type family

-improve_wanted_top_fun_eqs fam_tc lhs_tys rhs_ty

-  | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc

-  = return (map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty)

-

-  -- ToDo: use ideas in #23162 for closed type families; injectivity only for open

-

-  -- See Note [Type inference for type families with injectivity]

-  -- Open, so look for inj

-  | Injective inj_args <- tyConInjectivityInfo fam_tc

-  = do { fam_envs <- getFamInstEnvs

-       ; top_eqns <- improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty

-       ; let local_eqns = improve_injective_wanted_famfam  inj_args fam_tc lhs_tys rhs_ty

-       ; traceTcS "improve_wanted_top_fun_eqs" $

-         vcat [ ppr fam_tc, text "local_eqns" <+> ppr local_eqns, text "top_eqns" <+> ppr top_eqns ]

-  -- xxx ToDo: this does both local and top => bug?

-       ; return (local_eqns ++ top_eqns) }

-

-  | otherwise  -- No injectivity

-  = return []

-

-improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon -> [TcType] -> Xi -> TcS [TypeEqn]

--- Interact with top-level instance declarations

--- See Section 5.2 in the Injective Type Families paper

-improve_injective_wanted_top fam_envs inj_args fam_tc lhs_tys rhs_ty

-  = concatMapM do_one branches

-  where

-    branches :: [CoAxBranch]

-    branches | isOpenTypeFamilyTyCon fam_tc

-             , let fam_insts = lookupFamInstEnvByTyCon fam_envs fam_tc

-             = concatMap (fromBranches . coAxiomBranches . fi_axiom) fam_insts

-

-             | Just ax <- isClosedSynFamilyTyConWithAxiom_maybe fam_tc

-             = fromBranches (coAxiomBranches ax)

-

-             | otherwise

-             = []

-

-    do_one :: CoAxBranch -> TcS [TypeEqn]

-    do_one branch@(CoAxBranch { cab_tvs = branch_tvs, cab_lhs = branch_lhs_tys, cab_rhs = branch_rhs })

-      | let in_scope1 = in_scope `extendInScopeSetList` branch_tvs

-      , Just subst <- tcUnifyTyForInjectivity False in_scope1 branch_rhs rhs_ty

-                      -- False: matching, not unifying

-      = do { let inSubst tv = tv `elemVarEnv` getTvSubstEnv subst

-                 unsubstTvs = filterOut inSubst branch_tvs

-                 -- The order of unsubstTvs is important; it must be

-                 -- in telescope order e.g. (k:*) (a:k)

-

-           ; (_subst_tvs, subst1) <- instFlexiX subst unsubstTvs

-                -- If the current substitution bind [k -> *], and

-                -- one of the un-substituted tyvars is (a::k), we'd better

-                -- be sure to apply the current substitution to a's kind.

-                -- Hence instFlexiX.   #13135 was an example.

-

-           ; traceTcS "improve_inj_top" $

-             vcat [ text "branch_rhs" <+> ppr branch_rhs

-                  , text "rhs_ty" <+> ppr rhs_ty

-                  , text "subst" <+> ppr subst

-                  , text "subst1" <+> ppr subst1 ]

-           ; if apartnessCheck (substTys subst1 branch_lhs_tys) branch

-             then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys)

-                     ; return (mkInjectivityEqns inj_args (map (substTy subst1) branch_lhs_tys) lhs_tys) }

-                  -- NB: The fresh unification variables (from unsubstTvs) are on the left

-                  --     See Note [Improvement orientation]

-             else do { traceTcS "improve_inj_top2" empty; return []  } }

-      | otherwise

-      = do { traceTcS "improve_inj_top:fail" (ppr branch_rhs $$ ppr rhs_ty $$ ppr in_scope $$ ppr branch_tvs)

-           ; return [] }

-

-    in_scope = mkInScopeSet (tyCoVarsOfType rhs_ty)

-

-

-improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [TypeEqn]

--- Interact with itself, specifically  F s1 s2 ~ F t1 t2

-improve_injective_wanted_famfam inj_args fam_tc lhs_tys rhs_ty

-  | Just (tc, rhs_tys) <- tcSplitTyConApp_maybe rhs_ty

-  , tc == fam_tc

-  = mkInjectivityEqns inj_args lhs_tys rhs_tys

-  | otherwise

-  = []

-

-mkInjectivityEqns :: [Bool] -> [TcType] -> [TcType] -> [TypeEqn]

--- When F s1 s2 s3 ~ F t1 t2 t3, and F has injectivity info [True,False,True]

--- return the equations [Pair s1 t1, Pair s3 t3]

-mkInjectivityEqns inj_args lhs_args rhs_args

-  = [ Pair lhs_arg rhs_arg | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]

-

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

-improveLocalFunEqs :: InertCans

-                   -> TyCon -> [TcType] -> EqCt   -- F args ~ rhs

-                   -> TcS Bool

--- Emit equalities from interaction between two equalities

-improveLocalFunEqs inerts fam_tc args (EqCt { eq_ev = work_ev, eq_rhs = rhs })

-  | isGiven work_ev = improveGivenLocalFunEqs  funeqs_for_tc fam_tc args work_ev rhs

-  | otherwise       = improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs

-  where

-    funeqs = inert_funeqs inerts

-    funeqs_for_tc :: [EqCt]   -- Mixture of Given and Wanted

-    funeqs_for_tc = [ funeq_ct | equal_ct_list <- findFunEqsByTyCon funeqs fam_tc

-                               , funeq_ct <- equal_ct_list

-                               , NomEq == eq_eq_rel funeq_ct ]

-                                  -- Representational equalities don't interact

-                                  -- with type family dependencies

-

-

-improveGivenLocalFunEqs :: [EqCt]    -- Inert items, mixture of Given and Wanted

-                        -> TyCon -> [TcType] -> CtEvidence -> Xi  -- Work item (Given)

-                        -> TcS Bool  -- Always False (no unifications)

--- Emit equalities from interaction between two Given type-family equalities

---    e.g.    (x+y1~z, x+y2~z) => (y1 ~ y2)

-improveGivenLocalFunEqs funeqs_for_tc fam_tc work_args work_ev work_rhs

-  | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc

-  = do { mapM_ (do_one ops) funeqs_for_tc

-       ; return False }     -- False: no unifications

-  | otherwise

-  = return False

-  where

-    given_co :: Coercion = ctEvCoercion work_ev

-

-    do_one :: BuiltInSynFamily -> EqCt -> TcS ()

-    -- Used only work-item is Given

-    do_one ops EqCt { eq_ev  = inert_ev, eq_lhs = inert_lhs, eq_rhs = inert_rhs }

-      | isGiven inert_ev                    -- Given/Given interaction

-      , TyFamLHS _ inert_args <- inert_lhs  -- Inert item is F inert_args ~ inert_rhs

-      , work_rhs `tcEqType` inert_rhs       -- Both RHSs are the same

-      , -- So we have work_ev  : F work_args  ~ rhs

-        --            inert_ev : F inert_args ~ rhs

-        let pairs :: [(CoAxiomRule, TypeEqn)]

-            pairs = tryInteractInertFam ops fam_tc work_args inert_args

-      , not (null pairs)

-      = do { traceTcS "improveGivenLocalFunEqs" (vcat[ ppr fam_tc <+> ppr work_args

-                                                     , text "work_ev" <+>  ppr work_ev

-                                                     , text "inert_ev" <+> ppr inert_ev

-                                                     , ppr work_rhs

-                                                     , ppr pairs ])

-           ; emitNewGivens (ctEvLoc inert_ev) (map mk_ax_co pairs) }

-             -- This CtLoc for the new Givens doesn't reflect the

-             -- fact that it's a combination of Givens, but I don't

-             -- this that matters.

-      where

-        inert_co = ctEvCoercion inert_ev

-        mk_ax_co (ax,_) = (Nominal, mkAxiomCo ax [combined_co])

-          where

-            combined_co = given_co `mkTransCo` mkSymCo inert_co

-            -- given_co :: F work_args  ~ rhs

-            -- inert_co :: F inert_args ~ rhs

-            -- the_co :: F work_args ~ F inert_args

-

-    do_one _  _ = return ()

-

-improveWantedLocalFunEqs

-    :: [EqCt]     -- Inert items (Given and Wanted)

-    -> TyCon -> [TcType] -> CtEvidence -> Xi  -- Work item (Wanted)

-    -> TcS Bool   -- True <=> some unifications

--- Emit improvement equalities for a Wanted constraint, by comparing

--- the current work item with inert CFunEqs (both Given and Wanted)

--- E.g.   x + y ~ z,   x + y' ~ z   =>   [W] y ~ y'

---

--- See Note [FunDep and implicit parameter reactions]

-improveWantedLocalFunEqs funeqs_for_tc fam_tc args work_ev rhs

-  | null improvement_eqns

-  = return False

-  | otherwise

-  = do { traceTcS "interactFunEq improvements: " $

-                   vcat [ text "Eqns:" <+> ppr improvement_eqns

-                        , text "Candidates:" <+> ppr funeqs_for_tc ]

-       ; unifyAndEmitFunDepWanteds work_ev improvement_eqns }

-  where

-    work_loc      = ctEvLoc work_ev

-    work_pred     = ctEvPred work_ev

-    fam_inj_info  = tyConInjectivityInfo fam_tc

-

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

-    improvement_eqns :: [FunDepEqn (CtLoc, RewriterSet)]

-    improvement_eqns

-      | Just ops <- isBuiltInSynFamTyCon_maybe fam_tc

-      =    -- Try built-in families, notably for arithmethic

-        concatMap (do_one_built_in ops rhs) funeqs_for_tc

-

-      | Injective injective_args <- fam_inj_info

-      =    -- Try improvement from type families with injectivity annotations

-        concatMap (do_one_injective injective_args rhs) funeqs_for_tc

-

-      | otherwise

-      = []

-

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

-    do_one_built_in ops rhs (EqCt { eq_lhs = TyFamLHS _ iargs, eq_rhs = irhs, eq_ev = inert_ev })

-      | irhs `tcEqType` rhs

-      = mk_fd_eqns inert_ev (map snd $ tryInteractInertFam ops fam_tc args iargs)

-      | otherwise

-      = []

-    do_one_built_in _ _ _ = pprPanic "interactFunEq 1" (ppr fam_tc) -- TyVarLHS

-

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

-    -- See Note [Type inference for type families with injectivity]

-    do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args

-                                        , eq_rhs = irhs, eq_ev = inert_ev })

-      | rhs `tcEqType` irhs

-      = mk_fd_eqns inert_ev $ mkInjectivityEqns inj_args args inert_args

-      | otherwise

-      = []

-

-    do_one_injective _ _ _ = pprPanic "interactFunEq 2" (ppr fam_tc)  -- TyVarLHS

-

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

-    mk_fd_eqns :: CtEvidence -> [TypeEqn] -> [FunDepEqn (CtLoc, RewriterSet)]

-    mk_fd_eqns inert_ev eqns

-      | null eqns  = []

-      | otherwise  = [ FDEqn { fd_qtvs = [], fd_eqs = eqns

-                             , fd_loc   = (loc, inert_rewriters) } ]

-      where

-        initial_loc  -- start with the location of the Wanted involved

-          | isGiven work_ev = inert_loc

-          | otherwise       = work_loc

-        eqn_orig        = InjTFOrigin1 work_pred  (ctLocOrigin work_loc)  (ctLocSpan work_loc)

-                                       inert_pred (ctLocOrigin inert_loc) (ctLocSpan inert_loc)

-        eqn_loc         = setCtLocOrigin initial_loc eqn_orig

-        inert_pred      = ctEvPred inert_ev

-        inert_loc       = ctEvLoc inert_ev

-        inert_rewriters = ctEvRewriters inert_ev

-        loc = eqn_loc { ctl_depth = ctl_depth inert_loc `maxSubGoalDepth`

-                                    ctl_depth work_loc }

-

-{- Note [Type inference for type families with injectivity]

-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

-Suppose we have a type family with an injectivity annotation:

-    type family F a b = r | r -> b

-

-Then if we have an equality like F s1 t1 ~ F s2 t2,

-we can use the injectivity to get a new Wanted constraint on

-the injective argument

-  [W] t1 ~ t2

-

-That in turn can help GHC solve constraints that would otherwise require

-guessing.  For example, consider the ambiguity check for

-   f :: F Int b -> Int

-We get the constraint

-   [W] F Int b ~ F Int beta

-where beta is a unification variable.  Injectivity lets us pick beta ~ b.

-

-Injectivity information is also used at the call sites. For example:

-   g = f True

-gives rise to

-   [W] F Int b ~ Bool

-from which we can derive b.  This requires looking at the defining equations of

-a type family, ie. finding equation with a matching RHS (Bool in this example)

-and inferring values of type variables (b in this example) from the LHS patterns

-of the matching equation.  For closed type families we have to perform

-additional apartness check for the selected equation to check that the selected

-is guaranteed to fire for given LHS arguments.

-

-These new constraints are Wanted constraints, but we will not use the evidence.

-We could go further and offer evidence from decomposing injective type-function

-applications, but that would require new evidence forms, and an extension to

-FC, so we don't do that right now (Dec 14).

-

-We generate these Wanteds in three places, depending on how we notice the

-injectivity.

-

-1. When we have a [W] F tys1 ~ F tys2. This is handled in canEqCanLHS2, and

-described in Note [Decomposing type family applications] in GHC.Tc.Solver.Equality

-

-2. When we have [W] F tys1 ~ T and [W] F tys2 ~ T. Note that neither of these

-constraints rewrites the other, as they have different LHSs. This is done

-in improveLocalFunEqs, called during the interactWithInertsStage.

-

-3. When we have [W] F tys ~ T and an equation for F that looks like F tys' = T.

-This is done in improve_top_fun_eqs, called from the top-level reactions stage.

-

-See also Note [Injective type families] in GHC.Core.TyCon

-

-Note [Cache-caused loops]

-~~~~~~~~~~~~~~~~~~~~~~~~~

-It is very dangerous to cache a rewritten wanted family equation as 'solved' in our

-solved cache (which is the default behaviour or xCtEvidence), because the interaction

-may not be contributing towards a solution. Here is an example:

-

-Initial inert set:

-  [W] g1 : F a ~ beta1

-Work item:

-  [W] g2 : F a ~ beta2

-The work item will react with the inert yielding the _same_ inert set plus:

-    (i)   Will set g2 := g1 `cast` g3

-    (ii)  Will add to our solved cache that [S] g2 : F a ~ beta2

-    (iii) Will emit [W] g3 : beta1 ~ beta2

-Now, the g3 work item will be spontaneously solved to [G] g3 : beta1 ~ beta2

-and then it will react the item in the inert ([W] g1 : F a ~ beta1). So it

-will set

-      g1 := g ; sym g3

-and what is g? Well it would ideally be a new goal of type (F a ~ beta2) but

-remember that we have this in our solved cache, and it is ... g2! In short we

-created the evidence loop:

-

-        g2 := g1 ; g3

-        g3 := refl

-        g1 := g2 ; sym g3

-

-To avoid this situation we do not cache as solved any workitems (or inert)

-which did not really made a 'step' towards proving some goal. Solved's are

-just an optimization so we don't lose anything in terms of completeness of

-solving.

--}

-  doDictFunDepImprovement,

-import GHC.Tc.Types.Evidence

-import GHC.Tc.Types.Constraint

-import GHC.Tc.Types.CtLoc

-import GHC.Tc.Types.Origin

-import GHC.Core.InstEnv     ( ClsInst(..) )

-import GHC.Core.Coercion.Axiom( TypeEqn )

-

-*          Functional dependencies, instantiation of equations

-doDictFunDepImprovement :: DictCt -> SolverStage ()

--- (doDictFunDepImprovement inst_envs cts)

--- doLocalFunDepImprovement does StartAgain if there

-doDictFunDepImprovement dict_ct

-  = do { doDictFunDepImprovementLocal dict_ct

-       ; doDictFunDepImprovementTop   dict_ct }

-doDictFunDepImprovementLocal :: DictCt -> SolverStage ()

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

-       ; traceTcS "doDictFunDepImprovementLocal {" (ppr dict_ct)

-       ; traceTcS "doDictFunDepImprovementLocal }" (text "imp =" <+> ppr imp)

-           ; traceTcS "doDictFunDepImprovementLocal item" $

-doDictFunDepImprovementTop :: DictCt -> SolverStage ()

-doDictFunDepImprovementTop dict_ct@(DictCt { di_ev = ev, di_cls = cls, di_tys = xis })

-       ; traceTcS "doDictFunDepImprovementTop {" (ppr dict_ct)

-       ; traceTcS "doDictFunDepImprovementTop }" (text "imp =" <+> ppr imp)