GitLab

Simon Peyton Jones pushed to branch wip/T23162-spj at Glasgow Haskell Compiler / GHC

Commits:

46241879
by Simon Peyton Jones at 2025-07-07T16:05:46+01:00
```
Make FunDeps into a new module
```

e970a6b8

by Simon Peyton Jones at 2025-07-07T16:39:04+01:00

Solve new_eqs rather than adding them to WantedConstraints

6 changed files:

compiler/GHC/Tc/Solver/Dict.hs
compiler/GHC/Tc/Solver/Equality.hs
+ compiler/GHC/Tc/Solver/FunDeps.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Solver/Solve.hs
compiler/ghc.cabal.in

Changes:

compiler/GHC/Tc/Solver/Dict.hs

@@ -8,9 +8,6 @@ module GHC.Tc.Solver.Dict (
    matchLocalInst, chooseInstance,
    makeSuperClasses, mkStrictSuperClasses,
    solveCallStack,    -- For GHC.Tc.Solver
+-
 -  -- * Functional dependencies
 -  doDictFunDepImprovement
    ) where
  import GHC.Prelude
@@ -1379,346 +1376,6 @@ with the least superclass depth (see Note [Replacement vs keeping]),
  but that doesn't work for the example from #22216.
  -}
 -{- *********************************************************************
 -*                                                                      *
 -*          Functional dependencies, instantiation of equations
 -*                                                                      *
 -************************************************************************
+-
 -When we spot an equality arising from a functional dependency,
 -we now use that equality (a "wanted") to rewrite the work-item
 -constraint right away.  This avoids two dangers
+-
 - Danger 1: If we send the original constraint on down the pipeline
 -           it may react with an instance declaration, and in delicate
 -           situations (when a Given overlaps with an instance) that
 -           may produce new insoluble goals: see #4952
+-
 - Danger 2: If we don't rewrite the constraint, it may re-react
 -           with the same thing later, and produce the same equality
 -           again --> termination worries.
+-
 -To achieve this required some refactoring of GHC.Tc.Instance.FunDeps (nicer
 -now!).
+-
 -Note [FunDep and implicit parameter reactions]
 -~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 -Currently, our story of interacting two dictionaries (or a dictionary
 -and top-level instances) for functional dependencies (including implicit
 -parameters), is that we simply produce new Wanted equalities.  So for example
+-
 -        class D a b | a -> b where ...
 -    Inert:
 -        [G] d1 : D Int Bool
 -    WorkItem:
 -        [W] d2 : D Int alpha
+-
 -    We generate the extra work item
 -        [W] cv : alpha ~ Bool
 -    where 'cv' is currently unused.  However, this new item can perhaps be
 -    spontaneously solved to become given and react with d2,
 -    discharging it in favour of a new constraint d2' thus:
 -        [W] d2' : D Int Bool
 -        d2 := d2' |> D Int cv
 -    Now d2' can be discharged from d1
+-
 -We could be more aggressive and try to *immediately* solve the dictionary
 -using those extra equalities.
+-
 -If that were the case with the same inert set and work item we might discard
 -d2 directly:
+-
 -        [W] cv : alpha ~ Bool
 -        d2 := d1 |> D Int cv
+-
 -But in general it's a bit painful to figure out the necessary coercion,
 -so we just take the first approach. Here is a better example. Consider:
 -    class C a b c | a -> b
 -And:
 -     [G] d1 : C T Int Char
 -     [W] d2 : C T beta Int
 -In this case, it's *not even possible* to solve the wanted immediately.
 -So we should simply output the functional dependency and add this guy
 -[but NOT its superclasses] back in the worklist. Even worse:
 -     [G] d1 : C T Int beta
 -     [W] d2: C T beta Int
 -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, 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
 -       [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] in GHC.Tc.Solver.Equality.
 ---- 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 [Do fundeps last]
 -~~~~~~~~~~~~~~~~~~~~~~
 -Consider T4254b:
 -  class FD a b | a -> b where { op :: a -> b }
+-
 -  instance FD Int Bool
+-
 -  foo :: forall a b. (a~Int,FD a b) => a -> Bool
 -  foo = op
+-
 -(DFL1) Try local fundeps first.
 -  From the ambiguity check on the type signature we get
 -    [G] FD Int b
 -    [W] FD Int beta
 -  Interacting these gives beta:=b; then we start again and solve without
 -  trying fundeps between the new [W] FD Int b and the top-level instance.
 -  If we did, we'd generate [W] b ~ Bool, which fails.
+-
 -(DFL2) Try solving from top-level instances before fundeps
 -  From the definition `foo = op` we get
 -    [G] FD Int b
 -    [W] FD Int Bool
 -  We solve this from the top level instance before even trying fundeps.
 -  If we did try fundeps, we'd generate [W] b ~ Bool, which fails.
+-
+-
 -Note [Weird fundeps]
 -~~~~~~~~~~~~~~~~~~~~
 -Consider   class Het a b | a -> b where
 -              het :: m (f c) -> a -> m b
+-
 -           class GHet (a :: * -> *) (b :: * -> *) | a -> b
 -           instance            GHet (K a) (K [a])
 -           instance Het a b => GHet (K a) (K b)
+-
 -The two instances don't actually conflict on their fundeps,
 -although it's pretty strange.  So they are both accepted. Now
 -try   [W] GHet (K Int) (K Bool)
 -This triggers fundeps from both instance decls;
 -      [W] K Bool ~ K [a]
 -      [W] K Bool ~ K beta
 -And there's a risk of complaining about Bool ~ [a].  But in fact
 -the Wanted matches the second instance, so we never get as far
 -as the fundeps.
+-
 -#7875 is a case in point.
 --}
+-
 -doDictFunDepImprovement :: Cts -> TcS (Cts, Bool)
 --- (doDictFunDepImprovement inst_envs cts)
 ---   * Generate the fundeps from interacting the
 ---     top-level `inst_envs` with the constraints `cts`
 ---   * Do the unifications and return any unsolved constraints
 --- See Note [Fundeps with instances, and equality orientation]
 -doDictFunDepImprovement unsolved_wanteds
 -  = do { inerts <- getInertCans  -- The inert_dicts are all Givens
 -       ; inst_envs <- getInstEnvs
 -       ; (_, new_eqs, unifs) <- foldrM (do_one_dict inst_envs)
 -                                       (inert_dicts inerts, emptyBag, False)
 -                                       unsolved_wanteds
 -       ; return (new_eqs, unifs) }
+-
 -do_one_dict :: InstEnvs -> Ct
 -            -> (DictMap DictCt, Cts, Bool)
 -            -> TcS (DictMap DictCt, Cts, Bool)
 -do_one_dict inst_envs (CDictCan dict_ct) (local_dicts, new_eqs, unifs)
 -  = do { (new_eqs1, unifs1) <- do_one_top inst_envs dict_ct
 -       ; (local_dicts2, new_eqs2, unifs2) <- do_one_local local_dicts dict_ct
 -       ; return ( local_dicts2
 -                , new_eqs1 `unionBags` new_eqs2 `unionBags` new_eqs
 -                , unifs1 || unifs2 || unifs ) }
+-
 -do_one_dict _ _ acc  -- Non-DictCt constraints
 -  = return acc
+-
 -do_one_top :: InstEnvs -> DictCt -> TcS (Cts, Bool)
 -do_one_top inst_envs (DictCt { di_ev = ev, di_cls = cls, di_tys = xis })
 -  = unifyFunDepWanteds ev eqns
 -  where
 -    eqns :: [FunDepEqn (CtLoc, RewriterSet)]
 -    eqns = improveFromInstEnv inst_envs mk_ct_loc cls xis
+-
 -    dict_pred      = mkClassPred cls xis
 -    dict_loc       = ctEvLoc ev
 -    dict_origin    = ctLocOrigin dict_loc
 -    dict_rewriters = ctEvRewriters ev
+-
 -    mk_ct_loc :: ClsInst  -- The instance decl
 -              -> (CtLoc, RewriterSet)
 -    mk_ct_loc ispec
 -      = (dict_loc { ctl_origin = new_orig }, dict_rewriters)
 -      where
 -        inst_pred = mkClassPred cls (is_tys ispec)
 -        inst_loc  = getSrcSpan (is_dfun ispec)
 -        new_orig  = FunDepOrigin2 dict_pred dict_origin
 -                                  inst_pred inst_loc
+-
 -do_one_local :: DictMap DictCt -> DictCt -> TcS (DictMap DictCt, Cts, Bool)
 --- Using functional dependencies, interact the unsolved Wanteds
 --- against each other and the inert Givens, to produce new equalities
 -do_one_local locals dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev })
 -    -- locals contains all the Givens and earlier Wanteds
 -  = do { (new_eqs, unifs) <- foldrM do_interaction (emptyBag, False) $
 -                             findDictsByClass locals cls
 -       ; return (addDict dict_ct locals, new_eqs, unifs) }
 -  where
 -    wanted_pred = ctEvPred wanted_ev
 -    wanted_loc  = ctEvLoc  wanted_ev
+-
 -    do_interaction :: DictCt -> (Cts,Bool) -> TcS (Cts,Bool)
 -    do_interaction (DictCt { di_ev = all_ev }) (new_eqs, unifs) -- This can be Given or Wanted
 -      = do { traceTcS "doLocalFunDepImprovement" $
 -             vcat [ ppr wanted_ev
 -                  , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc)
 -                  , pprCtLoc all_loc, ppr (isGivenLoc all_loc)
 -                  , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ]
+-
 -           ; (new_eqs1, unifs1) <- unifyFunDepWanteds wanted_ev $
 -                                   improveFromAnother (deriv_loc, all_rewriters)
 -                                                      all_pred wanted_pred
 -           ; return (new_eqs1 `unionBags` new_eqs, unifs1 || unifs) }
 -      where
 -        all_pred  = ctEvPred all_ev
 -        all_loc   = ctEvLoc all_ev
 -        all_rewriters = ctEvRewriters all_ev
 -        deriv_loc = wanted_loc { ctl_depth  = deriv_depth
 -                               , ctl_origin = deriv_origin }
 -        deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth`
 -                      ctl_depth all_loc
 -        deriv_origin = FunDepOrigin1 wanted_pred
 -                                     (ctLocOrigin wanted_loc)
 -                                     (ctLocSpan wanted_loc)
 -                                     all_pred
 -                                     (ctLocOrigin all_loc)
 -                                     (ctLocSpan all_loc)
+-
  {- *********************************************************************
  *                                                                      *

compiler/GHC/Tc/Solver/Equality.hs

@@ -14,6 +14,7 @@ import GHC.Tc.Solver.Irred( solveIrred )
  import GHC.Tc.Solver.Dict( matchLocalInst, chooseInstance )
  import GHC.Tc.Solver.Rewrite
  import GHC.Tc.Solver.Monad
 +import GHC.Tc.Solver.FunDeps( unifyAndEmitFunDepWanteds )
  import GHC.Tc.Solver.InertSet
  import GHC.Tc.Solver.Types( findFunEqsByTyCon )
  import GHC.Tc.Types.Evidence
@@ -3108,13 +3109,17 @@ 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

compiler/GHC/Tc/Solver/FunDeps.hs

 +{-# LANGUAGE DuplicateRecordFields #-}
 +{-# LANGUAGE MultiWayIf #-}
++
 +-- | Solving Class constraints CDictCan
 +module GHC.Tc.Solver.FunDeps (
 +  unifyAndEmitFunDepWanteds,
 +  doDictFunDepImprovement,
 +  ImprovementResult, noImprovement
 +  ) where
++
 +import GHC.Prelude
++
 +import GHC.Tc.Instance.FunDeps
 +import GHC.Tc.Types.Evidence
 +import GHC.Tc.Types.Constraint
 +import GHC.Tc.Types.CtLoc
 +import GHC.Tc.Types.Origin
 +import GHC.Tc.Solver.InertSet
 +import GHC.Tc.Solver.Monad
 +import GHC.Tc.Solver.Types
 +import GHC.Tc.Utils.TcType
 +import GHC.Tc.Utils.Unify( UnifyEnv(..) )
 +import GHC.Tc.Utils.Monad    as TcM
++
 +import GHC.Core.Type
 +import GHC.Core.InstEnv     ( InstEnvs, ClsInst(..) )
 +import GHC.Core.Coercion.Axiom( TypeEqn )
++
 +import GHC.Types.Name
 +import GHC.Types.Var.Set
++
 +import GHC.Utils.Outputable
++
 +import GHC.Data.Bag
 +import GHC.Data.Pair
++
 +import qualified Data.Semigroup as S
++
 +import Control.Monad
++
 +{- *********************************************************************
 +*                                                                      *
 +*          Functional dependencies, instantiation of equations
 +*                                                                      *
 +************************************************************************
++
 +When we spot an equality arising from a functional dependency,
 +we now use that equality (a "wanted") to rewrite the work-item
 +constraint right away.  This avoids two dangers
++
 + Danger 1: If we send the original constraint on down the pipeline
 +           it may react with an instance declaration, and in delicate
 +           situations (when a Given overlaps with an instance) that
 +           may produce new insoluble goals: see #4952
++
 + Danger 2: If we don't rewrite the constraint, it may re-react
 +           with the same thing later, and produce the same equality
 +           again --> termination worries.
++
 +To achieve this required some refactoring of GHC.Tc.Instance.FunDeps (nicer
 +now!).
++
 +Note [FunDep and implicit parameter reactions]
 +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 +Currently, our story of interacting two dictionaries (or a dictionary
 +and top-level instances) for functional dependencies (including implicit
 +parameters), is that we simply produce new Wanted equalities.  So for example
++
 +        class D a b | a -> b where ...
 +    Inert:
 +        [G] d1 : D Int Bool
 +    WorkItem:
 +        [W] d2 : D Int alpha
++
 +    We generate the extra work item
 +        [W] cv : alpha ~ Bool
 +    where 'cv' is currently unused.  However, this new item can perhaps be
 +    spontaneously solved to become given and react with d2,
 +    discharging it in favour of a new constraint d2' thus:
 +        [W] d2' : D Int Bool
 +        d2 := d2' |> D Int cv
 +    Now d2' can be discharged from d1
++
 +We could be more aggressive and try to *immediately* solve the dictionary
 +using those extra equalities.
++
 +If that were the case with the same inert set and work item we might discard
 +d2 directly:
++
 +        [W] cv : alpha ~ Bool
 +        d2 := d1 |> D Int cv
++
 +But in general it's a bit painful to figure out the necessary coercion,
 +so we just take the first approach. Here is a better example. Consider:
 +    class C a b c | a -> b
 +And:
 +     [G] d1 : C T Int Char
 +     [W] d2 : C T beta Int
 +In this case, it's *not even possible* to solve the wanted immediately.
 +So we should simply output the functional dependency and add this guy
 +[but NOT its superclasses] back in the worklist. Even worse:
 +     [G] d1 : C T Int beta
 +     [W] d2: C T beta Int
 +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, 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
 +       [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] in GHC.Tc.Solver.Equality.
 +--- 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 [Do fundeps last]
 +~~~~~~~~~~~~~~~~~~~~~~
 +Consider T4254b:
 +  class FD a b | a -> b where { op :: a -> b }
++
 +  instance FD Int Bool
++
 +  foo :: forall a b. (a~Int,FD a b) => a -> Bool
 +  foo = op
++
 +(DFL1) Try local fundeps first.
 +  From the ambiguity check on the type signature we get
 +    [G] FD Int b
 +    [W] FD Int beta
 +  If we ineract that Wanted with /both/ the t0p-level instance, /and/ the
 +  local Given, we'll get
 +      beta ~ Int   and     beta ~ b
 +  respectively.  That would generate (b~Bool), which would fai.  I think
 +  it doesn't matter which of the two we pick, but historically we have
 +  picked teh local-fundeps firs.
++
 +(DFL2) Try solving from top-level instances before fundeps.
 +  From the definition `foo = op` we get
 +    [G] FD Int b
 +    [W] FD Int Bool
 +  We solve this from the top level instance before even trying fundeps.
 +  If we did try fundeps, we'd generate [W] b ~ Bool, which fails.
++
 +  (DFL2) is achieved by trying fundeps only on /unsolved/ Wanteds.
++
++
 +Note [Weird fundeps]
 +~~~~~~~~~~~~~~~~~~~~
 +Consider   class Het a b | a -> b where
 +              het :: m (f c) -> a -> m b
++
 +           class GHet (a :: * -> *) (b :: * -> *) | a -> b
 +           instance            GHet (K a) (K [a])
 +           instance Het a b => GHet (K a) (K b)
++
 +The two instances don't actually conflict on their fundeps,
 +although it's pretty strange.  So they are both accepted. Now
 +try   [W] GHet (K Int) (K Bool)
 +This triggers fundeps from both instance decls;
 +      [W] K Bool ~ K [a]
 +      [W] K Bool ~ K beta
 +And there's a risk of complaining about Bool ~ [a].  But in fact
 +the Wanted matches the second instance, so we never get as far
 +as the fundeps.
++
 +#7875 is a case in point.
 +-}
++
 +doDictFunDepImprovement :: Cts -> TcS ImprovementResult
 +-- (doDictFunDepImprovement inst_envs cts)
 +--   * Generate the fundeps from interacting the
 +--     top-level `inst_envs` with the constraints `cts`
 +--   * Do the unifications and return any unsolved constraints
 +-- See Note [Fundeps with instances, and equality orientation]
 +-- foldrM :: (Foldable t, Monad m) => (a -> b -> m b) -> b -> t a -> m b
 +doDictFunDepImprovement unsolved_wanteds
 +  = do { inerts    <- getInertCans  -- The inert_dicts are all Givens
 +       ; inst_envs <- getInstEnvs
 +       ; (_, imp_res) <- foldM (do_one_dict inst_envs)
 +                               (inert_dicts inerts, noopImprovement)
 +                               unsolved_wanteds
 +       ; return imp_res }
++
 +do_one_dict :: InstEnvs
 +            -> (DictMap DictCt, ImprovementResult)
 +            -> Ct
 +            -> TcS (DictMap DictCt, ImprovementResult)
 +-- The `local_dicts` accumulator starts life as just the Givens, but
 +--   as we encounter each Wanted we augment it. Result: each Wanted
 +--   is interacted with all the Givens, and all prededing Wanteds.
 +--   This is worst-case quadratic because we have to compare each
 +--   constraint with all the others, to find all the pairwise interactions
 +do_one_dict inst_envs (local_dicts, imp_res) (CDictCan dict_ct)
 +  = do { (local_dicts1, imp_res1) <- do_one_local local_dicts dict_ct
 +       ; if noImprovement imp_res1
 +         then do { imp_res2 <- do_one_top inst_envs dict_ct
 +                 ; return (local_dicts1, imp_res `plusImprovements` imp_res2) }
 +         else      return (local_dicts1, imp_res `plusImprovements` imp_res1) }
++
 +do_one_dict _ acc _  -- Non-DictCt constraints
 +  = return acc
++
 +do_one_top :: InstEnvs -> DictCt -> TcS ImprovementResult
 +do_one_top inst_envs (DictCt { di_ev = ev, di_cls = cls, di_tys = xis })
 +  = unifyFunDepWanteds ev eqns
 +  where
 +    eqns :: [FunDepEqn (CtLoc, RewriterSet)]
 +    eqns = improveFromInstEnv inst_envs mk_ct_loc cls xis
++
 +    dict_pred      = mkClassPred cls xis
 +    dict_loc       = ctEvLoc ev
 +    dict_origin    = ctLocOrigin dict_loc
 +    dict_rewriters = ctEvRewriters ev
++
 +    mk_ct_loc :: ClsInst  -- The instance decl
 +              -> (CtLoc, RewriterSet)
 +    mk_ct_loc ispec
 +      = (dict_loc { ctl_origin = new_orig }, dict_rewriters)
 +      where
 +        inst_pred = mkClassPred cls (is_tys ispec)
 +        inst_loc  = getSrcSpan (is_dfun ispec)
 +        new_orig  = FunDepOrigin2 dict_pred dict_origin
 +                                  inst_pred inst_loc
++
 +do_one_local :: DictMap DictCt -> DictCt -> TcS (DictMap DictCt, ImprovementResult)
 +-- Using functional dependencies, interact the unsolved Wanteds
 +-- against each other and the inert Givens, to produce new equalities
 +do_one_local locals dict_ct@(DictCt { di_cls = cls, di_ev = wanted_ev })
 +    -- locals contains all the Givens and earlier Wanteds
 +  = do { imp_res <- foldM do_interaction noopImprovement $
 +                    findDictsByClass locals cls
 +       ; return (addDict dict_ct locals, imp_res) }
 +  where
 +    wanted_pred = ctEvPred wanted_ev
 +    wanted_loc  = ctEvLoc  wanted_ev
++
 +    do_interaction :: (Cts,Bool) -> DictCt -> TcS (Cts,Bool)
 +    do_interaction (new_eqs, unifs) (DictCt { di_ev = all_ev }) -- This can be Given or Wanted
 +      = do { traceTcS "doLocalFunDepImprovement" $
 +             vcat [ ppr wanted_ev
 +                  , pprCtLoc wanted_loc, ppr (isGivenLoc wanted_loc)
 +                  , pprCtLoc all_loc, ppr (isGivenLoc all_loc)
 +                  , pprCtLoc deriv_loc, ppr (isGivenLoc deriv_loc) ]
++
 +           ; (new_eqs1, unifs1) <- unifyFunDepWanteds wanted_ev $
 +                                   improveFromAnother (deriv_loc, all_rewriters)
 +                                                      all_pred wanted_pred
 +           ; return (new_eqs1 `unionBags` new_eqs, unifs1 || unifs) }
 +      where
 +        all_pred  = ctEvPred all_ev
 +        all_loc   = ctEvLoc all_ev
 +        all_rewriters = ctEvRewriters all_ev
 +        deriv_loc = wanted_loc { ctl_depth  = deriv_depth
 +                               , ctl_origin = deriv_origin }
 +        deriv_depth = ctl_depth wanted_loc `maxSubGoalDepth`
 +                      ctl_depth all_loc
 +        deriv_origin = FunDepOrigin1 wanted_pred
 +                                     (ctLocOrigin wanted_loc)
 +                                     (ctLocSpan wanted_loc)
 +                                     all_pred
 +                                     (ctLocOrigin all_loc)
 +                                     (ctLocSpan all_loc)
++
++
 +{-
 +************************************************************************
 +*                                                                      *
 +              Emitting equalities arising from fundeps
 +*                                                                      *
 +************************************************************************
 +-}
++
 +type ImprovementResult = (Cts, Bool)
 +  -- The Cts are the new equality constraints
 +  -- The Bool is True if we unified any meta-ty-vars on when
 +  --  generating those new equality constraints
++
 +noopImprovement :: ImprovementResult
 +noopImprovement = (emptyBag, False)
++
 +noImprovement :: ImprovementResult -> Bool
 +noImprovement (cts,unifs) = not unifs && isEmptyBag cts
++
 +plusImprovements :: ImprovementResult -> ImprovementResult -> ImprovementResult
 +plusImprovements (cts1,unif1) (cts2,unif2)
 +  = (cts1 `unionBags` cts2, unif1 || unif2)
++
++
 +unifyAndEmitFunDepWanteds :: CtEvidence  -- The work item
 +                          -> [FunDepEqn (CtLoc, RewriterSet)]
 +                          -> TcS Bool   -- True <=> some unification happened
 +unifyAndEmitFunDepWanteds ev fd_eqns
 +  = do { (new_eqs, unifs)  <- unifyFunDepWanteds ev fd_eqns
++
 +       ;   -- Emit the deferred constraints
 +           -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
 +           --
 +           -- All the constraints in `cts` share the same rewriter set so,
 +           -- rather than looking at it one by one, we pass it to
 +           -- extendWorkListChildEqs; just a small optimisation.
 +       ; unless (isEmptyBag new_eqs) $
 +         updWorkListTcS (extendWorkListChildEqs ev new_eqs)
++
 +       ; return unifs }
++
 +unifyFunDepWanteds :: CtEvidence  -- The work item
 +                  -> [FunDepEqn (CtLoc, RewriterSet)]
 +                  -> TcS ImprovementResult
++
 +unifyFunDepWanteds _ [] = return noopImprovement -- common case noop
 +-- See Note [FunDep and implicit parameter reactions]
++
 +unifyFunDepWanteds ev fd_eqns
 +  = do { (fresh_tvs_s, cts, unified_tvs) <- wrapUnifierX ev Nominal do_fundeps
++
 +       -- Figure out if a "real" unification happened: See Note [unifyFunDeps]
 +       ; let unif_happened = any is_old_tv unified_tvs
 +             fresh_tvs     = mkVarSet (concat fresh_tvs_s)
 +             is_old_tv tv  = not (tv `elemVarSet` fresh_tvs)
++
 +       ; return (cts, unif_happened) }
 +  where
 +    do_fundeps :: UnifyEnv -> TcM [[TcTyVar]]
 +    do_fundeps env = mapM (do_one env) fd_eqns
++
 +    do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM [TcTyVar]
 +    do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
 +      = do { (fresh_tvs, eqs') <- instantiateFunDepEqn tvs (reverse eqs)
 +                     -- (reverse eqs): See Note [Reverse order of fundep equations]
 +           ; uPairsTcM env_one eqs'
 +           ; return fresh_tvs }
 +      where
 +        env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters
 +                       , u_loc       = loc }
++
 +instantiateFunDepEqn :: [TyVar] -> [TypeEqn] -> TcM ([TcTyVar], [TypeEqn])
 +instantiateFunDepEqn tvs eqs
 +  | null tvs
 +  = return ([], eqs)
 +  | otherwise
 +  = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs)
 +       ; (tvs', subst) <- instFlexiXTcM emptySubst tvs  -- Takes account of kind substitution
 +       ; return (tvs', map (subst_pair subst) eqs) }
 +  where
 +    subst_pair subst (Pair ty1 ty2)
 +       = Pair (substTyUnchecked subst' ty1) ty2
 +              -- ty2 does not mention fd_qtvs, so no need to subst it.
 +              -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
 +              --     Wrinkle (1)
 +       where
 +         subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
 +                  -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
 +                  -- of matching with the [W] constraint. So we add its free
 +                  -- vars to InScopeSet, to satisfy substTy's invariants, even
 +                  -- though ty1 will never (currently) be a poytype, so this
 +                  -- InScopeSet will never be looked at.
++

compiler/GHC/Tc/Solver/Monad.hs

@@ -105,10 +105,9 @@ module GHC.Tc.Solver.Monad (
      -- Unification
      wrapUnifierX, wrapUnifierTcS, unifyFunDeps, uPairsTcM, unifyForAllBody,
 -    unifyFunDepWanteds, unifyAndEmitFunDepWanteds,
      -- MetaTyVars
 -    newFlexiTcSTy, instFlexiX,
 +    newFlexiTcSTy, instFlexiX, instFlexiXTcM,
      cloneMetaTyVar,
      tcInstSkolTyVarsX,
@@ -129,8 +128,7 @@ module GHC.Tc.Solver.Monad (
      pprEq,
      -- Enforcing invariants for type equalities
 -    checkTypeEq,
 -    instantiateFunDepEqn
 +    checkTypeEq
  ) where
  import GHC.Prelude
@@ -2235,83 +2233,6 @@ solverDepthError loc ty
    where
      depth = ctLocDepth loc
 -{-
 -************************************************************************
 -*                                                                      *
 -              Emitting equalities arising from fundeps
 -*                                                                      *
 -************************************************************************
 --}
+-
 -unifyAndEmitFunDepWanteds :: CtEvidence  -- The work item
 -                          -> [FunDepEqn (CtLoc, RewriterSet)]
 -                          -> TcS Bool   -- True <=> some unification happened
 -unifyAndEmitFunDepWanteds ev fd_eqns
 -  = do { (new_eqs, unifs)  <- unifyFunDepWanteds ev fd_eqns
+-
 -       ;   -- Emit the deferred constraints
 -           -- See Note [Work-list ordering] in GHC.Tc.Solved.Equality
 -           --
 -           -- All the constraints in `cts` share the same rewriter set so,
 -           -- rather than looking at it one by one, we pass it to
 -           -- extendWorkListChildEqs; just a small optimisation.
 -       ; unless (isEmptyBag new_eqs) $
 -         updWorkListTcS (extendWorkListChildEqs ev new_eqs)
+-
 -       ; return unifs }
+-
 -unifyFunDepWanteds :: CtEvidence  -- The work item
 -                  -> [FunDepEqn (CtLoc, RewriterSet)]
 -                  -> TcS (Cts, Bool)   -- True <=> some unification happened
+-
 -unifyFunDepWanteds _ [] = return (emptyBag, False) -- common case noop
 --- See Note [FunDep and implicit parameter reactions]
+-
 -unifyFunDepWanteds ev fd_eqns
 -  = do { (fresh_tvs_s, cts, unified_tvs) <- wrapUnifierX ev Nominal do_fundeps
+-
 -       -- Figure out if a "real" unification happened: See Note [unifyFunDeps]
 -       ; let unif_happened = any is_old_tv unified_tvs
 -             fresh_tvs     = mkVarSet (concat fresh_tvs_s)
 -             is_old_tv tv  = not (tv `elemVarSet` fresh_tvs)
+-
 -       ; return (cts, unif_happened) }
 -  where
 -    do_fundeps :: UnifyEnv -> TcM [[TcTyVar]]
 -    do_fundeps env = mapM (do_one env) fd_eqns
+-
 -    do_one :: UnifyEnv -> FunDepEqn (CtLoc, RewriterSet) -> TcM [TcTyVar]
 -    do_one uenv (FDEqn { fd_qtvs = tvs, fd_eqs = eqs, fd_loc = (loc, rewriters) })
 -      = do { (fresh_tvs, eqs') <- instantiateFunDepEqn tvs (reverse eqs)
 -                     -- (reverse eqs): See Note [Reverse order of fundep equations]
 -           ; uPairsTcM env_one eqs'
 -           ; return fresh_tvs }
 -      where
 -        env_one = uenv { u_rewriters = u_rewriters uenv S.<> rewriters
 -                       , u_loc       = loc }
+-
 -instantiateFunDepEqn :: [TyVar] -> [TypeEqn] -> TcM ([TcTyVar], [TypeEqn])
 -instantiateFunDepEqn tvs eqs
 -  | null tvs
 -  = return ([], eqs)
 -  | otherwise
 -  = do { TcM.traceTc "emitFunDepWanteds 2" (ppr tvs $$ ppr eqs)
 -       ; (tvs', subst) <- instFlexiXTcM emptySubst tvs  -- Takes account of kind substitution
 -       ; return (tvs', map (subst_pair subst) eqs) }
 -  where
 -    subst_pair subst (Pair ty1 ty2)
 -       = Pair (substTyUnchecked subst' ty1) ty2
 -              -- ty2 does not mention fd_qtvs, so no need to subst it.
 -              -- See GHC.Tc.Instance.Fundeps Note [Improving against instances]
 -              --     Wrinkle (1)
 -       where
 -         subst' = extendSubstInScopeSet subst (tyCoVarsOfType ty1)
 -                  -- The free vars of ty1 aren't just fd_qtvs: ty1 is the result
 -                  -- of matching with the [W] constraint. So we add its free
 -                  -- vars to InScopeSet, to satisfy substTy's invariants, even
 -                  -- though ty1 will never (currently) be a poytype, so this
 -                  -- InScopeSet will never be looked at.
+-
  {-
  ************************************************************************
  *                                                                      *

compiler/GHC/Tc/Solver/Solve.hs

@@ -15,6 +15,7 @@ module GHC.Tc.Solver.Solve (
  import GHC.Prelude
  import GHC.Tc.Solver.Dict
 +import GHC.Tc.Solver.FunDeps( doDictFunDepImprovement )
  import GHC.Tc.Solver.Equality( solveEquality )
  import GHC.Tc.Solver.Irred( solveIrred )
  import GHC.Tc.Solver.Rewrite( rewrite, rewriteType )
@@ -119,13 +120,13 @@ simplify_loop n limit definitely_redo_implications
                              , int (lengthBag simples) <+> text "simples to solve" ])
         ; traceTcS "simplify_loop: wc =" (ppr wc)
 -       ; (unifs1, wc1) <- reportUnifications $  -- See Note [Superclass iteration]
 -                          solveSimpleWanteds simples
 +       ; (n_unifs, wc1) <- reportUnifications $  -- See Note [Superclass iteration]
 +                           solveSimpleWanteds simples
                  -- Any insoluble constraints are in 'simples' and so get rewritten
                  -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
         ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]
 -                   && unifs1 == 0                    -- for this conditional
 +                   && n_unifs == 0                   -- for this conditional
                     && isEmptyBag (wc_impl wc1)
                  then return (wc { wc_simple = wc_simple wc1 })  -- Short cut
                  else do { implics2 <- solveNestedImplications $
@@ -207,10 +208,19 @@ maybe_simplify_again n limit unif_happened wc@(WC { wc_simple = simples })
      try_fundeps :: TcS (Maybe NextAction)
      try_fundeps
 -      = do { (new_eqs, unifs) <- doDictFunDepImprovement simples
 -           ; if null new_eqs && not unifs
 +      = do { (new_eqs, unifs1) <- doDictFunDepImprovement simples
 +           ; if null new_eqs && not unifs1
               then return Nothing
 -             else return (Just (NA_TryAgain (wc `addSimples` new_eqs) unifs)) }
 +             else
 +        -- We solve new_eqs immediately, hoping to get some unifications
 +        -- If instead we just added them to `wc` we'll iterate and (in case when
 +        -- that doesn't solve it) we'll add the same constraint again... loop!
 +        do { traceTcS "try_fundeps" (ppr unifs1 $$ ppr new_eqs)
 +           ; (n_unifs2, _wc) <- reportUnifications $
 +                                solveSimpleWanteds new_eqs
 +           ; if (unifs1 || n_unifs2 > 0)
 +             then return (Just (NA_TryAgain wc True))
 +             else return Nothing } }
  {- Note [Superclass iteration]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

compiler/ghc.cabal.in

@@ -854,6 +854,7 @@ Library
          GHC.Tc.Solver.Irred
          GHC.Tc.Solver.Equality
          GHC.Tc.Solver.Dict
 +        GHC.Tc.Solver.FunDeps
          GHC.Tc.Solver.Monad
          GHC.Tc.Solver.Types
          GHC.Tc.TyCl