+                       -- INVARIANT: not all False

+(IMP1) fd_qtvs: sometimes the instance mentions variables in the RHS that

+(IMP2) Multi-range fundeps. When these meta_tvs are involved, there is a subtle

+(IMP3) improveFromInstEnv doesn't return any equations that already hold.

+    Reason: just an optimisation; the caller does the same thing, but

+    with a bit more ceremony.

+                                 -- See (IMP2) in Note [Improving against instances]

+ | discard ty1 ty2 = -- See (IMP3) in Note [Improving against instances]

+                     zipAndComputeFDEqs discard tys1 tys2

+           ; (co, new_eqs) <- wrapUnifier (ctEvidence ct) Nominal $ \uenv ->

+                              -- NB: nominal equality!

+                              uType uenv z_ty1 z_ty2

+       ; co <- wrapUnifierAndEmit ev role $ \uenv ->

+               uType uenv t1 t2

+                                    wrapUnifier ev (eqRelRole eq_rel) $ \uenv ->

+   especially Refl ones.  We use the `wrapUnifier` wrapper for `uType`,

+   rather than /emit/ them into the monad, as `wrapUnifierAndEmit` does.

+       ; co <- wrapUnifierAndEmit ev Nominal $ \uenv ->

+So canDecomposableTyConAppOK uses wrapUnifierAndEmit etc to short-cut

+* `wrapUnifierAndEmit` adds the bag of deferred constraints from

+             -> do { co <- wrapUnifierAndEmit ev role $ \uenv ->

+             -> do { co <- wrapUnifierAndEmit ev Nominal $ \ uenv ->

+         -> do { (unifs, (kind_co, cts)) <- reportUnifications $

+                                            wrapUnifier ev Nominal $ \uenv ->

+                                            let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)

+                                            in unSwap swapped (uType uenv') ki1 ki2

+

+               -- Emit any unsolved kind equalities

+               ; unless (isEmptyBag cts) $

+                 updWorkListTcS (extendWorkListChildEqs ev cts)

+

+               ; if unifs

+directly instead of calling wrapUnifier. (Otherwise, we'd end up

+{- Note [Overview of fundeps]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+Here is our plan for dealing with functional dependencies

+* When we have failed to solve a Wanted constraint, do this

+  1. Generate any fundep-equalities [FunDepEqn] from that constraint.

+  2. Try to solve that [FunDepEqn]

+  3. If any unifications happened, send the constraint back to the

+     start of the pipeline

+* Step (1) How we generate those [FunDepEqn] varies:

+       - tryDictFunDeps: for class constraints (C t1 .. tn)

+         we look at top-level instances and inert Givens

+       - tryEqFunDeps: for type-family equalities (F t1 .. tn ~ ty)

+         we look at top-level family instances

+                    and inert Given family equalities

+* Step (2). We use `solveFunDeps` to solve the [FunDepEqn] in a nested

+  solver.  Key property:

+

+      The ONLY effect of `solveFunDeps` is possibly to perform unifications:

+      - It entirely discards any unsolved fundep equalities.

+

+      - Ite entirely discards any evidence arising from solving fundep equalities

+

+* Step (3) if we did any unifications in Step (2), we start again with the

+  current unsolved Wanted.  It might now be soluble!

+

+* For Given constraints, things are different:

+    - tryDictFunDeps: we do nothing

+    - tryEqFunDeps: for type-family equalities, we can produce new

+        actual evidence for built-in type families.  E.g.

+             [G] co : 3 ~ x + 1

+        We can produce new evidence

+             [G] co' : x ~ 2

+  So we generate and emit fresh Givens.  See

+     `improveGivenTopFunEqs` and `improveGivenLocalFunEqs`

+  No unification is involved here, just emitting new Givens.

+

+(FD1) Consequences for error messages.

+  Because we discard any unsolved FunDepEqns, we get better error messages.

+  Consider   class C a b | a -> b

+             instance C Int Bool

+  and [W] C Int Char

+  We'll get an insoluble fundep-equality  (Char ~ Bool), but it's very

+  unhelpful to report it.  Much better just to say

+     No instance for C Int Bool

+

+  Similarly if had [W] C Int S, [W] C Int T, it is not helpful to

+  complain about insoluble (S ~ T).

+Note [Partial functional dependencies]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+Consider this (#12522):

+  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 fundep equalities

+  [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 is crucial that, when solving,

+  we unify    gamma1 := alpha    (YES)

+  and not     alpha := gamma1    (NO)

+Why?  Because if we do (YES) we'll think we have made some progress

+(some unification has happened), and hence go round again; but actually all we

+have done is to replace `alpha` with `gamma1`.

+These "fresh unification variables" in fundep-equalities are ubituitous.

+For example

+      class C a b | a -> b

+      instance .. => C Int [x]

+If we see

+      [W] C Int alpha

+we'll generate a fundep-equality   [W] alpha ~ [beta1]

+where `beta1` is one of those "fresh unification variables

+This problem shows up in several guises; see (at the bottom)

+  * Historical Note [Improvement orientation]

+  * Historical Note [Fundeps with instances, and equality orientation]

+The solution is super-simple:

+  * A fundep-equality is described by `FunDepEqn`, whose `fd_qtvs` field explicitly

+    lists the "fresh variables"

+  * Function `instantiateFunDepEqn` instantiates a `FunDepEqn`, and CRUCIALLY

+    gives the new unification variables a level one deeper than the current

+    level.

+  * Now, given `alpha ~ beta`, all the unification machinery guarantees, to

+    unify the variable with the deeper level.  See GHC.Tc.Utils.Unify

+    Note [Deeper level on the left].  That ensures that the fresh `gamma1`

+    will be eliminated in favour of `alpha`. Hooray.

+  * Better still, we solve the [FunDepEqn] with

+      solveFunDeps :: CtEvidence -> [FunDepEqn] -> TcS Bool

+    It uses `reportUnifications` to see if any unification happened at this

+    level or outside -- that is, it does NOT report unifications to the fresh

+    unification variables.  So `solveFunDeps` returns True only if it

+    unifies a variable /other than/ the fresh ones.  Bingo.

+Another victory for levels numbers!

+  respectively.  That would generate (b~Bool), which would fail.  I think

+

+{- *********************************************************************

+*                                                                      *

+*          Functional dependencies for dictionaries

+*                                                                      *

+********************************************************************* -}

+

+                     -- See (DFL1) of Note [Do fundeps last]

+  = do { fd_eqns <- improve_wanted_top_fun_eqs fam_tc args rhs_ty

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

+       ; solveFunDeps ev fd_eqns }

+improve_wanted_top_fun_eqs :: TyCon -> [TcType] -> Xi -> TcS [FunDepEqn]

+  = return [FDEqn { fd_qtvs = []

+                  , fd_eqs = map snd $ tryInteractTopFam ops fam_tc lhs_tys rhs_ty }]

+         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?

+improve_injective_wanted_top :: FamInstEnvs -> [Bool] -> TyCon

+                             -> [TcType] -> Xi -> TcS [FunDepEqn]

+-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are

+    do_one :: CoAxBranch -> TcS [FunDepEqn]

+           ; let branch_lhs_tys' = substTys subst1 branch_lhs_tys

+           ; if apartnessCheck branch_lhs_tys' branch

+             then do { traceTcS "improv_inj_top1" (ppr branch_lhs_tys')

+                     ; return [mkInjectivityFDEqn inj_args branch_lhs_tys' lhs_tys] }

+improve_injective_wanted_famfam :: [Bool] -> TyCon -> [TcType] -> Xi -> [FunDepEqn]

+-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are

+  = [mkInjectivityFDEqn inj_args lhs_tys rhs_tys]

+mkInjectivityFDEqn :: [Bool] -> [TcType] -> [TcType] -> FunDepEqn

+--   return the FDEqn { fd_eqs = [Pair s1 t1, Pair s3 t3] }

+-- The injectivity flags [Bool] will not all be False, but nothing goes wrong if they are

+mkInjectivityFDEqn inj_args lhs_args rhs_args

+  = FDEqn { fd_qtvs = [], fd_eqs = eqs }

+  where

+    eqs = [ Pair lhs_arg rhs_arg

+          | (True, lhs_arg, rhs_arg) <- zip3 inj_args lhs_args rhs_args ]

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

+      = [FDEqn { fd_qtvs = [], fd_eqs = map snd $ tryInteractInertFam ops fam_tc args iargs }]

+    do_one_injective inj_args rhs (EqCt { eq_lhs = TyFamLHS _ inert_args, eq_rhs = irhs })

+      = [mkInjectivityFDEqn inj_args args inert_args]

+{- *********************************************************************

+********************************************************************* -}

+-- The returned Bool is True if some unifications happened

+--

+-- See Note [Overview of fundeps]

+  = return False -- Common case no-op

+             <- reportUnifications $

+                nestFunDepsTcS     $

+                do { (_, eqs) <- wrapUnifier work_ev Nominal do_fundeps

+       -- ToDo: is this still a problem?

+

+{- 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 wrapUnifierAndEmit, which will fail, adding these

+to the work list. However, 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'.

+

+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.

+

+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.

+

+In general, I believe this is (now, anyway) just an optimisation, not required

+to avoid loops.

+-}

+

+{- *********************************************************************

+*                                                                      *

+                 Historical notes

+

+     Here are a bunch of Notes that are rendered obselete by

+          Note [Partial functional dependencies]

+

+*                                                                      *

+********************************************************************* -}

+

+{-

+Historical 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.

+

+--->  ToDo: all this fragility has gone away!   Fix the Note! <---

+

+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.

+

+Historical Note [Fundeps with instances, and equality orientation]

+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

+This Note describes a delicate interaction that constrains the orientation of

+equalities. This one is about fundeps, but the /exact/ same thing arises for

+type-family injectivity constraints: see Note [Improvement orientation].

+

+doTopFunDepImprovement compares the constraint with all the instance

+declarations, to see if we can produce any equalities. E.g

+   class C2 a b | a -> b

+   instance C Int Bool

+Then the constraint (C Int ty) generates the equality [W] ty ~ Bool.

+

+There is a nasty corner in #19415 which led to the typechecker looping:

+   class C s t b | s -> t

+   instance ... => C (T kx x) (T ky y) Int

+   T :: forall k. k -> Type

+

+   work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char

+      where kb0, b0 are unification vars

+

+   ==> {doTopFunDepImprovement: compare work_item with instance,

+        generate /fresh/ unification variables kfresh0, yfresh0,

+        emit a new Wanted, and add dwrk to inert set}

+

+   Suppose we emit this new Wanted from the fundep:

+       [W] T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0)

+

+   ==> {solve that equality kb0 := kfresh0, b0 := yfresh0}

+   Now kick out dwrk, since it mentions kb0

+   But now we are back to the start!  Loop!

+

+NB1: This example relies on an instance that does not satisfy the

+     coverage condition (although it may satisfy the weak coverage

+     condition), and hence whose fundeps generate fresh unification

+     variables.  Not satisfying the coverage condition is known to

+     lead to termination trouble, but in this case it's plain silly.

+

+NB2: In this example, the third parameter to C ensures that the

+     instance doesn't actually match the Wanted, so we can't use it to

+     solve the Wanted

+

+We solve the problem by (#21703):

+

+    carefully orienting the new Wanted so that all the

+    freshly-generated unification variables are on the LHS.

+

+    Thus we call unifyWanteds on

+       T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0)

+    and /NOT/

+       T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0)

+

+Now we'll unify kfresh0:=kb0, yfresh0:=b0, and all is well.  The general idea

+is that we want to preferentially eliminate those freshly-generated

+unification variables, rather than unifying older variables, which causes

+kick-out etc.

+

+Keeping younger variables on the left also gives very minor improvement in

+the compiler performance by having less kick-outs and allocations (-0.1% on

+average).  Indeed Historical Note [Eliminate younger unification variables]

+in GHC.Tc.Utils.Unify describes an earlier attempt to do so systematically,

+apparently now in abeyance.

+

+But this is is a delicate solution. We must take care to /preserve/

+orientation during solving. Wrinkles:

+

+(W1) We start with

+       [W] T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0)

+     Decompose to

+       [W] kfresh0 ~ kb0

+       [W] (yfresh0::kfresh0) ~ (b0::kb0)

+     Preserve orientation when decomposing!!

+

+(W2) Suppose we happen to tackle the second Wanted from (W1)

+     first. Then in canEqCanLHSHetero we emit a /kind/ equality, as

+     well as a now-homogeneous type equality

+       [W] kco : kfresh0 ~ kb0