Killing cc_fundeps, streamlining kind equality orientation, and type equality processing order

Fixes: #217093
Associated to #19415

This change
* Flips the orientation of the the generated kind equality coercion in canEqLHSHetero;
* Removes `cc_fundeps` in CDictCan as the check was incomplete;
* Changes `canDecomposableTyConAppOk` to ensure we process kind equalities before type equalities and avoiding a call to `canEqLHSHetero` while processing wanted TyConApp equalities
* Adds 2 new tests for validating the change
   - testsuites/typecheck/should_compile/T21703.hs and
   - testsuites/typecheck/should_fail/T19415b.hs (a simpler version of T19415.hs)
* Misc: Due to the change in the equality direction some error messages now have flipped type mismatch errors
* Changes in Notes:
  - Note [Fundeps with instances, and equality orientation] supercedes Note [Fundeps with instances]
  - Added Note [Kind Equality Orientation] to visualize the kind flipping
  - Added Note [Decomposing Dependent TyCons and Processing Wanted Equalties]

20 files changed, 318 insertions, 123 deletions

diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index 2f0af16168..41ae8fab36 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -113,10 +113,9 @@ canonicalize (CIrredCan { cc_ev = ev })
     --    e.g. a ~ [a], where [G] a ~ [Int], can decompose
 
 canonicalize (CDictCan { cc_ev = ev, cc_class  = cls
-                       , cc_tyargs = xis, cc_pend_sc = pend_sc
-                       , cc_fundeps = fds })
+                       , cc_tyargs = xis, cc_pend_sc = pend_sc })
   = {-# SCC "canClass" #-}
-    canClass ev cls xis pend_sc fds
+    canClass ev cls xis pend_sc
 
 canonicalize (CEqCan { cc_ev     = ev
                      , cc_lhs    = lhs
@@ -156,7 +155,7 @@ canClassNC ev cls tys
   | isGiven ev  -- See Note [Eagerly expand given superclasses]
   = do { sc_cts <- mkStrictSuperClasses ev [] [] cls tys
        ; emitWork sc_cts
-       ; canClass ev cls tys False fds }
+       ; canClass ev cls tys False }
 
   | CtWanted { ctev_rewriters = rewriters } <- ev
   , Just ip_name <- isCallStackPred cls tys
@@ -182,20 +181,17 @@ canClassNC ev cls tys
                                   (ctLocSpan loc) (ctEvExpr new_ev)
        ; solveCallStack ev ev_cs
 
-       ; canClass new_ev cls tys
-                  False -- No superclasses
-                  False -- No top level instances for fundeps
+       ; canClass new_ev cls tys False -- No superclasses
        }
 
   | otherwise
-  = canClass ev cls tys (has_scs cls) fds
+  = canClass ev cls tys (has_scs cls)
 
   where
     has_scs cls = not (null (classSCTheta cls))
     loc  = ctEvLoc ev
     orig = ctLocOrigin loc
     pred = ctEvPred ev
-    fds  = classHasFds cls
 
 solveCallStack :: CtEvidence -> EvCallStack -> TcS ()
 -- Also called from GHC.Tc.Solver when defaulting call stacks
@@ -210,11 +206,10 @@ solveCallStack ev ev_cs = do
 canClass :: CtEvidence
          -> Class -> [Type]
          -> Bool            -- True <=> un-explored superclasses
-         -> Bool            -- True <=> unexploited fundep(s)
          -> TcS (StopOrContinue Ct)
 -- Precondition: EvVar is class evidence
 
-canClass ev cls tys pend_sc fds
+canClass ev cls tys pend_sc
   = -- all classes do *nominal* matching
     assertPpr (ctEvRole ev == Nominal) (ppr ev $$ ppr cls $$ ppr tys) $
     do { (redns@(Reductions _ xis), rewriters) <- rewriteArgsNom ev cls_tc tys
@@ -222,8 +217,7 @@ canClass ev cls tys pend_sc fds
              mk_ct new_ev = CDictCan { cc_ev = new_ev
                                      , cc_tyargs = xis
                                      , cc_class = cls
-                                     , cc_pend_sc = pend_sc
-                                     , cc_fundeps = fds }
+                                     , cc_pend_sc = pend_sc }
        ; mb <- rewriteEvidence rewriters ev redn
        ; traceTcS "canClass" (vcat [ ppr ev
                                    , ppr xi, ppr mb ])
@@ -671,7 +665,7 @@ mk_superclasses_of rec_clss ev tvs theta cls tys
 
     this_ct | null tvs, null theta
             = CDictCan { cc_ev = ev, cc_class = cls, cc_tyargs = tys
-                       , cc_pend_sc = loop_found, cc_fundeps = classHasFds cls }
+                       , cc_pend_sc = loop_found }
                  -- NB: If there is a loop, we cut off, so we have not
                  --     added the superclasses, hence cc_pend_sc = True
             | otherwise
@@ -1534,6 +1528,7 @@ canTyConApp :: CtEvidence -> EqRel
             -> TyCon -> [TcType]
             -> TcS (StopOrContinue Ct)
 -- See Note [Decomposing TyConApp equalities]
+-- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
 -- Neither tc1 nor tc2 is a saturated funTyCon, nor a type family
 -- But they can be data families.
 canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -1620,6 +1615,7 @@ do so on the spot.  An important special case is where s1=s2,
 and we get just Refl.
 
 So canDecomposableTyConAppOK uses unifyWanted etc to short-cut that work.
+See also Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
 
 Note [Decomposing TyConApp equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -1948,7 +1944,7 @@ Extra points
 canDecomposableTyConAppOK :: CtEvidence -> EqRel
                           -> TyCon -> [TcType] -> [TcType]
                           -> TcS (StopOrContinue Ct)
--- Precondition: tys1 and tys2 are the same length, hence "OK"
+-- Precondition: tys1 and tys2 are the same finite length, hence "OK"
 canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
   = assert (tys1 `equalLength` tys2) $
     do { traceTcS "canDecomposableTyConAppOK"
@@ -1956,10 +1952,12 @@ canDecomposableTyConAppOK ev eq_rel tc tys1 tys2
        ; case ev of
            CtWanted { ctev_dest = dest, ctev_rewriters = rewriters }
                   -- new_locs and tc_roles are both infinite, so
-                  -- we are guaranteed that cos has the same length
+                  -- we are guaranteed that cos has the same lengthm
                   -- as tys1 and tys2
-             -> do { cos <- zipWith4M (unifyWanted rewriters) new_locs tc_roles tys1 tys2
-                            -- See Note [Fast path when decomposing TyConApps]
+                  -- See Note [Fast path when decomposing TyConApps]
+                  -- Caution: unifyWanteds is order sensitive
+                  -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
+             -> do { cos <- unifyWanteds rewriters new_locs tc_roles tys1 tys2
                    ; setWantedEq dest (mkTyConAppCo role tc cos) }
 
            CtGiven { ctev_evar = evar }
@@ -2192,6 +2190,35 @@ canEqCanLHS ev eq_rel swapped lhs1 ps_xi1 xi2 ps_xi2
     k1 = canEqLHSKind lhs1
     k2 = typeKind xi2
 
+
+{-
+Note [Kind Equality Orientation]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+While in theory [W] x ~ y and [W] y ~ x ought to give us the same behaviour, in practice it does not.
+See Note [Fundeps with instances, and equality orientation] where this is discussed at length.
+As a rule of thumb: we keep the newest unification variables on the left of the equality.
+See also Note [Improvement orientation] in GHC.Tc.Solver.Interact.
+
+In particular, `canEqCanLHSHetero` produces the following constraint equalities
+
+[X] (xi1 :: ki1) ~ (xi2 :: ki2)
+  -->  [X] kco :: ki1 ~ ki2
+       [X] co : xi1 :: ki1 ~ (xi2 |> sym kco) :: ki1
+
+Note that the types in the LHS of the new constraints are the ones that were on the LHS of
+the original constraint.
+
+--- Historical note ---
+We prevously used to flip the kco to avoid using a sym in the cast
+
+[X] (xi1 :: ki1) ~ (xi2 :: ki2)
+  -->  [X] kco :: ki2 ~ ki1
+       [X] co : xi1 :: ki1 ~ (xi2 |> kco) :: ki1
+
+But this sent solver in an infinite loop (see #19415).
+-- End of historical note --
+-}
+
 canEqCanLHSHetero :: CtEvidence         -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
                   -> EqRel -> SwapFlag
                   -> CanEqLHS           -- xi1
@@ -2201,46 +2228,50 @@ canEqCanLHSHetero :: CtEvidence         -- :: (xi1 :: ki1) ~ (xi2 :: ki2)
                   -> TcS (StopOrContinue Ct)
 canEqCanLHSHetero ev eq_rel swapped lhs1 ki1 xi2 ki2
   -- See Note [Equalities with incompatible kinds]
-  = do { (kind_ev, kind_co) <- mk_kind_eq   -- :: ki2 ~N ki1
+  -- See Note [Kind Equality Orientation]
+  -- NB: preserve left-to-right orientation!!
+  -- See Note [Fundeps with instances, and equality orientation]
+  --     wrinkle (W2) in GHC.Tc.Solver.Interact
+  = do { (kind_ev, kind_co) <- mk_kind_eq   -- :: ki1 ~N ki2
 
-       ; let  -- kind_co :: (ki2 :: *) ~N (ki1 :: *)   (whether swapped or not)
+       ; let  -- kind_co :: (ki1 :: *) ~N (ki2 :: *)   (whether swapped or not)
              lhs_redn = mkReflRedn role xi1
-             rhs_redn = mkGReflRightRedn role xi2 kind_co
+             rhs_redn = mkGReflRightRedn role xi2 (mkSymCo kind_co)
 
              -- See Note [Equalities with incompatible kinds], Wrinkle (1)
              -- This will be ignored in rewriteEqEvidence if the work item is a Given
              rewriters = rewriterSetFromCo kind_co
 
        ; traceTcS "Hetero equality gives rise to kind equality"
-           (ppr kind_co <+> dcolon <+> sep [ ppr ki2, text "~#", ppr ki1 ])
+           (ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
        ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
 
        ; emitWorkNC [type_ev]  -- delay the type equality until after we've finished
                                -- the kind equality, which may unlock things
                                -- See Note [Equalities with incompatible kinds]
 
-       ; canEqNC kind_ev NomEq ki2 ki1 }
+       ; canEqNC kind_ev NomEq ki1 ki2 }
   where
     mk_kind_eq :: TcS (CtEvidence, CoercionN)
     mk_kind_eq = case ev of
       CtGiven { ctev_evar = evar }
-        -> do { let kind_co = maybe_sym $ mkKindCo (mkCoVarCo evar)  -- :: k2 ~ k1
+        -> do { let kind_co = maybe_sym $ mkKindCo (mkCoVarCo evar) -- :: k1 ~ k2
               ; kind_ev <- newGivenEvVar kind_loc (kind_pty, evCoercion kind_co)
               ; return (kind_ev, ctEvCoercion kind_ev) }
 
       CtWanted { ctev_rewriters = rewriters }
-        -> newWantedEq kind_loc rewriters Nominal ki2 ki1
+        -> newWantedEq kind_loc rewriters Nominal ki1 ki2
 
     xi1      = canEqLHSType lhs1
     loc      = ctev_loc ev
     role     = eqRelRole eq_rel
     kind_loc = mkKindLoc xi1 xi2 loc
-    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki2 ki1
+    kind_pty = mkHeteroPrimEqPred liftedTypeKind liftedTypeKind ki1 ki2
 
     maybe_sym = case swapped of
-          IsSwapped  -> id         -- if the input is swapped, then we already
-                                   -- will have k2 ~ k1
-          NotSwapped -> mkSymCo
+          IsSwapped  -> mkSymCo         -- if the input is swapped, then we
+                                        -- will have k2 ~ k1, so flip it to k1 ~ k2
+          NotSwapped -> id
 
 -- guaranteed that typeKind lhs == typeKind rhs
 canEqCanLHSHomo :: CtEvidence
@@ -2550,8 +2581,8 @@ k2 and use this to cast. To wit, from
 
 (where [X] is [G] or [W]), we go to
 
-  [X] co :: k2 ~ k1
-  [X] (tv :: k1) ~ ((rhs |> co) :: k1)
+  [X] co :: k1 ~ k2
+  [X] (tv :: k1) ~ ((rhs |> sym co) :: k1)
 
 We carry on with the *kind equality*, not the type equality, because
 solving the former may unlock the latter. This choice is made in
@@ -2564,7 +2595,7 @@ Wrinkles:
      for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
      This is done in canEqCanLHSHetero.
 
- (2) If we have [W] w :: alpha ~ (rhs |> co_hole), should we unify alpha? No.
+ (2) If we have [W] w :: alpha ~ (rhs |> sym co_hole), should we unify alpha? No.
      The problem is that the wanted w is effectively rewritten by another wanted,
      and unifying alpha effectively promotes this wanted to a given. Doing so
      means we lose track of the rewriter set associated with the wanted.
@@ -2582,8 +2613,8 @@ Wrinkles:
      unifyTest in canEqTyVarFunEq.
 
  (3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
-     algorithm detailed here, producing [W] co :: k2 ~ k1, and adding
-     [W] (a :: k1) ~ ((rhs |> co) :: k1) to the irreducibles. Some time
+     algorithm detailed here, producing [W] co :: k1 ~ k2, and adding
+     [W] (a :: k1) ~ ((rhs |> sym co) :: k1) to the irreducibles. Some time
      later, we solve co, and fill in co's coercion hole. This kicks out
      the irreducible as described in (2).
      But now, during canonicalization, we see the cast
@@ -3238,3 +3269,55 @@ unifyWanted rewriters loc role orig_ty1 orig_ty2
        | ty1 `tcEqType` ty2 = return (mkReflCo role ty1)
         -- Check for equality; e.g. a ~ a, or (m a) ~ (m a)
        | otherwise = emitNewWantedEq loc rewriters role orig_ty1 orig_ty2
+
+
+{-
+Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we decompose a dependent tycon we obtain a list of
+mixed wanted type and kind equalities. Ideally we want
+all the kind equalities to get solved first so that we avoid
+generating duplicate kind equalities
+
+For example, consider decomposing a TyCon equality
+
+    (0) [W] T k_fresh (t1::k_fresh) ~ T k1 (t2::k_fresh)
+
+This gives rise to 2 equalities in the solver worklist
+
+    (1) [W] k_fresh ~ k1
+    (2) [W] t1::k_fresh ~ t2::k1
+
+The solver worklist is processed in LIFO order:
+see GHC.Tc.Solver.InertSet.selectWorkItem.
+i.e. (2) is processed _before_ (1). Now, while solving (2)
+we would call `canEqCanLHSHetero` and that would emit a
+wanted kind equality
+
+    (3) [W] k_fresh ~ k1
+
+But (3) is exactly the same as (1)!
+
+To avoid such duplicate wanted constraints from being added to the worklist,
+we ensure that (2) is processed before (1). Since we are processing
+the worklist in a LIFO ordering, we do it by emitting (1) before (2).
+This is exactly what we do in `unifyWanteds`.
+
+NB: This ordering is not needed when we decompose FunTyCons as they are not dependently typed
+-}
+
+-- NB: Length of [CtLoc] and [Roles] may be infinite
+-- but list of RHS [TcType] and LHS [TcType] is finite and both are of equal length
+unifyWanteds :: RewriterSet -> [CtLoc] -> [Role]
+             -> [TcType] -- List of RHS types
+             -> [TcType] -- List of LHS types
+             -> TcS [Coercion]
+unifyWanteds rewriters ctlocs roles rhss lhss = unify_wanteds rewriters $ zip4 ctlocs roles rhss lhss
+  where
+    -- Order is important here
+    -- See Note [Decomposing Dependent TyCons and Processing Wanted Equalities]
+    unify_wanteds _ [] = return []
+    unify_wanteds rewriters ((new_loc, tc_role, ty1, ty2) : rest)
+       = do { cos <- unify_wanteds rewriters rest
+            ; co  <- unifyWanted rewriters new_loc tc_role ty1 ty2
+            ; return (co:cos) }
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index f17b520c94..37c8dd6d01 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -1732,8 +1732,12 @@ Then it is solvable, but its very hard to detect this on the spot.
 It's exactly the same with implicit parameters, except that the
 "aggressive" approach would be much easier to implement.
 
-Note [Fundeps with instances]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+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
@@ -1747,52 +1751,122 @@ There is a nasty corner in #19415 which led to the typechecker looping:
 
    work_item: dwrk :: C (T @ka (a::ka)) (T @kb0 (b0::kb0)) Char
       where kb0, b0 are unification vars
-   ==> {fundeps against instance; k0, y0 fresh unification vars}
-       [W] T kb0 (b0::kb0) ~ T k0 (y0::k0)
-       Add dwrk to inert set
-   ==> {solve that equality kb0 := k0, b0 := y0
-   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), which is known to lead to termination trouble
-
-NB2: if the unification was the other way round, k0:=kb0, all would be
-well.  It's a very delicate problem.
-
-The ticket #19415 discusses various solutions, but the one we adopted
-is very simple:
-
-* There is a flag in CDictCan (cc_fundeps :: Bool)
 
-* cc_fundeps = True means
-    a) The class has fundeps
-    b) We have not had a successful hit against instances yet
+   ==> {doTopFundepImprovement: compare work_item with instance,
+        generate /fresh/ unification variables kfresh0, yfresh0,
+        emit a new Wanted, and add dwrk to inert set}
 
-* In doTopFundepImprovement, if we emit some constraints we flip the flag
-  to False, so that we won't try again with the same CDictCan.  In our
-  example, dwrk will have its flag set to False.
+   Suppose we emit this new Wanted from the fundep:
+       [W] T kb0 (b0::kb0) ~ T kfresh0 (yfresh0::kfresh0)
 
-* Not that if we have no "hits" we must /not/ flip the flag. We might have
-      dwrk :: C alpha beta Char
-  which does not yet trigger fundeps from the instance, but later we
-  get alpha := T ka a.  We could be cleverer, and spot that the constraint
-  is such that we will /never/ get any hits (no unifiers) but we don't do
-  that yet.
-
-Easy!  What could go wrong?
-* Maybe the class has multiple fundeps, and we get hit with one but not
-  the other.  Per-fundep flags?
-* Maybe we get a hit against one instance with one fundep but, after
-  the work-item is instantiated a bit more, we get a second hit
-  against a second instance.  (This is a pretty strange and
-  undesirable thing anyway, and can only happen with overlapping
-  instances; one example is in Note [Weird fundeps].)
+   ==> {solve that equality kb0 := kfresh0, b0 := yfresh0}
+   Now kick out dwrk, since it mentions kb0
+   But now we are back to the start!  Loop!
 
-But both of these seem extremely exotic, and ignoring them threatens
-completeness (fixable with some type signature), but not termination
-(not fixable).  So for now we are just doing the simplest thing.
+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 emit
+       [W] T kfresh0 (yfresh0::kfresh0) ~ T kb0 (b0::kb0)
+    and /NOT/
+       [W] 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 orientiation 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
+       [W] (yfresh0::kfresh0) ~ (b0::kb0) |> (sym kco)
+     Preserve orientation in canEqCanLHSHetero!!  (Failing to
+     preserve orientation here was the immediate cause of #21703.)
+
+(W3) There is a potential interaction with the swapping done by
+     GHC.Tc.Utils.Unify.swapOverTyVars.  We think it's fine, but it's
+     a slight worry.  See especially Note [TyVar/TyVar orientation] in
+     that module.
+
+The trouble is that "preserving orientation" is a rather global invariant,
+and sometimes we definitely do want to swap (e.g. Int ~ alpha), so we don't
+even have a precise statement of what the invariant is.  The advantage
+of the preserve-orientation plan is that it is extremely cheap to implement,
+and apparently works beautifully.
+
+--- Alternative plan (1) ---
+Rather than have an ill-defined invariant, another possiblity is to
+elminate those fresh unification variables at birth, when generating
+the new fundep-inspired equalities.
+
+The key idea is to call `instFlexiX` in `emitFunDepWanteds` on only those
+type variables that are guaranteed to give us some progress. This means we
+have to locally (without calling emitWanteds) identify the type variables
+that do not give us any progress.  In the above example, we _know_ that
+emitting the two wanteds `kco` and `co` is fruitless.
+
+  Q: How do we identify such no-ops?
+
+  1. Generate a matching substitution from LHS to RHS
+        ɸ = [kb0 :-> k0, b0 :->  y0]
+  2. Call `instFlexiX` on only those type variables that do not appear in the domain of ɸ
+        ɸ' = instFlexiX ɸ (tvs - domain ɸ)
+  3. Apply ɸ' on LHS and then call emitWanteds
+        unifyWanteds ... (subst ɸ' LHS) RHS
+
+Why will this work?  The matching substitution ɸ will be a best effort
+substitution that gives us all the easy solutions. It can be generated with
+modified version of `Core/Unify.unify_tys` where we run it in a matching mode
+and never generate `SurelyApart` and always return a `MaybeApart Subst`
+instead.
+
+The same alternative plan would work for type-family injectivity constraints:
+see Note [Improvement orientation].
+--- End of Alternative plan (1) ---
+
+--- Alternative plan (2) ---
+We could have a new flavour of TcTyVar (like `TauTv`, `TyVarTv` etc; see GHC.Tc.Utils.TcType.MetaInfo)
+for the fresh unification variables introduced by functional dependencies.  Say `FunDepTv`.  Then in
+GHC.Tc.Utils.Unify.swapOverTyVars we could arrange to keep a `FunDepTv` on the left if possible.
+Looks possible, but it's one more complication.
+--- End of Alternative plan (2) ---
+
+
+--- Historical note: Failed Alternative Plan (3) ---
+Previously we used a flag `cc_fundeps` in `CDictCan`. It would flip to False
+once we used a fun dep to hint the solver to break and to stop emitting more
+wanteds.  This solution was not complete, and caused a failures while trying
+to solve for transitive functional dependencies (test case: T21703)
+-- End of Historical note: Failed Alternative Plan (3) --
 
 Note [Weird fundeps]
 ~~~~~~~~~~~~~~~~~~~~
@@ -1819,22 +1893,15 @@ as the fundeps.
 doTopFundepImprovement :: Ct -> TcS (StopOrContinue Ct)
 -- Try to functional-dependency improvement between the constraint
 -- and the top-level instance declarations
--- See Note [Fundeps with instances]
+-- See Note [Fundeps with instances, and equality orientation]
 -- See also Note [Weird fundeps]
 doTopFundepImprovement work_item@(CDictCan { cc_ev = ev, cc_class = cls
-                                           , cc_tyargs = xis
-                                           , cc_fundeps = has_fds })
-  | has_fds
+                                           , cc_tyargs = xis })
   = do { traceTcS "try_fundeps" (ppr work_item)
        ; instEnvs <- getInstEnvs
        ; let fundep_eqns = improveFromInstEnv instEnvs mk_ct_loc cls xis
-       ; case fundep_eqns of
-           [] -> continueWith work_item  -- No improvement
-           _  -> do { emitFunDepWanteds (ctEvRewriters ev) fundep_eqns
-                    ; continueWith (work_item { cc_fundeps = False }) } }
-  | otherwise
-  = continueWith work_item
-
+       ; emitFunDepWanteds (ctEvRewriters ev) fundep_eqns
+       ; continueWith work_item }
   where
      dict_pred   = mkClassPred cls xis
      dict_loc    = ctEvLoc ev
@@ -1852,7 +1919,10 @@ doTopFundepImprovement work_item = pprPanic "doTopFundepImprovement" (ppr work_i
 
 emitFunDepWanteds :: RewriterSet  -- from the work item
                   -> [FunDepEqn (CtLoc, RewriterSet)] -> TcS ()
+
+emitFunDepWanteds _ [] = return () -- common case noop
 -- See Note [FunDep and implicit parameter reactions]
+
 emitFunDepWanteds work_rewriters fd_eqns
   = mapM_ do_one_FDEqn fd_eqns
   where
@@ -2134,6 +2204,9 @@ we do *not* need to expand type synonyms because the matcher will do that for us
 
 Note [Improvement orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Fundeps with instances, and equality orientation], which describes
+the Exact Same Prolem, 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
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index 475437701c..a876522913 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -197,17 +197,11 @@ data Ct
       cc_class  :: Class,
       cc_tyargs :: [Xi],   -- cc_tyargs are rewritten w.r.t. inerts, so Xi
 
-      cc_pend_sc :: Bool,
+      cc_pend_sc :: Bool
           -- See Note [The superclass story] in GHC.Tc.Solver.Canonical
           -- True <=> (a) cc_class has superclasses
           --          (b) we have not (yet) added those
           --              superclasses as Givens
-
-      cc_fundeps :: Bool
-          -- See Note [Fundeps with instances] in GHC.Tc.Solver.Interact
-          -- True <=> the class has fundeps, and we have not yet
-          --          compared this constraint with the global
-          --          instances for fundep improvement
     }
 
   | CIrredCan {  -- These stand for yet-unusable predicates
@@ -676,10 +670,8 @@ instance Outputable Ct where
       pp_sort = case ct of
          CEqCan {}        -> text "CEqCan"
          CNonCanonical {} -> text "CNonCanonical"
-         CDictCan { cc_pend_sc = psc, cc_fundeps = fds }
-            | psc, fds     -> text "CDictCan(psc,fds)"
-            | psc, not fds -> text "CDictCan(psc)"
-            | not psc, fds -> text "CDictCan(fds)"
+         CDictCan { cc_pend_sc = psc }
+            | psc          -> text "CDictCan(psc)"
             | otherwise    -> text "CDictCan"
          CIrredCan { cc_reason = reason } -> text "CIrredCan" <> ppr reason
          CQuantCan (QCI { qci_pend_sc = pend_sc })
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index f7e1ec938a..41faa2fece 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -2307,6 +2307,9 @@ Needless to say, all there are wrinkles:
 
 Note [TyVar/TyVar orientation]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [Fundeps with instances, and equality orientation]
+where the kind equality orientation is important
+
 Given (a ~ b), should we orient the CEqCan as (a~b) or (b~a)?
 This is a surprisingly tricky question! This is invariant (TyEq:TV).
 
diff --git a/testsuite/tests/indexed-types/should_fail/T3330c.stderr b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
index be6103ace1..fad84899b1 100644
--- a/testsuite/tests/indexed-types/should_fail/T3330c.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T3330c.stderr
@@ -1,6 +1,6 @@
 
 T3330c.hs:25:43: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         f1 :: * -> *
         f1 x :: *
diff --git a/testsuite/tests/indexed-types/should_fail/T9662.stderr b/testsuite/tests/indexed-types/should_fail/T9662.stderr
index 20e0084aa2..43c8b26191 100644
--- a/testsuite/tests/indexed-types/should_fail/T9662.stderr
+++ b/testsuite/tests/indexed-types/should_fail/T9662.stderr
@@ -1,13 +1,13 @@
 
 T9662.hs:49:8: error: [GHC-25897]
-    • Couldn't match type ‘k’ with ‘Int’
+    • Couldn't match type ‘n’ with ‘Int’
       Expected: Exp (((sh :. k) :. m) :. n)
                 -> Exp (((sh :. m) :. n) :. k)
         Actual: Exp
                   (Tuple (((Atom a0 :. Atom Int) :. Atom Int) :. Atom Int))
                 -> Exp
                      (Plain (((Unlifted (Atom a0) :. Exp Int) :. Exp Int) :. Exp Int))
-      ‘k’ is a rigid type variable bound by
+      ‘n’ is a rigid type variable bound by
         the type signature for:
           test :: forall sh k m n.
                   Shape (((sh :. k) :. m) :. n) -> Shape (((sh :. m) :. n) :. k)
diff --git a/testsuite/tests/polykinds/T11399.stderr b/testsuite/tests/polykinds/T11399.stderr
index 80ebbf38ba..a3baab2378 100644
--- a/testsuite/tests/polykinds/T11399.stderr
+++ b/testsuite/tests/polykinds/T11399.stderr
@@ -1,6 +1,6 @@
 
 T11399.hs:10:32: error: [GHC-18872]
-    • Couldn't match kind ‘GHC.Types.RuntimeRep’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘GHC.Types.RuntimeRep’
       When matching kinds
         a :: * -> *
         TYPE :: GHC.Types.RuntimeRep -> *
diff --git a/testsuite/tests/polykinds/T14172.stderr b/testsuite/tests/polykinds/T14172.stderr
index df3868fb6c..45ff51c259 100644
--- a/testsuite/tests/polykinds/T14172.stderr
+++ b/testsuite/tests/polykinds/T14172.stderr
@@ -12,11 +12,9 @@ T14172.hs:7:46: error: [GHC-88464]
         traverseCompose :: (a -> f b) -> g a -> f (h _)
 
 T14172.hs:8:19: error: [GHC-25897]
-    • Couldn't match type ‘a’ with ‘g'1 a'0’
-      Expected: (f'0 a -> f (f'0 b)) -> g a -> f (h a')
-        Actual: (Unwrapped (Compose f'0 g'1 a'0) -> f (Unwrapped (h a')))
-                -> Compose f'0 g'1 a'0 -> f (h a')
-      ‘a’ is a rigid type variable bound by
+    • Couldn't match type ‘h’ with ‘Compose f'0 g'0’
+        arising from a use of ‘_Wrapping’
+      ‘h’ is a rigid type variable bound by
         the inferred type of
           traverseCompose :: (a -> f b) -> g a -> f (h a')
         at T14172.hs:7:1-47
diff --git a/testsuite/tests/rep-poly/T13929.stderr b/testsuite/tests/rep-poly/T13929.stderr
index 5c4a61b80d..fe8c845a8b 100644
--- a/testsuite/tests/rep-poly/T13929.stderr
+++ b/testsuite/tests/rep-poly/T13929.stderr
@@ -3,8 +3,8 @@ T13929.hs:29:24: error: [GHC-55287]
     • The tuple argument in first position
       does not have a fixed runtime representation.
       Its type is:
-        a0 :: TYPE c1
-      Cannot unify ‘rf’ with the type variable ‘c1’
+        a0 :: TYPE c0
+      Cannot unify ‘rf’ with the type variable ‘c0’
       because it is not a concrete ‘RuntimeRep’.
     • In the expression: (# gunbox x, gunbox y #)
       In an equation for ‘gunbox’:
@@ -12,7 +12,6 @@ T13929.hs:29:24: error: [GHC-55287]
       In the instance declaration for
         ‘GUnbox (f :*: g) (TupleRep [rf, rg])’
     • Relevant bindings include
-        x :: f p (bound at T13929.hs:29:13)
         gunbox :: (:*:) f g p -> GUnboxed (f :*: g) (TupleRep [rf, rg])
           (bound at T13929.hs:29:5)
 
diff --git a/testsuite/tests/typecheck/should_compile/T21703.hs b/testsuite/tests/typecheck/should_compile/T21703.hs
new file mode 100644
index 0000000000..352dbc72a2
--- /dev/null
+++ b/testsuite/tests/typecheck/should_compile/T21703.hs
@@ -0,0 +1,22 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module T21703 where
+
+data Doc
+data Val
+data Head
+
+data EvalM a = EvalM a
+
+class MonadEval head val m | m -> head, head -> val where
+  ret :: a -> m a       
+
+instance MonadEval Head Val EvalM where
+  ret = EvalM
+
+class PrettyM m a where
+  prettyM :: a -> m a
+
+instance PrettyM EvalM Val where
+  prettyM = ret
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index 46db37f854..876bcc0dda 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -812,6 +812,7 @@ test('StaticPtrTypeFamily', normal, compile, [''])
 test('T20946', normal, compile, [''])
 test('T20996', normal, compile, [''])
 test('T20732', normal, compile, [''])
+test('T21703', normal, compile, [''])
 test('T21010', [extra_files(['T21010A.hs', 'T21010B.hs'])], multimod_compile, ['T21010.hs', '-v0'])
 test('FunDepOrigin1', normal, compile, [''])
 test('FloatFDs', normal, compile, [''])
diff --git a/testsuite/tests/typecheck/should_fail/T19415.stderr b/testsuite/tests/typecheck/should_fail/T19415.stderr
index 075d10bd97..7135b2caff 100644
--- a/testsuite/tests/typecheck/should_fail/T19415.stderr
+++ b/testsuite/tests/typecheck/should_fail/T19415.stderr
@@ -2,9 +2,9 @@
 T19415.hs:27:8: error: [GHC-18872]
     • Couldn't match type ‘[Char]’ with ‘Char’
         arising from a functional dependency between:
-          constraint ‘SetField "name" (Pet a0) (Pet b) Char’
+          constraint ‘SetField "name" (Pet a) (Pet b) Char’
             arising from a use of ‘setField’
-          instance ‘SetField "name" (Pet a) (Pet b1) String’
+          instance ‘SetField "name" (Pet a1) (Pet b1) String’
             at T19415.hs:(23,3)-(24,60)
     • In the expression: setField @"name" 'c' (Pet "hi")
       In an equation for ‘loop’: loop = setField @"name" 'c' (Pet "hi")
diff --git a/testsuite/tests/typecheck/should_fail/T19415b.hs b/testsuite/tests/typecheck/should_fail/T19415b.hs
new file mode 100644
index 0000000000..af83f66fbe
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19415b.hs
@@ -0,0 +1,15 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Loopy where
+
+data T a = MkT -- this needs to be poly-kinded
+
+class Ping s t b | s -> t b where
+  foo :: b -> s -> t
+
+instance Ping (T a) (T b) Int => Ping (T a) (T b) Int where
+  foo _ _ = MkT
+
+loop = foo 'c' MkT
diff --git a/testsuite/tests/typecheck/should_fail/T19415b.stderr b/testsuite/tests/typecheck/should_fail/T19415b.stderr
new file mode 100644
index 0000000000..4e109730a3
--- /dev/null
+++ b/testsuite/tests/typecheck/should_fail/T19415b.stderr
@@ -0,0 +1,8 @@
+
+T19415b.hs:15:8: error: [GHC-18872]
+    • Couldn't match type ‘Int’ with ‘Char’
+        arising from a functional dependency between:
+          constraint ‘Ping (T a0) (T b) Char’ arising from a use of ‘foo’
+          instance ‘Ping (T a) (T b1) Int’ at T19415b.hs:12:10-53
+    • In the expression: foo 'c' MkT
+      In an equation for ‘loop’: loop = foo 'c' MkT
diff --git a/testsuite/tests/typecheck/should_fail/T3950.stderr b/testsuite/tests/typecheck/should_fail/T3950.stderr
index 6c3740b342..cba7dda734 100644
--- a/testsuite/tests/typecheck/should_fail/T3950.stderr
+++ b/testsuite/tests/typecheck/should_fail/T3950.stderr
@@ -1,6 +1,6 @@
 
 T3950.hs:16:13: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         w :: (* -> * -> *) -> *
         Sealed :: (* -> *) -> *
diff --git a/testsuite/tests/typecheck/should_fail/T7368.stderr b/testsuite/tests/typecheck/should_fail/T7368.stderr
index 26f1c251e2..1485c88084 100644
--- a/testsuite/tests/typecheck/should_fail/T7368.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368.stderr
@@ -1,6 +1,6 @@
 
 T7368.hs:3:10: error: [GHC-18872]
-    • Couldn't match kind ‘* -> *’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         b0 :: *
         Maybe :: * -> *
diff --git a/testsuite/tests/typecheck/should_fail/T7368a.stderr b/testsuite/tests/typecheck/should_fail/T7368a.stderr
index 28054f1f92..7f9c97bce7 100644
--- a/testsuite/tests/typecheck/should_fail/T7368a.stderr
+++ b/testsuite/tests/typecheck/should_fail/T7368a.stderr
@@ -1,6 +1,6 @@
 
 T7368a.hs:8:6: error: [GHC-18872]
-    • Couldn't match kind ‘* -> *’ with ‘*’
+    • Couldn't match kind ‘*’ with ‘* -> *’
       When matching types
         f :: * -> *
         Bad :: (* -> *) -> *
diff --git a/testsuite/tests/typecheck/should_fail/T8603.stderr b/testsuite/tests/typecheck/should_fail/T8603.stderr
index d369b2d0db..fcb1b8828b 100644
--- a/testsuite/tests/typecheck/should_fail/T8603.stderr
+++ b/testsuite/tests/typecheck/should_fail/T8603.stderr
@@ -1,6 +1,6 @@
 
 T8603.hs:33:17: error: [GHC-18872]
-    • Couldn't match kind ‘*’ with ‘* -> *’
+    • Couldn't match kind ‘* -> *’ with ‘*’
       When matching types
         m0 :: * -> *
         [a2] :: *
diff --git a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
index 671784b45e..bbb18280c7 100644
--- a/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
+++ b/testsuite/tests/typecheck/should_fail/TcCoercibleFail.stderr
@@ -10,8 +10,8 @@ TcCoercibleFail.hs:14:8: error: [GHC-18872]
     • Couldn't match representation of type: m Int
                                with that of: m Age
         arising from a use of ‘coerce’
-      NB: We cannot know what roles the parameters to ‘m’ have;
-        we must assume that the role is nominal
+        NB: We cannot know what roles the parameters to ‘m’ have;
+          we must assume that the role is nominal
     • In the first argument of ‘($)’, namely ‘coerce’
       In the expression: coerce $ (return one :: m Int)
       In an equation for ‘foo2’: foo2 = coerce $ (return one :: m Int)
@@ -29,8 +29,8 @@ TcCoercibleFail.hs:18:8: error: [GHC-18872]
     • Couldn't match representation of type ‘Int’
                                with that of ‘Down Int’
         arising from a use of ‘coerce’
-      The data constructor ‘Data.Ord.Down’
-        of newtype ‘Down’ is not in scope
+        The data constructor ‘Data.Ord.Down’
+          of newtype ‘Down’ is not in scope
     • In the first argument of ‘($)’, namely ‘coerce’
       In the expression: coerce $ one :: Down Int
       In an equation for ‘foo4’: foo4 = coerce $ one :: Down Int
@@ -50,7 +50,7 @@ TcCoercibleFail.hs:30:9: error: [GHC-18872]
 
 TcCoercibleFail.hs:35:8: error:
     • Reduction stack overflow; size = 201
-      When simplifying the following type: Fix (Either Int)
+      When simplifying the following type: Age
       Use -freduction-depth=0 to disable this check
       (any upper bound you could choose might fail unpredictably with
        minor updates to GHC, so disabling the check is recommended if
diff --git a/testsuite/tests/typecheck/should_fail/all.T b/testsuite/tests/typecheck/should_fail/all.T
index 646e5685c7..ab7821398a 100644
--- a/testsuite/tests/typecheck/should_fail/all.T
+++ b/testsuite/tests/typecheck/should_fail/all.T
@@ -630,6 +630,7 @@ test('T19397E3', extra_files(['T19397S.hs']), multimod_compile_fail,
 test('T19397E4', extra_files(['T19397S.hs']), multimod_compile_fail,
     ['T19397E4.hs', '-v0 -main-is foo'])
 test('T19415', normal, compile_fail, [''])
+test('T19415b', normal, compile_fail, [''])
 test('T19915', normal, compile_fail, [''])
 test('T19977a', normal, compile_fail, [''])
 test('T19977b', normal, compile_fail, [''])