Rip GHC.Tc.Solver.Monad asunder (only)wip/break-up-tcs-monad

This creates new modules GHC.Tc.Solver.InertSet and
GHC.Tc.Solver.Types. The Monad module is still pretty
big, but this is an improvement. Moreover, it means
that GHC.HsToCore.Pmc.Solver.Types no longer depends
on the constraint solver (it now depends on GHC.Tc.Solver.InertSet),
making the error-messages work easier.

This patch thus contributes to #18516.

14 files changed, 2031 insertions, 1926 deletions

diff --git a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
index be977476df..9cec967592 100644
--- a/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
+++ b/compiler/GHC/HsToCore/Pmc/Solver/Types.hs
@@ -56,7 +56,7 @@ import GHC.Core.Utils (exprType)
 import GHC.Builtin.Names
 import GHC.Builtin.Types
 import GHC.Builtin.Types.Prim
-import GHC.Tc.Solver.Monad (InertSet, emptyInert)
+import GHC.Tc.Solver.InertSet (InertSet, emptyInert)
 import GHC.Tc.Utils.TcType (isStringTy)
 import GHC.Types.CompleteMatch (CompleteMatch(..))
 import GHC.Types.SourceText (SourceText(..), mkFractionalLit, FractionalLit
diff --git a/compiler/GHC/Tc/Gen/Pat.hs b/compiler/GHC/Tc/Gen/Pat.hs
index b401b4db60..32f8b15f4b 100644
--- a/compiler/GHC/Tc/Gen/Pat.hs
+++ b/compiler/GHC/Tc/Gen/Pat.hs
@@ -1054,7 +1054,7 @@ constraints will kick in: that logic only fires on constraints
 whose Origin is (OccurrenceOf f).
 
 See also Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-and Note [Solving CallStack constraints] in GHC.Tc.Solver.Monad
+and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
 -}
 ----------------------------
 -- | Convenient wrapper for calling a matchExpectedXXX function
diff --git a/compiler/GHC/Tc/Instance/Class.hs b/compiler/GHC/Tc/Instance/Class.hs
index af13a31272..f80d3eaf93 100644
--- a/compiler/GHC/Tc/Instance/Class.hs
+++ b/compiler/GHC/Tc/Instance/Class.hs
@@ -99,7 +99,7 @@ data ClsInstResult
 data InstanceWhat
   = BuiltinInstance
   | BuiltinEqInstance   -- A built-in "equality instance"; see the
-                        -- GHC.Tc.Solver.Monad Note [Solved dictionaries]
+                        -- GHC.Tc.Solver.InertSet Note [Solved dictionaries]
   | LocalInstance
   | TopLevInstance { iw_dfun_id   :: DFunId
                    , iw_safe_over :: SafeOverlapping }
@@ -124,7 +124,7 @@ safeOverlap (TopLevInstance { iw_safe_over = so }) = so
 safeOverlap _                                      = True
 
 instanceReturnsDictCon :: InstanceWhat -> Bool
--- See Note [Solved dictionaries] in GHC.Tc.Solver.Monad
+-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
 instanceReturnsDictCon (TopLevInstance {}) = True
 instanceReturnsDictCon BuiltinInstance     = True
 instanceReturnsDictCon BuiltinEqInstance   = False
diff --git a/compiler/GHC/Tc/Solver.hs b/compiler/GHC/Tc/Solver.hs
index e6212ef648..b37cc33451 100644
--- a/compiler/GHC/Tc/Solver.hs
+++ b/compiler/GHC/Tc/Solver.hs
@@ -46,6 +46,7 @@ import GHC.Tc.Solver.Rewrite     ( rewriteType )
 import GHC.Tc.Utils.Unify        ( buildTvImplication )
 import GHC.Tc.Utils.TcMType as TcM
 import GHC.Tc.Utils.Monad   as TcM
+import GHC.Tc.Solver.InertSet
 import GHC.Tc.Solver.Monad  as TcS
 import GHC.Tc.Types.Constraint
 import GHC.Core.Predicate
@@ -1770,7 +1771,7 @@ simplify_loop n limit definitely_redo_implications
        ; (unifs1, 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.Monad
+                -- See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet
 
        ; wc2 <- if not definitely_redo_implications  -- See Note [Superclass iteration]
                    && unifs1 == 0                    -- for this conditional
diff --git a/compiler/GHC/Tc/Solver/Canonical.hs b/compiler/GHC/Tc/Solver/Canonical.hs
index f0b4e9deb2..11606401c8 100644
--- a/compiler/GHC/Tc/Solver/Canonical.hs
+++ b/compiler/GHC/Tc/Solver/Canonical.hs
@@ -20,6 +20,7 @@ import GHC.Tc.Utils.TcType
 import GHC.Core.Type
 import GHC.Tc.Solver.Rewrite
 import GHC.Tc.Solver.Monad
+import GHC.Tc.Solver.InertSet
 import GHC.Tc.Types.Evidence
 import GHC.Tc.Types.EvTerm
 import GHC.Core.Class
@@ -159,7 +160,7 @@ canClassNC ev cls tys
   -- call, we need to push the current call-site onto the stack instead
   -- of solving it directly from a given.
   -- See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-  -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Monad
+  -- and Note [Solving CallStack constraints] in GHC.Tc.Solver.Types
   = do { -- First we emit a new constraint that will capture the
          -- given CallStack.
        ; let new_loc = setCtLocOrigin loc (IPOccOrigin (HsIPName ip_name))
@@ -1973,7 +1974,7 @@ When an equality fails, we still want to rewrite the equality
 all the way down, so that it accurately reflects
  (a) the mutable reference substitution in force at start of solving
  (b) any ty-binds in force at this point in solving
-See Note [Rewrite insolubles] in GHC.Tc.Solver.Monad.
+See Note [Rewrite insolubles] in GHC.Tc.Solver.InertSet.
 And if we don't do this there is a bad danger that
 GHC.Tc.Solver.applyTyVarDefaulting will find a variable
 that has in fact been substituted.
diff --git a/compiler/GHC/Tc/Solver/InertSet.hs b/compiler/GHC/Tc/Solver/InertSet.hs
new file mode 100644
index 0000000000..4ad07a58d4
--- /dev/null
+++ b/compiler/GHC/Tc/Solver/InertSet.hs
@@ -0,0 +1,1633 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE TypeApplications #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
+
+module GHC.Tc.Solver.InertSet (
+    -- * The work list
+    WorkList(..), isEmptyWorkList, emptyWorkList,
+    extendWorkListNonEq, extendWorkListCt,
+    extendWorkListCts, extendWorkListEq, extendWorkListDeriveds,
+    appendWorkList, extendWorkListImplic,
+    workListSize,
+    selectWorkItem,
+
+    -- * The inert set
+    InertSet(..),
+    InertCans(..),
+    InertEqs,
+    emptyInert,
+    addInertItem,
+
+    matchableGivens,
+    mightEqualLater,
+    prohibitedSuperClassSolve,
+
+    -- * Inert equalities
+    foldTyEqs, delEq, findEq,
+
+    -- * Kick-out
+    kickOutRewritableLHS
+
+  ) where
+
+import GHC.Prelude
+
+import GHC.Tc.Solver.Types
+
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Evidence
+import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcType
+import GHC.Types.Var
+import GHC.Types.Var.Env
+
+import GHC.Core.Predicate
+import GHC.Core.TyCo.FVs
+import qualified GHC.Core.TyCo.Rep as Rep
+import GHC.Core.TyCon
+import GHC.Core.Unify
+
+import GHC.Data.Bag
+import GHC.Utils.Misc       ( chkAppend, partitionWith )
+import GHC.Utils.Outputable
+import GHC.Utils.Panic
+
+import Data.List          ( partition )
+import Data.List.NonEmpty ( NonEmpty(..) )
+
+{-
+************************************************************************
+*                                                                      *
+*                            Worklists                                *
+*  Canonical and non-canonical constraints that the simplifier has to  *
+*  work on. Including their simplification depths.                     *
+*                                                                      *
+*                                                                      *
+************************************************************************
+
+Note [WorkList priorities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A WorkList contains canonical and non-canonical items (of all flavours).
+Notice that each Ct now has a simplification depth. We may
+consider using this depth for prioritization as well in the future.
+
+As a simple form of priority queue, our worklist separates out
+
+* equalities (wl_eqs); see Note [Prioritise equalities]
+* all the rest (wl_rest)
+
+Note [Prioritise equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+It's very important to process equalities /first/:
+
+* (Efficiency)  The general reason to do so is that if we process a
+  class constraint first, we may end up putting it into the inert set
+  and then kicking it out later.  That's extra work compared to just
+  doing the equality first.
+
+* (Avoiding fundep iteration) As #14723 showed, it's possible to
+  get non-termination if we
+      - Emit the Derived fundep equalities for a class constraint,
+        generating some fresh unification variables.
+      - That leads to some unification
+      - Which kicks out the class constraint
+      - Which isn't solved (because there are still some more Derived
+        equalities in the work-list), but generates yet more fundeps
+  Solution: prioritise derived equalities over class constraints
+
+* (Class equalities) We need to prioritise equalities even if they
+  are hidden inside a class constraint;
+  see Note [Prioritise class equalities]
+
+* (Kick-out) We want to apply this priority scheme to kicked-out
+  constraints too (see the call to extendWorkListCt in kick_out_rewritable
+  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
+  homo-kinded when kicked out, and hence we want to prioritise it.
+
+* (Derived equalities) Originally we tried to postpone processing
+  Derived equalities, in the hope that we might never need to deal
+  with them at all; but in fact we must process Derived equalities
+  eagerly, partly for the (Efficiency) reason, and more importantly
+  for (Avoiding fundep iteration).
+
+Note [Prioritise class equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We prioritise equalities in the solver (see selectWorkItem). But class
+constraints like (a ~ b) and (a ~~ b) are actually equalities too;
+see Note [The equality types story] in GHC.Builtin.Types.Prim.
+
+Failing to prioritise these is inefficient (more kick-outs etc).
+But, worse, it can prevent us spotting a "recursive knot" among
+Wanted constraints.  See comment:10 of #12734 for a worked-out
+example.
+
+So we arrange to put these particular class constraints in the wl_eqs.
+
+  NB: since we do not currently apply the substitution to the
+  inert_solved_dicts, the knot-tying still seems a bit fragile.
+  But this makes it better.
+
+Note [Residual implications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The wl_implics in the WorkList are the residual implication
+constraints that are generated while solving or canonicalising the
+current worklist.  Specifically, when canonicalising
+   (forall a. t1 ~ forall a. t2)
+from which we get the implication
+   (forall a. t1 ~ t2)
+See GHC.Tc.Solver.Monad.deferTcSForAllEq
+
+-}
+
+-- See Note [WorkList priorities]
+data WorkList
+  = WL { wl_eqs     :: [Ct]  -- CEqCan, CDictCan, CIrredCan
+                             -- Given, Wanted, and Derived
+                       -- Contains both equality constraints and their
+                       -- class-level variants (a~b) and (a~~b);
+                       -- See Note [Prioritise equalities]
+                       -- See Note [Prioritise class equalities]
+
+       , wl_rest    :: [Ct]
+
+       , wl_implics :: Bag Implication  -- See Note [Residual implications]
+    }
+
+appendWorkList :: WorkList -> WorkList -> WorkList
+appendWorkList
+    (WL { wl_eqs = eqs1, wl_rest = rest1
+        , wl_implics = implics1 })
+    (WL { wl_eqs = eqs2, wl_rest = rest2
+        , wl_implics = implics2 })
+   = WL { wl_eqs     = eqs1     ++ eqs2
+        , wl_rest    = rest1    ++ rest2
+        , wl_implics = implics1 `unionBags`   implics2 }
+
+workListSize :: WorkList -> Int
+workListSize (WL { wl_eqs = eqs, wl_rest = rest })
+  = length eqs + length rest
+
+extendWorkListEq :: Ct -> WorkList -> WorkList
+extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
+
+extendWorkListNonEq :: Ct -> WorkList -> WorkList
+-- Extension by non equality
+extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
+
+extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
+extendWorkListDeriveds evs wl
+  = extendWorkListCts (map mkNonCanonical evs) wl
+
+extendWorkListImplic :: Implication -> WorkList -> WorkList
+extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
+
+extendWorkListCt :: Ct -> WorkList -> WorkList
+-- Agnostic
+extendWorkListCt ct wl
+ = case classifyPredType (ctPred ct) of
+     EqPred {}
+       -> extendWorkListEq ct wl
+
+     ClassPred cls _  -- See Note [Prioritise class equalities]
+       |  isEqPredClass cls
+       -> extendWorkListEq ct wl
+
+     _ -> extendWorkListNonEq ct wl
+
+extendWorkListCts :: [Ct] -> WorkList -> WorkList
+-- Agnostic
+extendWorkListCts cts wl = foldr extendWorkListCt wl cts
+
+isEmptyWorkList :: WorkList -> Bool
+isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
+  = null eqs && null rest && isEmptyBag implics
+
+emptyWorkList :: WorkList
+emptyWorkList = WL { wl_eqs  = [], wl_rest = [], wl_implics = emptyBag }
+
+selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
+-- See Note [Prioritise equalities]
+selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest })
+  | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
+  | ct:cts <- rest = Just (ct, wl { wl_rest   = cts })
+  | otherwise      = Nothing
+
+-- Pretty printing
+instance Outputable WorkList where
+  ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
+   = text "WL" <+> (braces $
+     vcat [ ppUnless (null eqs) $
+            text "Eqs =" <+> vcat (map ppr eqs)
+          , ppUnless (null rest) $
+            text "Non-eqs =" <+> vcat (map ppr rest)
+          , ppUnless (isEmptyBag implics) $
+            ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
+                       (text "(Implics omitted)")
+          ])
+
+{- *********************************************************************
+*                                                                      *
+                InertSet: the inert set
+*                                                                      *
+*                                                                      *
+********************************************************************* -}
+
+data InertSet
+  = IS { inert_cans :: InertCans
+              -- Canonical Given, Wanted, Derived
+              -- Sometimes called "the inert set"
+
+       , inert_cycle_breakers :: [(TcTyVar, TcType)]
+              -- a list of CycleBreakerTv / original family applications
+              -- used to undo the cycle-breaking needed to handle
+              -- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
+
+       , inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
+              -- Just a hash-cons cache for use when reducing family applications
+              -- only
+              --
+              -- If    F tys :-> (co, rhs, flav),
+              -- then  co :: rhs ~N F tys
+              -- all evidence is from instances or Givens; no coercion holes here
+              -- (We have no way of "kicking out" from the cache, so putting
+              --  wanteds here means we can end up solving a Wanted with itself. Bad)
+
+       , inert_solved_dicts   :: DictMap CtEvidence
+              -- All Wanteds, of form ev :: C t1 .. tn
+              -- See Note [Solved dictionaries]
+              -- and Note [Do not add superclasses of solved dictionaries]
+       }
+
+instance Outputable InertSet where
+  ppr (IS { inert_cans = ics
+          , inert_solved_dicts = solved_dicts })
+      = vcat [ ppr ics
+             , ppUnless (null dicts) $
+               text "Solved dicts =" <+> vcat (map ppr dicts) ]
+         where
+           dicts = bagToList (dictsToBag solved_dicts)
+
+emptyInertCans :: InertCans
+emptyInertCans
+  = IC { inert_eqs          = emptyDVarEnv
+       , inert_given_eq_lvl = topTcLevel
+       , inert_given_eqs    = False
+       , inert_dicts        = emptyDictMap
+       , inert_safehask     = emptyDictMap
+       , inert_funeqs       = emptyFunEqs
+       , inert_insts        = []
+       , inert_irreds       = emptyCts }
+
+emptyInert :: InertSet
+emptyInert
+  = IS { inert_cans           = emptyInertCans
+       , inert_cycle_breakers = []
+       , inert_famapp_cache   = emptyFunEqs
+       , inert_solved_dicts   = emptyDictMap }
+
+
+{- Note [Solved dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+When we apply a top-level instance declaration, we add the "solved"
+dictionary to the inert_solved_dicts.  In general, we use it to avoid
+creating a new EvVar when we have a new goal that we have solved in
+the past.
+
+But in particular, we can use it to create *recursive* dictionaries.
+The simplest, degenerate case is
+    instance C [a] => C [a] where ...
+If we have
+    [W] d1 :: C [x]
+then we can apply the instance to get
+    d1 = $dfCList d
+    [W] d2 :: C [x]
+Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
+    d1 = $dfCList d
+    d2 = d1
+
+See Note [Example of recursive dictionaries]
+
+VERY IMPORTANT INVARIANT:
+
+ (Solved Dictionary Invariant)
+    Every member of the inert_solved_dicts is the result
+    of applying an instance declaration that "takes a step"
+
+    An instance "takes a step" if it has the form
+        dfunDList d1 d2 = MkD (...) (...) (...)
+    That is, the dfun is lazy in its arguments, and guarantees to
+    immediately return a dictionary constructor.  NB: all dictionary
+    data constructors are lazy in their arguments.
+
+    This property is crucial to ensure that all dictionaries are
+    non-bottom, which in turn ensures that the whole "recursive
+    dictionary" idea works at all, even if we get something like
+        rec { d = dfunDList d dx }
+    See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
+
+ Reason:
+   - All instances, except two exceptions listed below, "take a step"
+     in the above sense
+
+   - Exception 1: local quantified constraints have no such guarantee;
+     indeed, adding a "solved dictionary" when appling a quantified
+     constraint led to the ability to define unsafeCoerce
+     in #17267.
+
+   - Exception 2: the magic built-in instance for (~) has no
+     such guarantee.  It behaves as if we had
+         class    (a ~# b) => (a ~ b) where {}
+         instance (a ~# b) => (a ~ b) where {}
+     The "dfun" for the instance is strict in the coercion.
+     Anyway there's no point in recording a "solved dict" for
+     (t1 ~ t2); it's not going to allow a recursive dictionary
+     to be constructed.  Ditto (~~) and Coercible.
+
+THEREFORE we only add a "solved dictionary"
+  - when applying an instance declaration
+  - subject to Exceptions 1 and 2 above
+
+In implementation terms
+  - GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
+    conditional on the kind of instance
+
+  - It is only called when applying an instance decl,
+    in GHC.Tc.Solver.Interact.doTopReactDict
+
+  - ClsInst.InstanceWhat says what kind of instance was
+    used to solve the constraint.  In particular
+      * LocalInstance identifies quantified constraints
+      * BuiltinEqInstance identifies the strange built-in
+        instances for equality.
+
+  - ClsInst.instanceReturnsDictCon says which kind of
+    instance guarantees to return a dictionary constructor
+
+Other notes about solved dictionaries
+
+* See also Note [Do not add superclasses of solved dictionaries]
+
+* The inert_solved_dicts field is not rewritten by equalities,
+  so it may get out of date.
+
+* The inert_solved_dicts are all Wanteds, never givens
+
+* We only cache dictionaries from top-level instances, not from
+  local quantified constraints.  Reason: if we cached the latter
+  we'd need to purge the cache when bringing new quantified
+  constraints into scope, because quantified constraints "shadow"
+  top-level instances.
+
+Note [Do not add superclasses of solved dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Every member of inert_solved_dicts is the result of applying a
+dictionary function, NOT of applying superclass selection to anything.
+Consider
+
+        class Ord a => C a where
+        instance Ord [a] => C [a] where ...
+
+Suppose we are trying to solve
+  [G] d1 : Ord a
+  [W] d2 : C [a]
+
+Then we'll use the instance decl to give
+
+  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
+  [W] d3 : Ord [a]
+
+We must not add d4 : Ord [a] to the 'solved' set (by taking the
+superclass of d2), otherwise we'll use it to solve d3, without ever
+using d1, which would be a catastrophe.
+
+Solution: when extending the solved dictionaries, do not add superclasses.
+That's why each element of the inert_solved_dicts is the result of applying
+a dictionary function.
+
+Note [Example of recursive dictionaries]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+--- Example 1
+
+    data D r = ZeroD | SuccD (r (D r));
+
+    instance (Eq (r (D r))) => Eq (D r) where
+        ZeroD     == ZeroD     = True
+        (SuccD a) == (SuccD b) = a == b
+        _         == _         = False;
+
+    equalDC :: D [] -> D [] -> Bool;
+    equalDC = (==);
+
+We need to prove (Eq (D [])). Here's how we go:
+
+   [W] d1 : Eq (D [])
+By instance decl of Eq (D r):
+   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
+By instance decl of Eq [a]:
+   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
+                                   d1 = dfEqD d2
+Now this wanted can interact with our "solved" d1 to get:
+    d3 = d1
+
+-- Example 2:
+This code arises in the context of "Scrap Your Boilerplate with Class"
+
+    class Sat a
+    class Data ctx a
+    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
+    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
+
+    class Data Maybe a => Foo a
+
+    instance Foo t => Sat (Maybe t)                             -- dfunSat
+
+    instance Data Maybe a => Foo a                              -- dfunFoo1
+    instance Foo a        => Foo [a]                            -- dfunFoo2
+    instance                 Foo [Char]                         -- dfunFoo3
+
+Consider generating the superclasses of the instance declaration
+         instance Foo a => Foo [a]
+
+So our problem is this
+    [G] d0 : Foo t
+    [W] d1 : Data Maybe [t]   -- Desired superclass
+
+We may add the given in the inert set, along with its superclasses
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  WorkList
+    [W] d1 : Data Maybe [t]
+
+Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+  WorkList:
+    [W] d2 : Sat (Maybe [t])
+    [W] d3 : Data Maybe t
+
+Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
+  Inert:
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList:
+    [W] d3 : Data Maybe t
+    [W] d4 : Foo [t]
+
+Now, we can just solve d3 from d01; d3 := d01
+  Inert
+    [G] d0 : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+  WorkList
+    [W] d4 : Foo [t]
+
+Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
+  Inert
+    [G] d0  : Foo t
+    [G] d01 : Data Maybe t   -- Superclass of d0
+  Solved:
+        d1 : Data Maybe [t]
+        d2 : Sat (Maybe [t])
+        d4 : Foo [t]
+  WorkList:
+    [W] d5 : Foo t
+
+Now, d5 can be solved! d5 := d0
+
+Result
+   d1 := dfunData2 d2 d3
+   d2 := dfunSat d4
+   d3 := d01
+   d4 := dfunFoo2 d5
+   d5 := d0
+-}
+
+{- *********************************************************************
+*                                                                      *
+                InertCans: the canonical inerts
+*                                                                      *
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Tracking Given equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
+Note [Unification preconditions], we can't unify
+   alpha[2] ~ Int
+under a level-4 implication if there are any Given equalities
+bound by the implications at level 3 of 4.  To that end, the
+InertCans tracks
+
+  inert_given_eq_lvl :: TcLevel
+     -- The TcLevel of the innermost implication that has a Given
+     -- equality of the sort that make a unification variable untouchable
+     -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
+
+We update inert_given_eq_lvl whenever we add a Given to the
+inert set, in updateGivenEqs.
+
+Then a unification variable alpha[n] is untouchable iff
+    n < inert_given_eq_lvl
+that is, if the unification variable was born outside an
+enclosing Given equality.
+
+Exactly which constraints should trigger (UNTOUCHABLE), and hence
+should update inert_given_eq_lvl?
+
+* We do /not/ need to worry about let-bound skolems, such ast
+     forall[2] a. a ~ [b] => blah
+  See Note [Let-bound skolems]
+
+* Consider an implication
+      forall[2]. beta[1] => alpha[1] ~ Int
+  where beta is a unification variable that has already been unified
+  to () in an outer scope.  Then alpha[1] is perfectly touchable and
+  we can unify alpha := Int. So when deciding whether the givens contain
+  an equality, we should canonicalise first, rather than just looking at
+  the /original/ givens (#8644).
+
+ * However, we must take account of *potential* equalities. Consider the
+   same example again, but this time we have /not/ yet unified beta:
+      forall[2] beta[1] => ...blah...
+
+   Because beta might turn into an equality, updateGivenEqs conservatively
+   treats it as a potential equality, and updates inert_give_eq_lvl
+
+ * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?
+
+   That Given cannot affect the Wanted, because the Given is entirely
+   *local*: it mentions only skolems bound in the very same
+   implication. Such equalities need not make alpha untouchable. (Test
+   case typecheck/should_compile/LocalGivenEqs has a real-life
+   motivating example, with some detailed commentary.)
+   Hence the 'mentionsOuterVar' test in updateGivenEqs.
+
+   However, solely to support better error messages
+   (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
+   these "local" equalities in the boolean inert_given_eqs field.
+   This field is used only to set the ic_given_eqs field to LocalGivenEqs;
+   see the function getHasGivenEqs.
+
+   Here is a simpler case that triggers this behaviour:
+
+     data T where
+       MkT :: F a ~ G b => a -> b -> T
+
+     f (MkT _ _) = True
+
+   Because of this behaviour around local equality givens, we can infer the
+   type of f. This is typecheck/should_compile/LocalGivenEqs2.
+
+ * We need not look at the equality relation involved (nominal vs
+   representational), because representational equalities can still
+   imply nominal ones. For example, if (G a ~R G b) and G's argument's
+   role is nominal, then we can deduce a ~N b.
+
+Note [Let-bound skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+If   * the inert set contains a canonical Given CEqCan (a ~ ty)
+and  * 'a' is a skolem bound in this very implication,
+
+then:
+a) The Given is pretty much a let-binding, like
+      f :: (a ~ b->c) => a -> a
+   Here the equality constraint is like saying
+      let a = b->c in ...
+   It is not adding any new, local equality  information,
+   and hence can be ignored by has_given_eqs
+
+b) 'a' will have been completely substituted out in the inert set,
+   so we can safely discard it.
+
+For an example, see #9211.
+
+See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
+that the right variable is on the left of the equality when both are
+tyvars.
+
+You might wonder whether the skolem really needs to be bound "in the
+very same implication" as the equuality constraint.
+Consider this (c.f. #15009):
+
+  data S a where
+    MkS :: (a ~ Int) => S a
+
+  g :: forall a. S a -> a -> blah
+  g x y = let h = \z. ( z :: Int
+                      , case x of
+                           MkS -> [y,z])
+          in ...
+
+From the type signature for `g`, we get `y::a` .  Then when we
+encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
+body of the lambda we'll get
+
+  [W] alpha[1] ~ Int                             -- From z::Int
+  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]
+
+Now, unify alpha := a.  Now we are stuck with an unsolved alpha~Int!
+So we must treat alpha as untouchable under the forall[2] implication.
+
+Note [Detailed InertCans Invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+The InertCans represents a collection of constraints with the following properties:
+
+  * All canonical
+
+  * No two dictionaries with the same head
+  * No two CIrreds with the same type
+
+  * Family equations inert wrt top-level family axioms
+
+  * Dictionaries have no matching top-level instance
+
+  * Given family or dictionary constraints don't mention touchable
+    unification variables
+
+  * Non-CEqCan constraints are fully rewritten with respect
+    to the CEqCan equalities (modulo eqCanRewrite of course;
+    eg a wanted cannot rewrite a given)
+
+  * CEqCan equalities: see Note [inert_eqs: the inert equalities]
+    Also see documentation in Constraint.Ct for a list of invariants
+
+Note [inert_eqs: the inert equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Definition [Can-rewrite relation]
+A "can-rewrite" relation between flavours, written f1 >= f2, is a
+binary relation with the following properties
+
+  (R1) >= is transitive
+  (R2) If f1 >= f, and f2 >= f,
+       then either f1 >= f2 or f2 >= f1
+  (See Note [Why R2?].)
+
+Lemma (L0). If f1 >= f then f1 >= f1
+Proof.      By property (R2), with f1=f2
+
+Definition [Generalised substitution]
+A "generalised substitution" S is a set of triples (lhs -f-> t), where
+  lhs is a type variable or an exactly-saturated type family application
+    (that is, lhs is a CanEqLHS)
+  t is a type
+  f is a flavour
+such that
+  (WF1) if (lhs1 -f1-> t1) in S
+           (lhs2 -f2-> t2) in S
+        then (f1 >= f2) implies that lhs1 does not appear within lhs2
+  (WF2) if (lhs -f-> t) is in S, then t /= lhs
+
+Definition [Applying a generalised substitution]
+If S is a generalised substitution
+   S(f,t0) = t,  if (t0 -fs-> t) in S, and fs >= f
+           = apply S to components of t0, otherwise
+See also Note [Flavours with roles].
+
+Theorem: S(f,t0) is well defined as a function.
+Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S,
+               and  f1 >= f and f2 >= f
+       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
+
+Notation: repeated application.
+  S^0(f,t)     = t
+  S^(n+1)(f,t) = S(f, S^n(t))
+
+Definition: terminating generalised substitution
+A generalised substitution S is *terminating* iff
+
+  (IG1) there is an n such that
+        for every f,t, S^n(f,t) = S^(n+1)(f,t)
+
+By (IG1) we define S*(f,t) to be the result of exahaustively
+applying S(f,_) to t.
+
+-----------------------------------------------------------------------------
+Our main invariant:
+   the CEqCans in inert_eqs should be a terminating generalised substitution
+-----------------------------------------------------------------------------
+
+Note that termination is not the same as idempotence.  To apply S to a
+type, you may have to apply it recursively.  But termination does
+guarantee that this recursive use will terminate.
+
+Note [Why R2?]
+~~~~~~~~~~~~~~
+R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >=
+f1. If we do not have R2, we will easily fall into a loop.
+
+To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our
+inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And
+yet, we have a hard time noticing an occurs-check problem when building S, as
+the two equalities cannot rewrite one another.
+
+R2 actually restricts our ability to accept user-written programs. See
+Note [Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example.
+
+Note [Rewritable]
+~~~~~~~~~~~~~~~~~
+This Note defines what it means for a type variable or type family application
+(that is, a CanEqLHS) to be rewritable in a type. This definition is used
+by the anyRewritableXXX family of functions and is meant to model the actual
+behaviour in GHC.Tc.Solver.Rewrite.
+
+Ignoring roles (for now): A CanEqLHS lhs is *rewritable* in a type t if the
+lhs tree appears as a subtree within t without traversing any of the following
+components of t:
+  * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
+  * kinds of variable occurrences
+The check for rewritability *does* look in kinds of the bound variable of a
+ForAllTy.
+
+Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
+substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
+for all f.
+
+The reason for this definition is that the rewriter does not rewrite in coercions
+or variables' kinds. In turn, the rewriter does not need to rewrite there because
+those places are never used for controlling the behaviour of the solver: these
+places are not used in matching instances or in decomposing equalities.
+
+There is one exception to the claim that non-rewritable parts of the tree do
+not affect the solver: we sometimes do an occurs-check to decide e.g. how to
+orient an equality. (See the comments on
+GHC.Tc.Solver.Canonical.canEqTyVarFunEq.) Accordingly, the presence of a
+variable in a kind or coercion just might influence the solver. Here is an
+example:
+
+  type family Const x y where
+    Const x y = x
+
+  AxConst :: forall x y. Const x y ~# x
+
+  alpha :: Const Type Nat
+  [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
+                      AxConst Type alpha ;;
+                      sym (AxConst Type Nat))
+
+The cast is clearly ludicrous (it ties together a cast and its symmetric version),
+but we can't quite rule it out. (See (EQ1) from
+Note [Respecting definitional equality] in GHC.Core.TyCo.Rep to see why we need
+the Const Type Nat bit.) And yet this cast will (quite rightly) prevent alpha
+from unifying with the RHS. I (Richard E) don't have an example of where this
+problem can arise from a Haskell program, but we don't have an air-tight argument
+for why the definition of *rewritable* given here is correct.
+
+Taking roles into account: we must consider a rewrite at a given role. That is,
+a rewrite arises from some equality, and that equality has a role associated
+with it. As we traverse a type, we track what role we are allowed to rewrite with.
+
+For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
+Maybe b but not in F b, where F is a type function. This role-aware logic is
+present in both the anyRewritableXXX functions and in the rewriter.
+See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.
+
+Note [Extending the inert equalities]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Main Theorem [Stability under extension]
+   Suppose we have a "work item"
+       lhs -fw-> t
+   and a terminating generalised substitution S,
+   THEN the extended substitution T = S+(lhs -fw-> t)
+        is a terminating generalised substitution
+   PROVIDED
+      (T1) S(fw,lhs) = lhs   -- LHS of work-item is a fixpoint of S(fw,_)
+      (T2) S(fw,t)   = t     -- RHS of work-item is a fixpoint of S(fw,_)
+      (T3) lhs not in t      -- No occurs check in the work item
+          -- If lhs is a type family application, we require only that
+          -- lhs is not *rewritable* in t. See Note [Rewritable] and
+          -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+
+      AND, for every (lhs1 -fs-> s) in S:
+           (K0) not (fw >= fs)
+                Reason: suppose we kick out (lhs1 -fs-> s),
+                        and add (lhs -fw-> t) to the inert set.
+                        The latter can't rewrite the former,
+                        so the kick-out achieved nothing
+
+              -- From here, we can assume fw >= fs
+           OR (K4) lhs1 is a tyvar AND fs >= fw
+
+           OR { (K1) lhs is not rewritable in lhs1. See Note [Rewritable].
+                     Reason: if fw >= fs, WF1 says we can't have both
+                             lhs0 -fw-> t  and  F lhs0 -fs-> s
+
+                AND (K2): guarantees termination of the new substitution
+                    {  (K2a) not (fs >= fs)
+                    OR (K2b) lhs not in s }
+
+                AND (K3) See Note [K3: completeness of solving]
+                    { (K3a) If the role of fs is nominal: s /= lhs
+                      (K3b) If the role of fs is representational:
+                            s is not of form (lhs t1 .. tn) } }
+
+
+Conditions (T1-T3) are established by the canonicaliser
+Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable
+
+The idea is that
+* T1 and T2 are guaranteed by exhaustively rewriting the work-item
+  with S(fw,_).
+
+* T3 is guaranteed by an occurs-check on the work item.
+  This is done during canonicalisation, in canEqOK and checkTypeEq; invariant
+  (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
+
+* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
+  "keep" criteria.) If the current inert S contains a triple that does
+  not satisfy (K1-3), then we remove it from S by "kicking it out",
+  and re-processing it.
+
+* Note that kicking out is a Bad Thing, because it means we have to
+  re-process a constraint.  The less we kick out, the better.
+  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
+  this but haven't done the empirical study to check.
+
+* Assume we have  G>=G, G>=W and that's all.  Then, when performing
+  a unification we add a new given  a -G-> ty.  But doing so does NOT require
+  us to kick out an inert wanted that mentions a, because of (K2a).  This
+  is a common case, hence good not to kick out. See also (K2a) below.
+
+* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
+  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
+         and so K0 holds.  Intuitively, since fw can't rewrite anything (Lemma (L0)),
+         adding it cannot cause any loops
+  This is a common case, because Wanteds cannot rewrite Wanteds.
+  It's used to avoid even looking for constraint to kick out.
+
+* Lemma (L1): The conditions of the Main Theorem imply that there is no
+              (lhs -fs-> t) in S, s.t.  (fs >= fw).
+  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
+  S(fw,lhs)=lhs.  But since fs>=fw, S(fw,lhs) = t, hence t=lhs.  But now we
+  have (lhs -fs-> lhs) in S, which contradicts (WF2).
+
+* The extended substitution satisfies (WF1) and (WF2)
+  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
+  - (T3) guarantees (WF2).
+
+* (K2) and (K4) are about termination.  Intuitively, any infinite chain S^0(f,t),
+  S^1(f,t), S^2(f,t).... must pass through the new work item infinitely
+  often, since the substitution without the work item is terminating; and must
+  pass through at least one of the triples in S infinitely often.
+
+  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f)
+    (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t).
+    It is always safe to extend S with such a triple.
+
+    (NB: we could strengten K1) in this way too, but see K3.
+
+  - (K2b): if lhs not in s, we have no further opportunity to apply the
+    work item
+
+  - (K4): See Note [K4]
+
+* Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
+  if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
+  Proof. K4 holds; thus, we keep.
+
+Key lemma to make it watertight.
+  Under the conditions of the Main Theorem,
+  forall f st fw >= f, a is not in S^k(f,t), for any k
+
+Also, consider roles more carefully. See Note [Flavours with roles]
+
+Note [K4]
+~~~~~~~~~
+K4 is a "keep" condition of Note [Extending the inert equalities].
+Here is the scenario:
+
+* We are considering adding (lhs -fw-> t) to the inert set S.
+* S already has (lhs1 -fs-> s).
+* We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t.
+  See Note [Rewritable]. These are (T1), (T2), and (T3).
+* We further know fw >= fs. (If not, then we short-circuit via (K0).)
+
+K4 says that we may keep lhs1 -fs-> s in S if:
+  lhs1 is a tyvar AND fs >= fw
+
+Why K4 guarantees termination:
+  * If fs >= fw, we know a is not rewritable in t, because of (T2).
+  * We further know lhs /= a, because of (T1).
+  * Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
+    for a use of a -fs-> s (precisely because t does not mention a), and hence,
+    the extended substitution (with lhs -fw-> t in it) is a terminating
+    generalised substitution.
+
+Recall that the termination generalised substitution includes only mappings that
+pass an occurs check. This is (T3). At one point, we worried that the
+argument here would fail if s mentioned a, but (T3) rules out this possibility.
+Put another way: the terminating generalised substitution considers only the inert_eqs,
+not other parts of the inert set (such as the irreds).
+
+Can we liberalise K4? No.
+
+Why we cannot drop the (fs >= fw) condition:
+  * Suppose not (fs >= fw). It might be the case that t mentions a, and this
+    can cause a loop. Example:
+
+      Work:  [G] b ~ a
+      Inert: [D] a ~ b
+
+    (where G >= G, G >= D, and D >= D)
+    If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int.
+
+  * Note that the above example is different if the inert is a Given G, because
+    (T1) won't hold.
+
+Why we cannot drop the tyvar condition:
+  * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2).
+  * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s?
+    Yes! This can happen if t appears within tys.
+
+    Here is an example:
+
+      Work:  [G] a ~ Int
+      Inert: [G] F Int ~ F a
+
+    Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand
+    side. The key reason why K2b works in the tyvar case is that tyvars are atomic:
+    if the right-hand side of an equality does not mention a variable a, then it
+    cannot allow an equality with an LHS of a to fire. This is not the case for
+    type family applications.
+
+Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
+K4 will never prevent an inert with a type family on the left from being kicked
+out.
+
+Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
+This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
+it means we can effectively model the mutable filling of metavariables with
+Given/Nominal equalities. That is: it should be the case that we could rewrite
+our solver never to fill in a metavariable; instead, it would "solve" a wanted
+like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
+We would want the solver to behave the same whether it uses metavariables or
+Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
+just like we never unfill a metavariable. Nice.
+
+Getting this wrong (that is, allowing K4 to apply to situations with the type
+family on the left) led to #19042. (At that point, K4 was known as K2b.)
+
+Originally, this condition was part of K2, but #17672 suggests it should be
+a top-level K condition.
+
+Note [K3: completeness of solving]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(K3) is not necessary for the extended substitution
+to be terminating.  In fact K1 could be made stronger by saying
+   ... then (not (fw >= fs) or not (fs >= fs))
+But it's not enough for S to be terminating; we also want completeness.
+That is, we want to be able to solve all soluble wanted equalities.
+Suppose we have
+
+   work-item   b -G-> a
+   inert-item  a -W-> b
+
+Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
+so we could extend the inerts, thus:
+
+   inert-items   b -G-> a
+                 a -W-> b
+
+But if we kicked-out the inert item, we'd get
+
+   work-item     a -W-> b
+   inert-item    b -G-> a
+
+Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
+So we add one more clause to the kick-out criteria
+
+Another way to understand (K3) is that we treat an inert item
+        a -f-> b
+in the same way as
+        b -f-> a
+So if we kick out one, we should kick out the other.  The orientation
+is somewhat accidental.
+
+When considering roles, we also need the second clause (K3b). Consider
+
+  work-item    c -G/N-> a
+  inert-item   a -W/R-> b c
+
+The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
+But we don't kick out the inert item because not (W/R >= W/R).  So we just
+add the work item. But then, consider if we hit the following:
+
+  work-item    b -G/N-> Id
+  inert-items  a -W/R-> b c
+               c -G/N-> a
+where
+  newtype Id x = Id x
+
+For similar reasons, if we only had (K3a), we wouldn't kick the
+representational inert out. And then, we'd miss solving the inert, which
+now reduced to reflexivity.
+
+The solution here is to kick out representational inerts whenever the
+lhs of a work item is "exposed", where exposed means being at the
+head of the top-level application chain (lhs t1 .. tn).  See
+is_can_eq_lhs_head. This is encoded in (K3b).
+
+Beware: if we make this test succeed too often, we kick out too much,
+and the solver might loop.  Consider (#14363)
+  work item:   [G] a ~R f b
+  inert item:  [G] b ~R f a
+In GHC 8.2 the completeness tests more aggressive, and kicked out
+the inert item; but no rewriting happened and there was an infinite
+loop.  All we need is to have the tyvar at the head.
+
+Note [Flavours with roles]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+The system described in Note [inert_eqs: the inert equalities]
+discusses an abstract
+set of flavours. In GHC, flavours have two components: the flavour proper,
+taken from {Wanted, Derived, Given} and the equality relation (often called
+role), taken from {NomEq, ReprEq}.
+When substituting w.r.t. the inert set,
+as described in Note [inert_eqs: the inert equalities],
+we must be careful to respect all components of a flavour.
+For example, if we have
+
+  inert set: a -G/R-> Int
+             b -G/R-> Bool
+
+  type role T nominal representational
+
+and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
+T Int Bool. The reason is that T's first parameter has a nominal role, and
+thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
+substitution means that the proof in Note [inert_eqs: the inert equalities] may
+need to be revisited, but we don't think that the end conclusion is wrong.
+-}
+
+data InertCans   -- See Note [Detailed InertCans Invariants] for more
+  = IC { inert_eqs :: InertEqs
+              -- See Note [inert_eqs: the inert equalities]
+              -- All CEqCans with a TyVarLHS; index is the LHS tyvar
+              -- Domain = skolems and untouchables; a touchable would be unified
+
+       , inert_funeqs :: FunEqMap EqualCtList
+              -- All CEqCans with a TyFamLHS; index is the whole family head type.
+              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
+              --     wrt inert_eqs
+              -- Can include all flavours, [G], [W], [WD], [D]
+
+       , inert_dicts :: DictMap Ct
+              -- Dictionaries only
+              -- All fully rewritten (modulo flavour constraints)
+              --     wrt inert_eqs
+
+       , inert_insts :: [QCInst]
+
+       , inert_safehask :: DictMap Ct
+              -- Failed dictionary resolution due to Safe Haskell overlapping
+              -- instances restriction. We keep this separate from inert_dicts
+              -- as it doesn't cause compilation failure, just safe inference
+              -- failure.
+              --
+              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
+              -- in GHC.Tc.Solver
+
+       , inert_irreds :: Cts
+              -- Irreducible predicates that cannot be made canonical,
+              --     and which don't interact with others (e.g.  (c a))
+              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])
+
+       , inert_given_eq_lvl :: TcLevel
+              -- The TcLevel of the innermost implication that has a Given
+              -- equality of the sort that make a unification variable untouchable
+              -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
+              -- See Note [Tracking Given equalities]
+
+       , inert_given_eqs :: Bool
+              -- True <=> The inert Givens *at this level* (tcl_tclvl)
+              --          could includes at least one equality /other than/ a
+              --          let-bound skolem equality.
+              -- Reason: report these givens when reporting a failed equality
+              -- See Note [Tracking Given equalities]
+       }
+
+type InertEqs    = DTyVarEnv EqualCtList
+
+instance Outputable InertCans where
+  ppr (IC { inert_eqs = eqs
+          , inert_funeqs = funeqs, inert_dicts = dicts
+          , inert_safehask = safehask, inert_irreds = irreds
+          , inert_given_eq_lvl = ge_lvl
+          , inert_given_eqs = given_eqs
+          , inert_insts = insts })
+
+    = braces $ vcat
+      [ ppUnless (isEmptyDVarEnv eqs) $
+        text "Equalities:"
+          <+> pprCts (foldDVarEnv folder emptyCts eqs)
+      , ppUnless (isEmptyTcAppMap funeqs) $
+        text "Type-function equalities =" <+> pprCts (foldFunEqs folder funeqs emptyCts)
+      , ppUnless (isEmptyTcAppMap dicts) $
+        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
+      , ppUnless (isEmptyTcAppMap safehask) $
+        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
+      , ppUnless (isEmptyCts irreds) $
+        text "Irreds =" <+> pprCts irreds
+      , ppUnless (null insts) $
+        text "Given instances =" <+> vcat (map ppr insts)
+      , text "Innermost given equalities =" <+> ppr ge_lvl
+      , text "Given eqs at this level =" <+> ppr given_eqs
+      ]
+    where
+      folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest
+
+{- *********************************************************************
+*                                                                      *
+                   Inert equalities
+*                                                                      *
+********************************************************************* -}
+
+addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
+addTyEq old_eqs tv ct
+  = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct)
+  where
+    add_eq old_eqs _ = addToEqualCtList ct old_eqs
+
+addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
+            -> FunEqMap EqualCtList
+addCanFunEq old_eqs fun_tc fun_args ct
+  = alterTcApp old_eqs fun_tc fun_args upd
+  where
+    upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list
+    upd Nothing                  = Just $ unitEqualCtList ct
+
+foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
+foldTyEqs k eqs z
+  = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs
+
+findTyEqs :: InertCans -> TyVar -> [Ct]
+findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $
+                                  lookupDVarEnv (inert_eqs icans) tv)
+
+delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
+delEq ic lhs rhs = case lhs of
+    TyVarLHS tv
+      -> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
+    TyFamLHS tf args
+      -> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
+  where
+    isThisOne :: Ct -> Bool
+    isThisOne (CEqCan { cc_rhs = t1 }) = tcEqTypeNoKindCheck rhs t1
+    isThisOne other = pprPanic "delEq" (ppr lhs $$ ppr ic $$ ppr other)
+
+    upd :: Maybe EqualCtList -> Maybe EqualCtList
+    upd (Just eq_ct_list) = filterEqualCtList (not . isThisOne) eq_ct_list
+    upd Nothing           = Nothing
+
+findEq :: InertCans -> CanEqLHS -> [Ct]
+findEq icans (TyVarLHS tv) = findTyEqs icans tv
+findEq icans (TyFamLHS fun_tc fun_args)
+  = maybe [] id (fmap @Maybe equalCtListToList $
+                 findFunEq (inert_funeqs icans) fun_tc fun_args)
+
+{- *********************************************************************
+*                                                                      *
+                Adding to and removing from the inert set
+*                                                                      *
+*                                                                      *
+********************************************************************* -}
+
+addInertItem :: TcLevel -> InertCans -> Ct -> InertCans
+addInertItem tc_lvl
+             ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
+             item@(CEqCan { cc_lhs = lhs })
+  = updateGivenEqs tc_lvl item $
+    case lhs of
+       TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item }
+       TyVarLHS tv     -> ics { inert_eqs    = addTyEq eqs tv item }
+
+addInertItem tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
+  = updateGivenEqs tc_lvl item $   -- An Irred might turn out to be an
+                                 -- equality, so we play safe
+    ics { inert_irreds = irreds `snocBag` item }
+
+addInertItem _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
+  = ics { inert_dicts = addDictCt (inert_dicts ics) cls tys item }
+
+addInertItem _ _ item
+  = pprPanic "upd_inert set: can't happen! Inserting " $
+    ppr item   -- Can't be CNonCanonical because they only land in inert_irreds
+
+updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
+-- Set the inert_given_eq_level to the current level (tclvl)
+-- if the constraint is a given equality that should prevent
+-- filling in an outer unification variable.
+-- See Note [Tracking Given equalities]
+updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
+  | not (isGivenCt ct) = inerts
+  | not_equality ct    = inerts -- See Note [Let-bound skolems]
+  | otherwise          = inerts { inert_given_eq_lvl = ge_lvl'
+                                , inert_given_eqs    = True }
+  where
+    ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct)
+              -- Includes things like (c a), which *might* be an equality
+            = tclvl
+            | otherwise
+            = ge_lvl
+
+    not_equality :: Ct -> Bool
+    -- True <=> definitely not an equality of any kind
+    --          except for a let-bound skolem, which doesn't count
+    --          See Note [Let-bound skolems]
+    -- NB: no need to spot the boxed CDictCan (a ~ b) because its
+    --     superclass (a ~# b) will be a CEqCan
+    not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv)
+    not_equality (CDictCan {})                     = True
+    not_equality _                                 = False
+
+kickOutRewritableLHS :: CtFlavourRole  -- Flavour/role of the equality that
+                                       -- is being added to the inert set
+                     -> CanEqLHS       -- The new equality is lhs ~ ty
+                     -> InertCans
+                     -> (WorkList, InertCans)
+-- See Note [kickOutRewritable]
+kickOutRewritableLHS new_fr new_lhs
+                     ics@(IC { inert_eqs      = tv_eqs
+                             , inert_dicts    = dictmap
+                             , inert_funeqs   = funeqmap
+                             , inert_irreds   = irreds
+                             , inert_insts    = old_insts })
+  | not (new_fr `eqMayRewriteFR` new_fr)
+  = (emptyWorkList, ics)
+        -- If new_fr can't rewrite itself, it can't rewrite
+        -- anything else, so no need to kick out anything.
+        -- (This is a common case: wanteds can't rewrite wanteds)
+        -- Lemma (L2) in Note [Extending the inert equalities]
+
+  | otherwise
+  = (kicked_out, inert_cans_in)
+  where
+    -- inert_safehask stays unchanged; is that right?
+    inert_cans_in = ics { inert_eqs      = tv_eqs_in
+                        , inert_dicts    = dicts_in
+                        , inert_funeqs   = feqs_in
+                        , inert_irreds   = irs_in
+                        , inert_insts    = insts_in }
+
+    kicked_out :: WorkList
+    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
+    -- See Note [Prioritise equalities] (Kick-out).
+    -- The irreds may include non-canonical (hetero-kinded) equality
+    -- constraints, which perhaps may have become soluble after new_lhs
+    -- is substituted; ditto the dictionaries, which may include (a~b)
+    -- or (a~~b) constraints.
+    kicked_out = foldr extendWorkListCt
+                          (emptyWorkList { wl_eqs = tv_eqs_out ++ feqs_out })
+                          ((dicts_out `andCts` irs_out)
+                            `extendCtsList` insts_out)
+
+    (tv_eqs_out, tv_eqs_in) = foldDVarEnv (kick_out_eqs extend_tv_eqs)
+                                          ([], emptyDVarEnv) tv_eqs
+    (feqs_out,   feqs_in)   = foldFunEqs  (kick_out_eqs extend_fun_eqs)
+                                          funeqmap ([], emptyFunEqs)
+    (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
+    (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
+      -- Kick out even insolubles: See Note [Rewrite insolubles]
+      -- Of course we must kick out irreducibles like (c a), in case
+      -- we can rewrite 'c' to something more useful
+
+    -- Kick-out for inert instances
+    -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
+    insts_out :: [Ct]
+    insts_in  :: [QCInst]
+    (insts_out, insts_in)
+       | fr_may_rewrite (Given, NomEq)  -- All the insts are Givens
+       = partitionWith kick_out_qci old_insts
+       | otherwise
+       = ([], old_insts)
+    kick_out_qci qci
+      | let ev = qci_ev qci
+      , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
+      = Left (mkNonCanonical ev)
+      | otherwise
+      = Right qci
+
+    (_, new_role) = new_fr
+
+    fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
+    fr_tv_can_rewrite_ty new_tv role ty
+      = anyRewritableTyVar True role can_rewrite ty
+                  -- True: ignore casts and coercions
+      where
+        can_rewrite :: EqRel -> TyVar -> Bool
+        can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv
+
+    fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
+    fr_tf_can_rewrite_ty new_tf new_tf_args role ty
+      = anyRewritableTyFamApp role can_rewrite ty
+      where
+        can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
+        can_rewrite old_role old_tf old_tf_args
+          = new_role `eqCanRewrite` old_role &&
+            tcEqTyConApps new_tf new_tf_args old_tf old_tf_args
+              -- it's possible for old_tf_args to have too many. This is fine;
+              -- we'll only check what we need to.
+
+    {-# INLINE fr_can_rewrite_ty #-}   -- perform the check here only once
+    fr_can_rewrite_ty :: EqRel -> Type -> Bool
+    fr_can_rewrite_ty = case new_lhs of
+      TyVarLHS new_tv             -> fr_tv_can_rewrite_ty new_tv
+      TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args
+
+    fr_may_rewrite :: CtFlavourRole -> Bool
+    fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
+        -- Can the new item rewrite the inert item?
+
+    {-# INLINE kick_out_ct #-}   -- perform case on new_lhs here only once
+    kick_out_ct :: Ct -> Bool
+    -- Kick it out if the new CEqCan can rewrite the inert one
+    -- See Note [kickOutRewritable]
+    kick_out_ct = case new_lhs of
+      TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in
+                                fr_may_rewrite fs
+                             && fr_tv_can_rewrite_ty new_tv role (ctPred ct)
+      TyFamLHS new_tf new_tf_args
+        -> \ct -> let fs@(_, role) = ctFlavourRole ct in
+                  fr_may_rewrite fs
+               && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct)
+
+    extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
+    extend_tv_eqs eqs (TyVarLHS tv) cts = extendDVarEnv eqs tv cts
+    extend_tv_eqs eqs other _cts = pprPanic "extend_tv_eqs" (ppr eqs $$ ppr other)
+
+    extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
+                   -> FunEqMap EqualCtList
+    extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts
+      = insertTcApp eqs fam_tc fam_args cts
+    extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other)
+
+    kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
+                 -> EqualCtList -> ([Ct], container)
+                 -> ([Ct], container)
+    kick_out_eqs extend eqs (acc_out, acc_in)
+      = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of
+            Nothing -> acc_in
+            Just eqs_in_ecl@(EqualCtList (eq1 :| _))
+                    -> extend acc_in (cc_lhs eq1) eqs_in_ecl)
+      where
+        (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs)
+
+    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
+    kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty
+                        , cc_ev = ev, cc_eq_rel = eq_rel })
+      | not (fr_may_rewrite fs)
+      = False  -- (K0) Keep it in the inert set if the new thing can't rewrite it
+
+      -- Below here (fr_may_rewrite fs) is True
+
+      | TyVarLHS _ <- lhs
+      , fs `eqMayRewriteFR` new_fr
+      = False  -- (K4) Keep it in the inert set if the LHS is a tyvar and
+               -- it can rewrite the work item. See Note [K4]
+
+      | fr_can_rewrite_ty eq_rel (canEqLHSType lhs)
+      = True   -- (K1)
+         -- The above check redundantly checks the role & flavour,
+         -- but it's very convenient
+
+      | kick_out_for_inertness    = True   -- (K2)
+      | kick_out_for_completeness = True   -- (K3)
+      | otherwise                 = False
+
+      where
+        fs = (ctEvFlavour ev, eq_rel)
+        kick_out_for_inertness
+          =    (fs `eqMayRewriteFR` fs)           -- (K2a)
+            && fr_can_rewrite_ty eq_rel rhs_ty    -- (K2b)
+
+        kick_out_for_completeness  -- (K3) and Note [K3: completeness of solving]
+          = case eq_rel of
+              NomEq  -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a)
+              ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty    -- (K3b)
+
+    kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
+
+    is_can_eq_lhs_head (TyVarLHS tv) = go
+      where
+        go (Rep.TyVarTy tv')   = tv == tv'
+        go (Rep.AppTy fun _)   = go fun
+        go (Rep.CastTy ty _)   = go ty
+        go (Rep.TyConApp {})   = False
+        go (Rep.LitTy {})      = False
+        go (Rep.ForAllTy {})   = False
+        go (Rep.FunTy {})      = False
+        go (Rep.CoercionTy {}) = False
+    is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go
+      where
+        go (Rep.TyVarTy {})       = False
+        go (Rep.AppTy {})         = False  -- no TyConApp to the left of an AppTy
+        go (Rep.CastTy ty _)      = go ty
+        go (Rep.TyConApp tc args) = tcEqTyConApps fun_tc fun_args tc args
+        go (Rep.LitTy {})         = False
+        go (Rep.ForAllTy {})      = False
+        go (Rep.FunTy {})         = False
+        go (Rep.CoercionTy {})    = False
+
+{- Note [kickOutRewritable]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~
+See also Note [inert_eqs: the inert equalities].
+
+When we add a new inert equality (lhs ~N ty) to the inert set,
+we must kick out any inert items that could be rewritten by the
+new equality, to maintain the inert-set invariants.
+
+  - We want to kick out an existing inert constraint if
+    a) the new constraint can rewrite the inert one
+    b) 'lhs' is free in the inert constraint (so that it *will*)
+       rewrite it if we kick it out.
+
+    For (b) we use anyRewritableCanLHS, which examines the types /and
+    kinds/ that are directly visible in the type. Hence
+    we will have exposed all the rewriting we care about to make the
+    most precise kinds visible for matching classes etc. No need to
+    kick out constraints that mention type variables whose kinds
+    contain this LHS!
+
+  - A Derived equality can kick out [D] constraints in inert_eqs,
+    inert_dicts, inert_irreds etc.
+
+  - We don't kick out constraints from inert_solved_dicts, and
+    inert_solved_funeqs optimistically. But when we lookup we have to
+    take the substitution into account
+
+NB: we could in principle avoid kick-out:
+  a) When unifying a meta-tyvar from an outer level, because
+     then the entire implication will be iterated; see
+     Note [The Unification Level Flag] in GHC.Tc.Solver.Monad.
+
+  b) For Givens, after a unification.  By (GivenInv) in GHC.Tc.Utils.TcType
+     Note [TcLevel invariants], a Given can't include a meta-tyvar from
+     its own level, so it falls under (a).  Of course, we must still
+     kick out Givens when adding a new non-unification Given.
+
+But kicking out more vigorously may lead to earlier unification and fewer
+iterations, so we don't take advantage of these possibilities.
+
+Note [Rewrite insolubles]
+~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose we have an insoluble alpha ~ [alpha], which is insoluble
+because an occurs check.  And then we unify alpha := [Int].  Then we
+really want to rewrite the insoluble to [Int] ~ [[Int]].  Now it can
+be decomposed.  Otherwise we end up with a "Can't match [Int] ~
+[[Int]]" which is true, but a bit confusing because the outer type
+constructors match.
+
+Hence:
+ * In the main simplifier loops in GHC.Tc.Solver (solveWanteds,
+   simpl_loop), we feed the insolubles in solveSimpleWanteds,
+   so that they get rewritten (albeit not solved).
+
+ * We kick insolubles out of the inert set, if they can be
+   rewritten (see GHC.Tc.Solver.Monad.kick_out_rewritable)
+
+ * We rewrite those insolubles in GHC.Tc.Solver.Canonical.
+   See Note [Make sure that insolubles are fully rewritten]
+   in GHC.Tc.Solver.Canonical.
+-}
+
+{- *********************************************************************
+*                                                                      *
+                 Queries
+*                                                                      *
+*                                                                      *
+********************************************************************* -}
+
+mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
+mentionsOuterVar tclvl ev
+  = anyFreeVarsOfType (isOuterTyVar tclvl) $
+    ctEvPred ev
+
+isOuterTyVar :: TcLevel -> TyCoVar -> Bool
+-- True of a type variable that comes from a
+-- shallower level than the ambient level (tclvl)
+isOuterTyVar tclvl tv
+  | isTyVar tv = assertPpr (not (isTouchableMetaTyVar tclvl tv)) (ppr tv <+> ppr tclvl) $
+                 tclvl `strictlyDeeperThan` tcTyVarLevel tv
+    -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from
+    -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't
+    -- be a touchable meta tyvar.   If this wasn't true, you might worry that,
+    -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby
+    -- becomes "outer" even though its level numbers says it isn't.
+  | otherwise  = False  -- Coercion variables; doesn't much matter
+
+-- | Returns Given constraints that might,
+-- potentially, match the given pred. This is used when checking to see if a
+-- Given might overlap with an instance. See Note [Instance and Given overlap]
+-- in "GHC.Tc.Solver.Interact"
+matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
+matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
+  = filterBag matchable_given all_relevant_givens
+  where
+    -- just look in class constraints and irreds. matchableGivens does get called
+    -- for ~R constraints, but we don't need to look through equalities, because
+    -- canonical equalities are used for rewriting. We'll only get caught by
+    -- non-canonical -- that is, irreducible -- equalities.
+    all_relevant_givens :: Cts
+    all_relevant_givens
+      | Just (clas, _) <- getClassPredTys_maybe pred_w
+      = findDictsByClass (inert_dicts inert_cans) clas
+        `unionBags` inert_irreds inert_cans
+      | otherwise
+      = inert_irreds inert_cans
+
+    matchable_given :: Ct -> Bool
+    matchable_given ct
+      | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
+      = mightEqualLater inerts pred_g loc_g pred_w loc_w
+
+      | otherwise
+      = False
+
+mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
+-- See Note [What might equal later?]
+-- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
+mightEqualLater (IS { inert_cycle_breakers = cbvs })
+                given_pred given_loc wanted_pred wanted_loc
+  | prohibitedSuperClassSolve given_loc wanted_loc
+  = False
+
+  | otherwise
+  = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
+      SurelyApart              -> False  -- types that are surely apart do not equal later
+      MaybeApart MARInfinite _ -> False  -- see Example 7 in the Note.
+      _                        -> True
+
+  where
+    in_scope  = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
+
+    -- NB: flatten both at the same time, so that we can share mappings
+    -- from type family applications to variables, and also to guarantee
+    -- that the fresh variables are really fresh between the given and
+    -- the wanted. Flattening both at the same time is needed to get
+    -- Example 10 from the Note.
+    ([flattened_given, flattened_wanted], var_mapping)
+      = flattenTysX in_scope [given_pred, wanted_pred]
+
+    bind_fun :: BindFun
+    bind_fun tv rhs_ty
+      | isMetaTyVar tv
+      , can_unify tv (metaTyVarInfo tv) rhs_ty
+         -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
+         -- the latter was #19106.
+      = BindMe
+
+         -- See Examples 4, 5, and 6 from the Note
+      | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
+      , anyFreeVarsOfTypes mentions_meta_ty_var fam_args
+      = BindMe
+
+      | otherwise
+      = Apart
+
+    -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
+    -- (as they can be unified)
+    -- and also for CycleBreakerTvs that mentions meta-tyvars
+    mentions_meta_ty_var :: TyVar -> Bool
+    mentions_meta_ty_var tv
+      | isMetaTyVar tv
+      = case metaTyVarInfo tv of
+          -- See Examples 8 and 9 in the Note
+          CycleBreakerTv
+            | Just tyfam_app <- lookup tv cbvs
+            -> anyFreeVarsOfType mentions_meta_ty_var tyfam_app
+            | otherwise
+            -> pprPanic "mightEqualLater finds an unbound cbv" (ppr tv $$ ppr cbvs)
+          _ -> True
+      | otherwise
+      = False
+
+    -- like canSolveByUnification, but allows cbv variables to unify
+    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
+    can_unify _lhs_tv TyVarTv rhs_ty  -- see Example 3 from the Note
+      | Just rhs_tv <- tcGetTyVar_maybe rhs_ty
+      = case tcTyVarDetails rhs_tv of
+          MetaTv { mtv_info = TyVarTv } -> True
+          MetaTv {}                     -> False  -- could unify with anything
+          SkolemTv {}                   -> True
+          RuntimeUnk                    -> True
+      | otherwise  -- not a var on the RHS
+      = False
+    can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
+
+prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
+-- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
+prohibitedSuperClassSolve from_loc solve_loc
+  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
+  , ScOrigin wanted_size <- ctLocOrigin solve_loc
+  = given_size >= wanted_size
+  | otherwise
+  = False
diff --git a/compiler/GHC/Tc/Solver/Interact.hs b/compiler/GHC/Tc/Solver/Interact.hs
index efa03834dd..6e051c9ef6 100644
--- a/compiler/GHC/Tc/Solver/Interact.hs
+++ b/compiler/GHC/Tc/Solver/Interact.hs
@@ -38,6 +38,8 @@ import GHC.Tc.Types.Constraint
 import GHC.Core.Predicate
 import GHC.Tc.Types.Origin
 import GHC.Tc.Utils.TcMType( promoteMetaTyVarTo )
+import GHC.Tc.Solver.Types
+import GHC.Tc.Solver.InertSet
 import GHC.Tc.Solver.Monad
 import GHC.Data.Bag
 import GHC.Utils.Monad ( concatMapM, foldlM )
@@ -2389,7 +2391,7 @@ The same reasoning applies to
 
 And less obviously to:
 
-* Tuple classes.  For reasons described in GHC.Tc.Solver.Monad
+* Tuple classes.  For reasons described in GHC.Tc.Solver.Types
   Note [Tuples hiding implicit parameters], we may have a constraint
      [W] (?x::Int, C a)
   with an exactly-matching Given constraint.  We must decompose this
diff --git a/compiler/GHC/Tc/Solver/Monad.hs b/compiler/GHC/Tc/Solver/Monad.hs
index 3428e811ad..96228fcce5 100644
--- a/compiler/GHC/Tc/Solver/Monad.hs
+++ b/compiler/GHC/Tc/Solver/Monad.hs
@@ -3,23 +3,13 @@
 {-# LANGUAGE DerivingStrategies #-}
 {-# LANGUAGE GeneralizedNewtypeDeriving #-}
 {-# LANGUAGE ScopedTypeVariables #-}
-{-# LANGUAGE TypeApplications #-}
 {-# LANGUAGE TypeFamilies #-}
 
-{-# OPTIONS_GHC -Wno-incomplete-record-updates -Wno-incomplete-uni-patterns #-}
+{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
 
--- | Type definitions for the constraint solver
+-- | Monadic definitions for the constraint solver
 module GHC.Tc.Solver.Monad (
 
-    -- The work list
-    WorkList(..), isEmptyWorkList, emptyWorkList,
-    extendWorkListNonEq, extendWorkListCt,
-    extendWorkListCts, extendWorkListEq,
-    appendWorkList,
-    selectNextWorkItem,
-    workListSize,
-    getWorkList, updWorkListTcS, pushLevelNoWorkList,
-
     -- The TcS monad
     TcS, runTcS, runTcSDeriveds, runTcSWithEvBinds, runTcSInerts,
     failTcS, warnTcS, addErrTcS, wrapTcS,
@@ -27,6 +17,11 @@ module GHC.Tc.Solver.Monad (
     nestTcS, nestImplicTcS, setEvBindsTcS,
     emitImplicationTcS, emitTvImplicationTcS,
 
+    selectNextWorkItem,
+    getWorkList,
+    updWorkListTcS,
+    pushLevelNoWorkList,
+
     runTcPluginTcS, addUsedGRE, addUsedGREs, keepAlive,
     matchGlobalInst, TcM.ClsInstResult(..),
 
@@ -62,18 +57,17 @@ module GHC.Tc.Solver.Monad (
     tcLookupClass, tcLookupId,
 
     -- Inerts
-    InertSet(..), InertCans(..), emptyInert,
     updInertTcS, updInertCans, updInertDicts, updInertIrreds,
     getHasGivenEqs, setInertCans,
     getInertEqs, getInertCans, getInertGivens,
     getInertInsols, getInnermostGivenEqLevel,
     getTcSInerts, setTcSInerts,
-    matchableGivens, prohibitedSuperClassSolve, mightEqualLater,
     getUnsolvedInerts,
     removeInertCts, getPendingGivenScs,
     addInertCan, insertFunEq, addInertForAll,
     emitWorkNC, emitWork,
     isImprovable,
+    lookupInertDict,
 
     -- The Model
     kickOutAfterUnification,
@@ -82,14 +76,6 @@ module GHC.Tc.Solver.Monad (
     addInertSafehask, insertSafeOverlapFailureTcS, updInertSafehask,
     getSafeOverlapFailures,
 
-    -- Inert CDictCans
-    DictMap, emptyDictMap, lookupInertDict, findDictsByClass, addDict,
-    addDictsByClass, delDict, foldDicts, filterDicts, findDict,
-
-    -- Inert CEqCans
-    EqualCtList(..), findTyEqs, foldTyEqs,
-    findEq,
-
     -- Inert solved dictionaries
     addSolvedDict, lookupSolvedDict,
 
@@ -100,9 +86,6 @@ module GHC.Tc.Solver.Monad (
     lookupFamAppInert, lookupFamAppCache, extendFamAppCache,
     pprKicked,
 
-    -- Inert function equalities
-    findFunEq, findFunEqsByTyCon,
-
     instDFunType,                              -- Instantiation
 
     -- MetaTyVars
@@ -153,7 +136,9 @@ import GHC.Driver.Session
 import GHC.Core.Type
 import qualified GHC.Core.TyCo.Rep as Rep  -- this needs to be used only very locally
 import GHC.Core.Coercion
-import GHC.Core.Unify
+
+import GHC.Tc.Solver.Types
+import GHC.Tc.Solver.InertSet
 
 import GHC.Tc.Types.Evidence
 import GHC.Core.Class
@@ -173,1173 +158,25 @@ import GHC.Utils.Panic
 import GHC.Utils.Logger
 import GHC.Data.Bag as Bag
 import GHC.Types.Unique.Supply
-import GHC.Utils.Misc
 import GHC.Tc.Types
 import GHC.Tc.Types.Origin
 import GHC.Tc.Types.Constraint
 import GHC.Core.Predicate
 
 import GHC.Types.Unique.Set
-import GHC.Core.TyCon.Env
-import GHC.Data.Maybe
-
-import GHC.Core.Map.Type
-import GHC.Data.TrieMap
 
 import Control.Monad
 import GHC.Utils.Monad
 import Data.IORef
 import GHC.Exts (oneShot)
-import Data.List ( partition, mapAccumL )
-import Data.List.NonEmpty ( NonEmpty(..), cons, toList, nonEmpty )
-import qualified Data.List.NonEmpty as NE
+import Data.List ( mapAccumL )
+import Data.List.NonEmpty ( NonEmpty(..) )
 import Control.Arrow ( first )
 
 #if defined(DEBUG)
 import GHC.Data.Graph.Directed
 #endif
 
-{-
-************************************************************************
-*                                                                      *
-*                            Worklists                                *
-*  Canonical and non-canonical constraints that the simplifier has to  *
-*  work on. Including their simplification depths.                     *
-*                                                                      *
-*                                                                      *
-************************************************************************
-
-Note [WorkList priorities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-A WorkList contains canonical and non-canonical items (of all flavours).
-Notice that each Ct now has a simplification depth. We may
-consider using this depth for prioritization as well in the future.
-
-As a simple form of priority queue, our worklist separates out
-
-* equalities (wl_eqs); see Note [Prioritise equalities]
-* all the rest (wl_rest)
-
-Note [Prioritise equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-It's very important to process equalities /first/:
-
-* (Efficiency)  The general reason to do so is that if we process a
-  class constraint first, we may end up putting it into the inert set
-  and then kicking it out later.  That's extra work compared to just
-  doing the equality first.
-
-* (Avoiding fundep iteration) As #14723 showed, it's possible to
-  get non-termination if we
-      - Emit the Derived fundep equalities for a class constraint,
-        generating some fresh unification variables.
-      - That leads to some unification
-      - Which kicks out the class constraint
-      - Which isn't solved (because there are still some more Derived
-        equalities in the work-list), but generates yet more fundeps
-  Solution: prioritise derived equalities over class constraints
-
-* (Class equalities) We need to prioritise equalities even if they
-  are hidden inside a class constraint;
-  see Note [Prioritise class equalities]
-
-* (Kick-out) We want to apply this priority scheme to kicked-out
-  constraints too (see the call to extendWorkListCt in kick_out_rewritable
-  E.g. a CIrredCan can be a hetero-kinded (t1 ~ t2), which may become
-  homo-kinded when kicked out, and hence we want to prioritise it.
-
-* (Derived equalities) Originally we tried to postpone processing
-  Derived equalities, in the hope that we might never need to deal
-  with them at all; but in fact we must process Derived equalities
-  eagerly, partly for the (Efficiency) reason, and more importantly
-  for (Avoiding fundep iteration).
-
-Note [Prioritise class equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-We prioritise equalities in the solver (see selectWorkItem). But class
-constraints like (a ~ b) and (a ~~ b) are actually equalities too;
-see Note [The equality types story] in GHC.Builtin.Types.Prim.
-
-Failing to prioritise these is inefficient (more kick-outs etc).
-But, worse, it can prevent us spotting a "recursive knot" among
-Wanted constraints.  See comment:10 of #12734 for a worked-out
-example.
-
-So we arrange to put these particular class constraints in the wl_eqs.
-
-  NB: since we do not currently apply the substitution to the
-  inert_solved_dicts, the knot-tying still seems a bit fragile.
-  But this makes it better.
-
--}
-
--- See Note [WorkList priorities]
-data WorkList
-  = WL { wl_eqs     :: [Ct]  -- CEqCan, CDictCan, CIrredCan
-                             -- Given, Wanted, and Derived
-                       -- Contains both equality constraints and their
-                       -- class-level variants (a~b) and (a~~b);
-                       -- See Note [Prioritise equalities]
-                       -- See Note [Prioritise class equalities]
-
-       , wl_rest    :: [Ct]
-
-       , wl_implics :: Bag Implication  -- See Note [Residual implications]
-    }
-
-appendWorkList :: WorkList -> WorkList -> WorkList
-appendWorkList
-    (WL { wl_eqs = eqs1, wl_rest = rest1
-        , wl_implics = implics1 })
-    (WL { wl_eqs = eqs2, wl_rest = rest2
-        , wl_implics = implics2 })
-   = WL { wl_eqs     = eqs1     ++ eqs2
-        , wl_rest    = rest1    ++ rest2
-        , wl_implics = implics1 `unionBags`   implics2 }
-
-workListSize :: WorkList -> Int
-workListSize (WL { wl_eqs = eqs, wl_rest = rest })
-  = length eqs + length rest
-
-extendWorkListEq :: Ct -> WorkList -> WorkList
-extendWorkListEq ct wl = wl { wl_eqs = ct : wl_eqs wl }
-
-extendWorkListNonEq :: Ct -> WorkList -> WorkList
--- Extension by non equality
-extendWorkListNonEq ct wl = wl { wl_rest = ct : wl_rest wl }
-
-extendWorkListDeriveds :: [CtEvidence] -> WorkList -> WorkList
-extendWorkListDeriveds evs wl
-  = extendWorkListCts (map mkNonCanonical evs) wl
-
-extendWorkListImplic :: Implication -> WorkList -> WorkList
-extendWorkListImplic implic wl = wl { wl_implics = implic `consBag` wl_implics wl }
-
-extendWorkListCt :: Ct -> WorkList -> WorkList
--- Agnostic
-extendWorkListCt ct wl
- = case classifyPredType (ctPred ct) of
-     EqPred {}
-       -> extendWorkListEq ct wl
-
-     ClassPred cls _  -- See Note [Prioritise class equalities]
-       |  isEqPredClass cls
-       -> extendWorkListEq ct wl
-
-     _ -> extendWorkListNonEq ct wl
-
-extendWorkListCts :: [Ct] -> WorkList -> WorkList
--- Agnostic
-extendWorkListCts cts wl = foldr extendWorkListCt wl cts
-
-isEmptyWorkList :: WorkList -> Bool
-isEmptyWorkList (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
-  = null eqs && null rest && isEmptyBag implics
-
-emptyWorkList :: WorkList
-emptyWorkList = WL { wl_eqs  = [], wl_rest = [], wl_implics = emptyBag }
-
-selectWorkItem :: WorkList -> Maybe (Ct, WorkList)
--- See Note [Prioritise equalities]
-selectWorkItem wl@(WL { wl_eqs = eqs, wl_rest = rest })
-  | ct:cts <- eqs  = Just (ct, wl { wl_eqs    = cts })
-  | ct:cts <- rest = Just (ct, wl { wl_rest   = cts })
-  | otherwise      = Nothing
-
-getWorkList :: TcS WorkList
-getWorkList = do { wl_var <- getTcSWorkListRef
-                 ; wrapTcS (TcM.readTcRef wl_var) }
-
-selectNextWorkItem :: TcS (Maybe Ct)
--- Pick which work item to do next
--- See Note [Prioritise equalities]
-selectNextWorkItem
-  = do { wl_var <- getTcSWorkListRef
-       ; wl <- readTcRef wl_var
-       ; case selectWorkItem wl of {
-           Nothing -> return Nothing ;
-           Just (ct, new_wl) ->
-    do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
-         -- This is done by GHC.Tc.Solver.Interact.chooseInstance
-       ; writeTcRef wl_var new_wl
-       ; return (Just ct) } } }
-
--- Pretty printing
-instance Outputable WorkList where
-  ppr (WL { wl_eqs = eqs, wl_rest = rest, wl_implics = implics })
-   = text "WL" <+> (braces $
-     vcat [ ppUnless (null eqs) $
-            text "Eqs =" <+> vcat (map ppr eqs)
-          , ppUnless (null rest) $
-            text "Non-eqs =" <+> vcat (map ppr rest)
-          , ppUnless (isEmptyBag implics) $
-            ifPprDebug (text "Implics =" <+> vcat (map ppr (bagToList implics)))
-                       (text "(Implics omitted)")
-          ])
-
-
-{- *********************************************************************
-*                                                                      *
-                InertSet: the inert set
-*                                                                      *
-*                                                                      *
-********************************************************************* -}
-
-data InertSet
-  = IS { inert_cans :: InertCans
-              -- Canonical Given, Wanted, Derived
-              -- Sometimes called "the inert set"
-
-       , inert_cycle_breakers :: [(TcTyVar, TcType)]
-              -- a list of CycleBreakerTv / original family applications
-              -- used to undo the cycle-breaking needed to handle
-              -- Note [Type variable cycles in Givens] in GHC.Tc.Solver.Canonical
-
-       , inert_famapp_cache :: FunEqMap (TcCoercion, TcType)
-              -- Just a hash-cons cache for use when reducing family applications
-              -- only
-              --
-              -- If    F tys :-> (co, rhs, flav),
-              -- then  co :: rhs ~N F tys
-              -- all evidence is from instances or Givens; no coercion holes here
-              -- (We have no way of "kicking out" from the cache, so putting
-              --  wanteds here means we can end up solving a Wanted with itself. Bad)
-
-       , inert_solved_dicts   :: DictMap CtEvidence
-              -- All Wanteds, of form ev :: C t1 .. tn
-              -- See Note [Solved dictionaries]
-              -- and Note [Do not add superclasses of solved dictionaries]
-       }
-
-instance Outputable InertSet where
-  ppr (IS { inert_cans = ics
-          , inert_solved_dicts = solved_dicts })
-      = vcat [ ppr ics
-             , ppUnless (null dicts) $
-               text "Solved dicts =" <+> vcat (map ppr dicts) ]
-         where
-           dicts = bagToList (dictsToBag solved_dicts)
-
-emptyInertCans :: InertCans
-emptyInertCans
-  = IC { inert_eqs          = emptyDVarEnv
-       , inert_given_eq_lvl = topTcLevel
-       , inert_given_eqs    = False
-       , inert_dicts        = emptyDicts
-       , inert_safehask     = emptyDicts
-       , inert_funeqs       = emptyFunEqs
-       , inert_insts        = []
-       , inert_irreds       = emptyCts }
-
-emptyInert :: InertSet
-emptyInert
-  = IS { inert_cans           = emptyInertCans
-       , inert_cycle_breakers = []
-       , inert_famapp_cache   = emptyFunEqs
-       , inert_solved_dicts   = emptyDictMap }
-
-
-{- Note [Solved dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-When we apply a top-level instance declaration, we add the "solved"
-dictionary to the inert_solved_dicts.  In general, we use it to avoid
-creating a new EvVar when we have a new goal that we have solved in
-the past.
-
-But in particular, we can use it to create *recursive* dictionaries.
-The simplest, degenerate case is
-    instance C [a] => C [a] where ...
-If we have
-    [W] d1 :: C [x]
-then we can apply the instance to get
-    d1 = $dfCList d
-    [W] d2 :: C [x]
-Now 'd1' goes in inert_solved_dicts, and we can solve d2 directly from d1.
-    d1 = $dfCList d
-    d2 = d1
-
-See Note [Example of recursive dictionaries]
-
-VERY IMPORTANT INVARIANT:
-
- (Solved Dictionary Invariant)
-    Every member of the inert_solved_dicts is the result
-    of applying an instance declaration that "takes a step"
-
-    An instance "takes a step" if it has the form
-        dfunDList d1 d2 = MkD (...) (...) (...)
-    That is, the dfun is lazy in its arguments, and guarantees to
-    immediately return a dictionary constructor.  NB: all dictionary
-    data constructors are lazy in their arguments.
-
-    This property is crucial to ensure that all dictionaries are
-    non-bottom, which in turn ensures that the whole "recursive
-    dictionary" idea works at all, even if we get something like
-        rec { d = dfunDList d dx }
-    See Note [Recursive superclasses] in GHC.Tc.TyCl.Instance.
-
- Reason:
-   - All instances, except two exceptions listed below, "take a step"
-     in the above sense
-
-   - Exception 1: local quantified constraints have no such guarantee;
-     indeed, adding a "solved dictionary" when appling a quantified
-     constraint led to the ability to define unsafeCoerce
-     in #17267.
-
-   - Exception 2: the magic built-in instance for (~) has no
-     such guarantee.  It behaves as if we had
-         class    (a ~# b) => (a ~ b) where {}
-         instance (a ~# b) => (a ~ b) where {}
-     The "dfun" for the instance is strict in the coercion.
-     Anyway there's no point in recording a "solved dict" for
-     (t1 ~ t2); it's not going to allow a recursive dictionary
-     to be constructed.  Ditto (~~) and Coercible.
-
-THEREFORE we only add a "solved dictionary"
-  - when applying an instance declaration
-  - subject to Exceptions 1 and 2 above
-
-In implementation terms
-  - GHC.Tc.Solver.Monad.addSolvedDict adds a new solved dictionary,
-    conditional on the kind of instance
-
-  - It is only called when applying an instance decl,
-    in GHC.Tc.Solver.Interact.doTopReactDict
-
-  - ClsInst.InstanceWhat says what kind of instance was
-    used to solve the constraint.  In particular
-      * LocalInstance identifies quantified constraints
-      * BuiltinEqInstance identifies the strange built-in
-        instances for equality.
-
-  - ClsInst.instanceReturnsDictCon says which kind of
-    instance guarantees to return a dictionary constructor
-
-Other notes about solved dictionaries
-
-* See also Note [Do not add superclasses of solved dictionaries]
-
-* The inert_solved_dicts field is not rewritten by equalities,
-  so it may get out of date.
-
-* The inert_solved_dicts are all Wanteds, never givens
-
-* We only cache dictionaries from top-level instances, not from
-  local quantified constraints.  Reason: if we cached the latter
-  we'd need to purge the cache when bringing new quantified
-  constraints into scope, because quantified constraints "shadow"
-  top-level instances.
-
-Note [Do not add superclasses of solved dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Every member of inert_solved_dicts is the result of applying a
-dictionary function, NOT of applying superclass selection to anything.
-Consider
-
-        class Ord a => C a where
-        instance Ord [a] => C [a] where ...
-
-Suppose we are trying to solve
-  [G] d1 : Ord a
-  [W] d2 : C [a]
-
-Then we'll use the instance decl to give
-
-  [G] d1 : Ord a     Solved: d2 : C [a] = $dfCList d3
-  [W] d3 : Ord [a]
-
-We must not add d4 : Ord [a] to the 'solved' set (by taking the
-superclass of d2), otherwise we'll use it to solve d3, without ever
-using d1, which would be a catastrophe.
-
-Solution: when extending the solved dictionaries, do not add superclasses.
-That's why each element of the inert_solved_dicts is the result of applying
-a dictionary function.
-
-Note [Example of recursive dictionaries]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
---- Example 1
-
-    data D r = ZeroD | SuccD (r (D r));
-
-    instance (Eq (r (D r))) => Eq (D r) where
-        ZeroD     == ZeroD     = True
-        (SuccD a) == (SuccD b) = a == b
-        _         == _         = False;
-
-    equalDC :: D [] -> D [] -> Bool;
-    equalDC = (==);
-
-We need to prove (Eq (D [])). Here's how we go:
-
-   [W] d1 : Eq (D [])
-By instance decl of Eq (D r):
-   [W] d2 : Eq [D []]      where   d1 = dfEqD d2
-By instance decl of Eq [a]:
-   [W] d3 : Eq (D [])      where   d2 = dfEqList d3
-                                   d1 = dfEqD d2
-Now this wanted can interact with our "solved" d1 to get:
-    d3 = d1
-
--- Example 2:
-This code arises in the context of "Scrap Your Boilerplate with Class"
-
-    class Sat a
-    class Data ctx a
-    instance  Sat (ctx Char)             => Data ctx Char       -- dfunData1
-    instance (Sat (ctx [a]), Data ctx a) => Data ctx [a]        -- dfunData2
-
-    class Data Maybe a => Foo a
-
-    instance Foo t => Sat (Maybe t)                             -- dfunSat
-
-    instance Data Maybe a => Foo a                              -- dfunFoo1
-    instance Foo a        => Foo [a]                            -- dfunFoo2
-    instance                 Foo [Char]                         -- dfunFoo3
-
-Consider generating the superclasses of the instance declaration
-         instance Foo a => Foo [a]
-
-So our problem is this
-    [G] d0 : Foo t
-    [W] d1 : Data Maybe [t]   -- Desired superclass
-
-We may add the given in the inert set, along with its superclasses
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  WorkList
-    [W] d1 : Data Maybe [t]
-
-Solve d1 using instance dfunData2; d1 := dfunData2 d2 d3
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-  WorkList:
-    [W] d2 : Sat (Maybe [t])
-    [W] d3 : Data Maybe t
-
-Now, we may simplify d2 using dfunSat; d2 := dfunSat d4
-  Inert:
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList:
-    [W] d3 : Data Maybe t
-    [W] d4 : Foo [t]
-
-Now, we can just solve d3 from d01; d3 := d01
-  Inert
-    [G] d0 : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-  WorkList
-    [W] d4 : Foo [t]
-
-Now, solve d4 using dfunFoo2;  d4 := dfunFoo2 d5
-  Inert
-    [G] d0  : Foo t
-    [G] d01 : Data Maybe t   -- Superclass of d0
-  Solved:
-        d1 : Data Maybe [t]
-        d2 : Sat (Maybe [t])
-        d4 : Foo [t]
-  WorkList:
-    [W] d5 : Foo t
-
-Now, d5 can be solved! d5 := d0
-
-Result
-   d1 := dfunData2 d2 d3
-   d2 := dfunSat d4
-   d3 := d01
-   d4 := dfunFoo2 d5
-   d5 := d0
--}
-
-{- *********************************************************************
-*                                                                      *
-                InertCans: the canonical inerts
-*                                                                      *
-*                                                                      *
-********************************************************************* -}
-
-data InertCans   -- See Note [Detailed InertCans Invariants] for more
-  = IC { inert_eqs :: InertEqs
-              -- See Note [inert_eqs: the inert equalities]
-              -- All CEqCans with a TyVarLHS; index is the LHS tyvar
-              -- Domain = skolems and untouchables; a touchable would be unified
-
-       , inert_funeqs :: FunEqMap EqualCtList
-              -- All CEqCans with a TyFamLHS; index is the whole family head type.
-              -- LHS is fully rewritten (modulo eqCanRewrite constraints)
-              --     wrt inert_eqs
-              -- Can include all flavours, [G], [W], [WD], [D]
-
-       , inert_dicts :: DictMap Ct
-              -- Dictionaries only
-              -- All fully rewritten (modulo flavour constraints)
-              --     wrt inert_eqs
-
-       , inert_insts :: [QCInst]
-
-       , inert_safehask :: DictMap Ct
-              -- Failed dictionary resolution due to Safe Haskell overlapping
-              -- instances restriction. We keep this separate from inert_dicts
-              -- as it doesn't cause compilation failure, just safe inference
-              -- failure.
-              --
-              -- ^ See Note [Safe Haskell Overlapping Instances Implementation]
-              -- in "GHC.Tc.Solver"
-
-       , inert_irreds :: Cts
-              -- Irreducible predicates that cannot be made canonical,
-              --     and which don't interact with others (e.g.  (c a))
-              -- and insoluble predicates (e.g.  Int ~ Bool, or a ~ [a])
-
-       , inert_given_eq_lvl :: TcLevel
-              -- The TcLevel of the innermost implication that has a Given
-              -- equality of the sort that make a unification variable untouchable
-              -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
-              -- See Note [Tracking Given equalities] below
-
-       , inert_given_eqs :: Bool
-              -- True <=> The inert Givens *at this level* (tcl_tclvl)
-              --          could includes at least one equality /other than/ a
-              --          let-bound skolem equality.
-              -- Reason: report these givens when reporting a failed equality
-              -- See Note [Tracking Given equalities]
-       }
-
-type InertEqs    = DTyVarEnv EqualCtList
-
-newtype EqualCtList = EqualCtList (NonEmpty Ct)
-  deriving newtype Outputable
-  -- See Note [EqualCtList invariants]
-
-unitEqualCtList :: Ct -> EqualCtList
-unitEqualCtList ct = EqualCtList (ct :| [])
-
-addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
--- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList,
--- but not the others. See Note [EqualCtList invariants]
-addToEqualCtList ct (EqualCtList old_eqs)
-  | isWantedCt ct
-  , eq1 :| eqs <- old_eqs
-  = EqualCtList (eq1 :| ct : eqs)
-  | otherwise
-  = EqualCtList (ct `cons` old_eqs)
-
-filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
-filterEqualCtList pred (EqualCtList cts)
-  = fmap EqualCtList (nonEmpty $ NE.filter pred cts)
-
-equalCtListToList :: EqualCtList -> [Ct]
-equalCtListToList (EqualCtList cts) = toList cts
-
-listToEqualCtList :: [Ct] -> Maybe EqualCtList
--- NB: This does not maintain invariants other than having the EqualCtList be
--- non-empty
-listToEqualCtList cts = EqualCtList <$> nonEmpty cts
-
-{- Note [Tracking Given equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For reasons described in (UNTOUCHABLE) in GHC.Tc.Utils.Unify
-Note [Unification preconditions], we can't unify
-   alpha[2] ~ Int
-under a level-4 implication if there are any Given equalities
-bound by the implications at level 3 of 4.  To that end, the
-InertCans tracks
-
-  inert_given_eq_lvl :: TcLevel
-     -- The TcLevel of the innermost implication that has a Given
-     -- equality of the sort that make a unification variable untouchable
-     -- (see Note [Unification preconditions] in GHC.Tc.Utils.Unify).
-
-We update inert_given_eq_lvl whenever we add a Given to the
-inert set, in updateGivenEqs.
-
-Then a unification variable alpha[n] is untouchable iff
-    n < inert_given_eq_lvl
-that is, if the unification variable was born outside an
-enclosing Given equality.
-
-Exactly which constraints should trigger (UNTOUCHABLE), and hence
-should update inert_given_eq_lvl?
-
-* We do /not/ need to worry about let-bound skolems, such ast
-     forall[2] a. a ~ [b] => blah
-  See Note [Let-bound skolems]
-
-* Consider an implication
-      forall[2]. beta[1] => alpha[1] ~ Int
-  where beta is a unification variable that has already been unified
-  to () in an outer scope.  Then alpha[1] is perfectly touchable and
-  we can unify alpha := Int. So when deciding whether the givens contain
-  an equality, we should canonicalise first, rather than just looking at
-  the /original/ givens (#8644).
-
- * However, we must take account of *potential* equalities. Consider the
-   same example again, but this time we have /not/ yet unified beta:
-      forall[2] beta[1] => ...blah...
-
-   Because beta might turn into an equality, updateGivenEqs conservatively
-   treats it as a potential equality, and updates inert_give_eq_lvl
-
- * What about something like forall[2] a b. a ~ F b => [W] alpha[1] ~ X y z?
-
-   That Given cannot affect the Wanted, because the Given is entirely
-   *local*: it mentions only skolems bound in the very same
-   implication. Such equalities need not make alpha untouchable. (Test
-   case typecheck/should_compile/LocalGivenEqs has a real-life
-   motivating example, with some detailed commentary.)
-   Hence the 'mentionsOuterVar' test in updateGivenEqs.
-
-   However, solely to support better error messages
-   (see Note [HasGivenEqs] in GHC.Tc.Types.Constraint) we also track
-   these "local" equalities in the boolean inert_given_eqs field.
-   This field is used only to set the ic_given_eqs field to LocalGivenEqs;
-   see the function getHasGivenEqs.
-
-   Here is a simpler case that triggers this behaviour:
-
-     data T where
-       MkT :: F a ~ G b => a -> b -> T
-
-     f (MkT _ _) = True
-
-   Because of this behaviour around local equality givens, we can infer the
-   type of f. This is typecheck/should_compile/LocalGivenEqs2.
-
- * We need not look at the equality relation involved (nominal vs
-   representational), because representational equalities can still
-   imply nominal ones. For example, if (G a ~R G b) and G's argument's
-   role is nominal, then we can deduce a ~N b.
-
-Note [Let-bound skolems]
-~~~~~~~~~~~~~~~~~~~~~~~~
-If   * the inert set contains a canonical Given CEqCan (a ~ ty)
-and  * 'a' is a skolem bound in this very implication,
-
-then:
-a) The Given is pretty much a let-binding, like
-      f :: (a ~ b->c) => a -> a
-   Here the equality constraint is like saying
-      let a = b->c in ...
-   It is not adding any new, local equality  information,
-   and hence can be ignored by has_given_eqs
-
-b) 'a' will have been completely substituted out in the inert set,
-   so we can safely discard it.
-
-For an example, see #9211.
-
-See also GHC.Tc.Utils.Unify Note [Deeper level on the left] for how we ensure
-that the right variable is on the left of the equality when both are
-tyvars.
-
-You might wonder whether the skolem really needs to be bound "in the
-very same implication" as the equuality constraint.
-Consider this (c.f. #15009):
-
-  data S a where
-    MkS :: (a ~ Int) => S a
-
-  g :: forall a. S a -> a -> blah
-  g x y = let h = \z. ( z :: Int
-                      , case x of
-                           MkS -> [y,z])
-          in ...
-
-From the type signature for `g`, we get `y::a` .  Then when we
-encounter the `\z`, we'll assign `z :: alpha[1]`, say.  Next, from the
-body of the lambda we'll get
-
-  [W] alpha[1] ~ Int                             -- From z::Int
-  [W] forall[2]. (a ~ Int) => [W] alpha[1] ~ a   -- From [y,z]
-
-Now, unify alpha := a.  Now we are stuck with an unsolved alpha~Int!
-So we must treat alpha as untouchable under the forall[2] implication.
-
-Note [Detailed InertCans Invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The InertCans represents a collection of constraints with the following properties:
-
-  * All canonical
-
-  * No two dictionaries with the same head
-  * No two CIrreds with the same type
-
-  * Family equations inert wrt top-level family axioms
-
-  * Dictionaries have no matching top-level instance
-
-  * Given family or dictionary constraints don't mention touchable
-    unification variables
-
-  * Non-CEqCan constraints are fully rewritten with respect
-    to the CEqCan equalities (modulo eqCanRewrite of course;
-    eg a wanted cannot rewrite a given)
-
-  * CEqCan equalities: see Note [inert_eqs: the inert equalities]
-    Also see documentation in Constraint.Ct for a list of invariants
-
-Note [EqualCtList invariants]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-    * All are equalities
-    * All these equalities have the same LHS
-    * The list is never empty
-    * No element of the list can rewrite any other
-    * Derived before Wanted
-
-From the fourth invariant it follows that the list is
-   - A single [G], or
-   - Zero or one [D] or [WD], followed by any number of [W]
-
-The Wanteds can't rewrite anything which is why we put them last
-
-Note [inert_eqs: the inert equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Definition [Can-rewrite relation]
-A "can-rewrite" relation between flavours, written f1 >= f2, is a
-binary relation with the following properties
-
-  (R1) >= is transitive
-  (R2) If f1 >= f, and f2 >= f,
-       then either f1 >= f2 or f2 >= f1
-  (See Note [Why R2?].)
-
-Lemma (L0). If f1 >= f then f1 >= f1
-Proof.      By property (R2), with f1=f2
-
-Definition [Generalised substitution]
-A "generalised substitution" S is a set of triples (lhs -f-> t), where
-  lhs is a type variable or an exactly-saturated type family application
-    (that is, lhs is a CanEqLHS)
-  t is a type
-  f is a flavour
-such that
-  (WF1) if (lhs1 -f1-> t1) in S
-           (lhs2 -f2-> t2) in S
-        then (f1 >= f2) implies that lhs1 does not appear within lhs2
-  (WF2) if (lhs -f-> t) is in S, then t /= lhs
-
-Definition [Applying a generalised substitution]
-If S is a generalised substitution
-   S(f,t0) = t,  if (t0 -fs-> t) in S, and fs >= f
-           = apply S to components of t0, otherwise
-See also Note [Flavours with roles].
-
-Theorem: S(f,t0) is well defined as a function.
-Proof: Suppose (lhs -f1-> t1) and (lhs -f2-> t2) are both in S,
-               and  f1 >= f and f2 >= f
-       Then by (R2) f1 >= f2 or f2 >= f1, which contradicts (WF1)
-
-Notation: repeated application.
-  S^0(f,t)     = t
-  S^(n+1)(f,t) = S(f, S^n(t))
-
-Definition: terminating generalised substitution
-A generalised substitution S is *terminating* iff
-
-  (IG1) there is an n such that
-        for every f,t, S^n(f,t) = S^(n+1)(f,t)
-
-By (IG1) we define S*(f,t) to be the result of exahaustively
-applying S(f,_) to t.
-
------------------------------------------------------------------------------
-Our main invariant:
-   the CEqCans in inert_eqs should be a terminating generalised substitution
------------------------------------------------------------------------------
-
-Note that termination is not the same as idempotence.  To apply S to a
-type, you may have to apply it recursively.  But termination does
-guarantee that this recursive use will terminate.
-
-Note [Why R2?]
-~~~~~~~~~~~~~~
-R2 states that, if we have f1 >= f and f2 >= f, then either f1 >= f2 or f2 >=
-f1. If we do not have R2, we will easily fall into a loop.
-
-To see why, imagine we have f1 >= f, f2 >= f, and that's it. Then, let our
-inert set S = {a -f1-> b, b -f2-> a}. Computing S(f,a) does not terminate. And
-yet, we have a hard time noticing an occurs-check problem when building S, as
-the two equalities cannot rewrite one another.
-
-R2 actually restricts our ability to accept user-written programs. See Note
-[Deriveds do rewrite Deriveds] in GHC.Tc.Types.Constraint for an example.
-
-Note [Rewritable]
-~~~~~~~~~~~~~~~~~
-This Note defines what it means for a type variable or type family application
-(that is, a CanEqLHS) to be rewritable in a type. This definition is used
-by the anyRewritableXXX family of functions and is meant to model the actual
-behaviour in GHC.Tc.Solver.Rewrite.
-
-Ignoring roles (for now): A CanEqLHS lhs is *rewritable* in a type t if the
-lhs tree appears as a subtree within t without traversing any of the following
-components of t:
-  * coercions (whether they appear in casts CastTy or as arguments CoercionTy)
-  * kinds of variable occurrences
-The check for rewritability *does* look in kinds of the bound variable of a
-ForAllTy.
-
-Goal: If lhs is not rewritable in t, then t is a fixpoint of the generalised
-substitution containing only {lhs -f*-> t'}, where f* is a flavour such that f* >= f
-for all f.
-
-The reason for this definition is that the rewriter does not rewrite in coercions
-or variables' kinds. In turn, the rewriter does not need to rewrite there because
-those places are never used for controlling the behaviour of the solver: these
-places are not used in matching instances or in decomposing equalities.
-
-There is one exception to the claim that non-rewritable parts of the tree do
-not affect the solver: we sometimes do an occurs-check to decide e.g. how to
-orient an equality. (See the comments on
-GHC.Tc.Solver.Canonical.canEqTyVarFunEq.) Accordingly, the presence of a
-variable in a kind or coercion just might influence the solver. Here is an
-example:
-
-  type family Const x y where
-    Const x y = x
-
-  AxConst :: forall x y. Const x y ~# x
-
-  alpha :: Const Type Nat
-  [W] alpha ~ Int |> (sym (AxConst Type alpha) ;;
-                      AxConst Type alpha ;;
-                      sym (AxConst Type Nat))
-
-The cast is clearly ludicrous (it ties together a cast and its symmetric version),
-but we can't quite rule it out. (See (EQ1) from
-Note [Respecting definitional equality] in GHC.Core.TyCo.Rep to see why we need
-the Const Type Nat bit.) And yet this cast will (quite rightly) prevent alpha
-from unifying with the RHS. I (Richard E) don't have an example of where this
-problem can arise from a Haskell program, but we don't have an air-tight argument
-for why the definition of *rewritable* given here is correct.
-
-Taking roles into account: we must consider a rewrite at a given role. That is,
-a rewrite arises from some equality, and that equality has a role associated
-with it. As we traverse a type, we track what role we are allowed to rewrite with.
-
-For example, suppose we have an inert [G] b ~R# Int. Then b is rewritable in
-Maybe b but not in F b, where F is a type function. This role-aware logic is
-present in both the anyRewritableXXX functions and in the rewriter.
-See also Note [anyRewritableTyVar must be role-aware] in GHC.Tc.Utils.TcType.
-
-Note [Extending the inert equalities]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Main Theorem [Stability under extension]
-   Suppose we have a "work item"
-       lhs -fw-> t
-   and a terminating generalised substitution S,
-   THEN the extended substitution T = S+(lhs -fw-> t)
-        is a terminating generalised substitution
-   PROVIDED
-      (T1) S(fw,lhs) = lhs   -- LHS of work-item is a fixpoint of S(fw,_)
-      (T2) S(fw,t)   = t     -- RHS of work-item is a fixpoint of S(fw,_)
-      (T3) lhs not in t      -- No occurs check in the work item
-          -- If lhs is a type family application, we require only that
-          -- lhs is not *rewritable* in t. See Note [Rewritable] and
-          -- Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
-
-      AND, for every (lhs1 -fs-> s) in S:
-           (K0) not (fw >= fs)
-                Reason: suppose we kick out (lhs1 -fs-> s),
-                        and add (lhs -fw-> t) to the inert set.
-                        The latter can't rewrite the former,
-                        so the kick-out achieved nothing
-
-              -- From here, we can assume fw >= fs
-           OR (K4) lhs1 is a tyvar AND fs >= fw
-
-           OR { (K1) lhs is not rewritable in lhs1. See Note [Rewritable].
-                     Reason: if fw >= fs, WF1 says we can't have both
-                             lhs0 -fw-> t  and  F lhs0 -fs-> s
-
-                AND (K2): guarantees termination of the new substitution
-                    {  (K2a) not (fs >= fs)
-                    OR (K2b) lhs not in s }
-
-                AND (K3) See Note [K3: completeness of solving]
-                    { (K3a) If the role of fs is nominal: s /= lhs
-                      (K3b) If the role of fs is representational:
-                            s is not of form (lhs t1 .. tn) } }
-
-
-Conditions (T1-T3) are established by the canonicaliser
-Conditions (K1-K3) are established by GHC.Tc.Solver.Monad.kickOutRewritable
-
-The idea is that
-* T1 and T2 are guaranteed by exhaustively rewriting the work-item
-  with S(fw,_).
-
-* T3 is guaranteed by an occurs-check on the work item.
-  This is done during canonicalisation, in canEqOK and checkTypeEq; invariant
-  (TyEq:OC) of CEqCan. See also Note [CEqCan occurs check] in GHC.Tc.Types.Constraint.
-
-* (K1-3) are the "kick-out" criteria.  (As stated, they are really the
-  "keep" criteria.) If the current inert S contains a triple that does
-  not satisfy (K1-3), then we remove it from S by "kicking it out",
-  and re-processing it.
-
-* Note that kicking out is a Bad Thing, because it means we have to
-  re-process a constraint.  The less we kick out, the better.
-  TODO: Make sure that kicking out really *is* a Bad Thing. We've assumed
-  this but haven't done the empirical study to check.
-
-* Assume we have  G>=G, G>=W and that's all.  Then, when performing
-  a unification we add a new given  a -G-> ty.  But doing so does NOT require
-  us to kick out an inert wanted that mentions a, because of (K2a).  This
-  is a common case, hence good not to kick out. See also (K2a) below.
-
-* Lemma (L2): if not (fw >= fw), then K0 holds and we kick out nothing
-  Proof: using Definition [Can-rewrite relation], fw can't rewrite anything
-         and so K0 holds.  Intuitively, since fw can't rewrite anything (Lemma (L0)),
-         adding it cannot cause any loops
-  This is a common case, because Wanteds cannot rewrite Wanteds.
-  It's used to avoid even looking for constraint to kick out.
-
-* Lemma (L1): The conditions of the Main Theorem imply that there is no
-              (lhs -fs-> t) in S, s.t.  (fs >= fw).
-  Proof. Suppose the contrary (fs >= fw).  Then because of (T1),
-  S(fw,lhs)=lhs.  But since fs>=fw, S(fw,lhs) = t, hence t=lhs.  But now we
-  have (lhs -fs-> lhs) in S, which contradicts (WF2).
-
-* The extended substitution satisfies (WF1) and (WF2)
-  - (K1) plus (L1) guarantee that the extended substitution satisfies (WF1).
-  - (T3) guarantees (WF2).
-
-* (K2) and (K4) are about termination.  Intuitively, any infinite chain S^0(f,t),
-  S^1(f,t), S^2(f,t).... must pass through the new work item infinitely
-  often, since the substitution without the work item is terminating; and must
-  pass through at least one of the triples in S infinitely often.
-
-  - (K2a): if not(fs>=fs) then there is no f that fs can rewrite (fs>=f)
-    (this is Lemma (L0)), and hence this triple never plays a role in application S(f,t).
-    It is always safe to extend S with such a triple.
-
-    (NB: we could strengten K1) in this way too, but see K3.
-
-  - (K2b): if lhs not in s, we have no further opportunity to apply the
-    work item
-
-  - (K4): See Note [K4]
-
-* Lemma (L3). Suppose we have f* such that, for all f, f* >= f. Then
-  if we are adding lhs -fw-> t (where T1, T2, and T3 hold), we will keep a -f*-> s.
-  Proof. K4 holds; thus, we keep.
-
-Key lemma to make it watertight.
-  Under the conditions of the Main Theorem,
-  forall f st fw >= f, a is not in S^k(f,t), for any k
-
-Also, consider roles more carefully. See Note [Flavours with roles]
-
-Note [K4]
-~~~~~~~~~
-K4 is a "keep" condition of Note [Extending the inert equalities].
-Here is the scenario:
-
-* We are considering adding (lhs -fw-> t) to the inert set S.
-* S already has (lhs1 -fs-> s).
-* We know S(fw, lhs) = lhs, S(fw, t) = t, and lhs is not rewritable in t.
-  See Note [Rewritable]. These are (T1), (T2), and (T3).
-* We further know fw >= fs. (If not, then we short-circuit via (K0).)
-
-K4 says that we may keep lhs1 -fs-> s in S if:
-  lhs1 is a tyvar AND fs >= fw
-
-Why K4 guarantees termination:
-  * If fs >= fw, we know a is not rewritable in t, because of (T2).
-  * We further know lhs /= a, because of (T1).
-  * Accordingly, a use of the new inert item lhs -fw-> t cannot create the conditions
-    for a use of a -fs-> s (precisely because t does not mention a), and hence,
-    the extended substitution (with lhs -fw-> t in it) is a terminating
-    generalised substitution.
-
-Recall that the termination generalised substitution includes only mappings that
-pass an occurs check. This is (T3). At one point, we worried that the
-argument here would fail if s mentioned a, but (T3) rules out this possibility.
-Put another way: the terminating generalised substitution considers only the inert_eqs,
-not other parts of the inert set (such as the irreds).
-
-Can we liberalise K4? No.
-
-Why we cannot drop the (fs >= fw) condition:
-  * Suppose not (fs >= fw). It might be the case that t mentions a, and this
-    can cause a loop. Example:
-
-      Work:  [G] b ~ a
-      Inert: [D] a ~ b
-
-    (where G >= G, G >= D, and D >= D)
-    If we don't kick out the inert, then we get a loop on e.g. [D] a ~ Int.
-
-  * Note that the above example is different if the inert is a Given G, because
-    (T1) won't hold.
-
-Why we cannot drop the tyvar condition:
-  * Presume fs >= fw. Thus, F tys is not rewritable in t, because of (T2).
-  * Can the use of lhs -fw-> t create the conditions for a use of F tys -fs-> s?
-    Yes! This can happen if t appears within tys.
-
-    Here is an example:
-
-      Work:  [G] a ~ Int
-      Inert: [G] F Int ~ F a
-
-    Now, if we have [W] F a ~ Bool, we will rewrite ad infinitum on the left-hand
-    side. The key reason why K2b works in the tyvar case is that tyvars are atomic:
-    if the right-hand side of an equality does not mention a variable a, then it
-    cannot allow an equality with an LHS of a to fire. This is not the case for
-    type family applications.
-
-Bottom line: K4 can keep only inerts with tyvars on the left. Put differently,
-K4 will never prevent an inert with a type family on the left from being kicked
-out.
-
-Consequence: We never kick out a Given/Nominal equality with a tyvar on the left.
-This is Lemma (L3) of Note [Extending the inert equalities]. It is good because
-it means we can effectively model the mutable filling of metavariables with
-Given/Nominal equalities. That is: it should be the case that we could rewrite
-our solver never to fill in a metavariable; instead, it would "solve" a wanted
-like alpha ~ Int by turning it into a Given, allowing it to be used in rewriting.
-We would want the solver to behave the same whether it uses metavariables or
-Givens. And (L3) says that no Given/Nominals over tyvars are ever kicked out,
-just like we never unfill a metavariable. Nice.
-
-Getting this wrong (that is, allowing K4 to apply to situations with the type
-family on the left) led to #19042. (At that point, K4 was known as K2b.)
-
-Originally, this condition was part of K2, but #17672 suggests it should be
-a top-level K condition.
-
-Note [K3: completeness of solving]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-(K3) is not necessary for the extended substitution
-to be terminating.  In fact K1 could be made stronger by saying
-   ... then (not (fw >= fs) or not (fs >= fs))
-But it's not enough for S to be terminating; we also want completeness.
-That is, we want to be able to solve all soluble wanted equalities.
-Suppose we have
-
-   work-item   b -G-> a
-   inert-item  a -W-> b
-
-Assuming (G >= W) but not (W >= W), this fulfills all the conditions,
-so we could extend the inerts, thus:
-
-   inert-items   b -G-> a
-                 a -W-> b
-
-But if we kicked-out the inert item, we'd get
-
-   work-item     a -W-> b
-   inert-item    b -G-> a
-
-Then rewrite the work-item gives us (a -W-> a), which is soluble via Refl.
-So we add one more clause to the kick-out criteria
-
-Another way to understand (K3) is that we treat an inert item
-        a -f-> b
-in the same way as
-        b -f-> a
-So if we kick out one, we should kick out the other.  The orientation
-is somewhat accidental.
-
-When considering roles, we also need the second clause (K3b). Consider
-
-  work-item    c -G/N-> a
-  inert-item   a -W/R-> b c
-
-The work-item doesn't get rewritten by the inert, because (>=) doesn't hold.
-But we don't kick out the inert item because not (W/R >= W/R).  So we just
-add the work item. But then, consider if we hit the following:
-
-  work-item    b -G/N-> Id
-  inert-items  a -W/R-> b c
-               c -G/N-> a
-where
-  newtype Id x = Id x
-
-For similar reasons, if we only had (K3a), we wouldn't kick the
-representational inert out. And then, we'd miss solving the inert, which
-now reduced to reflexivity.
-
-The solution here is to kick out representational inerts whenever the
-lhs of a work item is "exposed", where exposed means being at the
-head of the top-level application chain (lhs t1 .. tn).  See
-is_can_eq_lhs_head. This is encoded in (K3b).
-
-Beware: if we make this test succeed too often, we kick out too much,
-and the solver might loop.  Consider (#14363)
-  work item:   [G] a ~R f b
-  inert item:  [G] b ~R f a
-In GHC 8.2 the completeness tests more aggressive, and kicked out
-the inert item; but no rewriting happened and there was an infinite
-loop.  All we need is to have the tyvar at the head.
-
-Note [Flavours with roles]
-~~~~~~~~~~~~~~~~~~~~~~~~~~
-The system described in Note [inert_eqs: the inert equalities]
-discusses an abstract
-set of flavours. In GHC, flavours have two components: the flavour proper,
-taken from {Wanted, Derived, Given} and the equality relation (often called
-role), taken from {NomEq, ReprEq}.
-When substituting w.r.t. the inert set,
-as described in Note [inert_eqs: the inert equalities],
-we must be careful to respect all components of a flavour.
-For example, if we have
-
-  inert set: a -G/R-> Int
-             b -G/R-> Bool
-
-  type role T nominal representational
-
-and we wish to compute S(W/R, T a b), the correct answer is T a Bool, NOT
-T Int Bool. The reason is that T's first parameter has a nominal role, and
-thus rewriting a to Int in T a b is wrong. Indeed, this non-congruence of
-substitution means that the proof in Note [The inert equalities] may need
-to be revisited, but we don't think that the end conclusion is wrong.
--}
-
-instance Outputable InertCans where
-  ppr (IC { inert_eqs = eqs
-          , inert_funeqs = funeqs, inert_dicts = dicts
-          , inert_safehask = safehask, inert_irreds = irreds
-          , inert_given_eq_lvl = ge_lvl
-          , inert_given_eqs = given_eqs
-          , inert_insts = insts })
-
-    = braces $ vcat
-      [ ppUnless (isEmptyDVarEnv eqs) $
-        text "Equalities:"
-          <+> pprCts (foldDVarEnv folder emptyCts eqs)
-      , ppUnless (isEmptyTcAppMap funeqs) $
-        text "Type-function equalities =" <+> pprCts (foldFunEqs folder funeqs emptyCts)
-      , ppUnless (isEmptyTcAppMap dicts) $
-        text "Dictionaries =" <+> pprCts (dictsToBag dicts)
-      , ppUnless (isEmptyTcAppMap safehask) $
-        text "Safe Haskell unsafe overlap =" <+> pprCts (dictsToBag safehask)
-      , ppUnless (isEmptyCts irreds) $
-        text "Irreds =" <+> pprCts irreds
-      , ppUnless (null insts) $
-        text "Given instances =" <+> vcat (map ppr insts)
-      , text "Innermost given equalities =" <+> ppr ge_lvl
-      , text "Given eqs at this level =" <+> ppr given_eqs
-      ]
-    where
-      folder (EqualCtList eqs) rest = nonEmptyToBag eqs `andCts` rest
-
 {- *********************************************************************
 *                                                                      *
              Shadow constraints and improvement
@@ -1409,7 +246,8 @@ by the [WD] and we soon get ee := e.
 Additional notes:
 
   * The derived shadow equalities live in inert_eqs, along with
-    the Givens and Wanteds; see Note [EqualCtList invariants].
+    the Givens and Wanteds; see Note [EqualCtList invariants]
+    in GHC.Tc.Solver.Types.
 
   * We make Derived shadows only for Wanteds, not Givens.  So we
     have only [G], not [GD] and [G] plus splitting.  See
@@ -1693,55 +531,6 @@ isImprovable _                                = True
 
 {- *********************************************************************
 *                                                                      *
-                   Inert equalities
-*                                                                      *
-********************************************************************* -}
-
-addTyEq :: InertEqs -> TcTyVar -> Ct -> InertEqs
-addTyEq old_eqs tv ct
-  = extendDVarEnv_C add_eq old_eqs tv (unitEqualCtList ct)
-  where
-    add_eq old_eqs _ = addToEqualCtList ct old_eqs
-
-addCanFunEq :: FunEqMap EqualCtList -> TyCon -> [TcType] -> Ct
-            -> FunEqMap EqualCtList
-addCanFunEq old_eqs fun_tc fun_args ct
-  = alterTcApp old_eqs fun_tc fun_args upd
-  where
-    upd (Just old_equal_ct_list) = Just $ addToEqualCtList ct old_equal_ct_list
-    upd Nothing                  = Just $ unitEqualCtList ct
-
-foldTyEqs :: (Ct -> b -> b) -> InertEqs -> b -> b
-foldTyEqs k eqs z
-  = foldDVarEnv (\(EqualCtList cts) z -> foldr k z cts) z eqs
-
-findTyEqs :: InertCans -> TyVar -> [Ct]
-findTyEqs icans tv = maybe [] id (fmap @Maybe equalCtListToList $
-                                  lookupDVarEnv (inert_eqs icans) tv)
-
-delEq :: InertCans -> CanEqLHS -> TcType -> InertCans
-delEq ic lhs rhs = case lhs of
-    TyVarLHS tv
-      -> ic { inert_eqs = alterDVarEnv upd (inert_eqs ic) tv }
-    TyFamLHS tf args
-      -> ic { inert_funeqs = alterTcApp (inert_funeqs ic) tf args upd }
-  where
-    isThisOne :: Ct -> Bool
-    isThisOne (CEqCan { cc_rhs = t1 }) = tcEqTypeNoKindCheck rhs t1
-    isThisOne other = pprPanic "delEq" (ppr lhs $$ ppr ic $$ ppr other)
-
-    upd :: Maybe EqualCtList -> Maybe EqualCtList
-    upd (Just eq_ct_list) = filterEqualCtList (not . isThisOne) eq_ct_list
-    upd Nothing           = Nothing
-
-findEq :: InertCans -> CanEqLHS -> [Ct]
-findEq icans (TyVarLHS tv) = findTyEqs icans tv
-findEq icans (TyFamLHS fun_tc fun_args)
-  = maybe [] id (fmap @Maybe equalCtListToList $
-                 findFunEq (inert_funeqs icans) fun_tc fun_args)
-
-{- *********************************************************************
-*                                                                      *
                    Inert instances: inert_insts
 *                                                                      *
 ********************************************************************* -}
@@ -1829,7 +618,7 @@ addInertCan ct
        ; ct  <- maybeEmitShadow ics ct
        ; ics <- maybeKickOut ics ct
        ; tclvl <- getTcLevel
-       ; setInertCans (add_item tclvl ics ct)
+       ; setInertCans (addInertItem tclvl ics ct)
 
        ; traceTcS "addInertCan }" $ empty }
 
@@ -1842,54 +631,6 @@ maybeKickOut ics ct
   | otherwise
   = return ics
 
-add_item :: TcLevel -> InertCans -> Ct -> InertCans
-add_item tc_lvl
-         ics@(IC { inert_funeqs = funeqs, inert_eqs = eqs })
-         item@(CEqCan { cc_lhs = lhs })
-  = updateGivenEqs tc_lvl item $
-    case lhs of
-       TyFamLHS tc tys -> ics { inert_funeqs = addCanFunEq funeqs tc tys item }
-       TyVarLHS tv     -> ics { inert_eqs    = addTyEq eqs tv item }
-
-add_item tc_lvl ics@(IC { inert_irreds = irreds }) item@(CIrredCan {})
-  = updateGivenEqs tc_lvl item $   -- An Irred might turn out to be an
-                                 -- equality, so we play safe
-    ics { inert_irreds = irreds `Bag.snocBag` item }
-
-add_item _ ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
-  = ics { inert_dicts = addDictCt (inert_dicts ics) cls tys item }
-
-add_item _ _ item
-  = pprPanic "upd_inert set: can't happen! Inserting " $
-    ppr item   -- Can't be CNonCanonical because they only land in inert_irreds
-
-updateGivenEqs :: TcLevel -> Ct -> InertCans -> InertCans
--- Set the inert_given_eq_level to the current level (tclvl)
--- if the constraint is a given equality that should prevent
--- filling in an outer unification variable.
--- See See Note [Tracking Given equalities]
-updateGivenEqs tclvl ct inerts@(IC { inert_given_eq_lvl = ge_lvl })
-  | not (isGivenCt ct) = inerts
-  | not_equality ct    = inerts -- See Note [Let-bound skolems]
-  | otherwise          = inerts { inert_given_eq_lvl = ge_lvl'
-                                , inert_given_eqs    = True }
-  where
-    ge_lvl' | mentionsOuterVar tclvl (ctEvidence ct)
-              -- Includes things like (c a), which *might* be an equality
-            = tclvl
-            | otherwise
-            = ge_lvl
-
-    not_equality :: Ct -> Bool
-    -- True <=> definitely not an equality of any kind
-    --          except for a let-bound skolem, which doesn't count
-    --          See Note [Let-bound skolems]
-    -- NB: no need to spot the boxed CDictCan (a ~ b) because its
-    --     superclass (a ~# b) will be a CEqCan
-    not_equality (CEqCan { cc_lhs = TyVarLHS tv }) = not (isOuterTyVar tclvl tv)
-    not_equality (CDictCan {})                     = True
-    not_equality _                                 = False
-
 -----------------------------------------
 kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
                                       -- is being added to the inert set
@@ -1897,7 +638,7 @@ kickOutRewritable  :: CtFlavourRole  -- Flavour/role of the equality that
                    -> InertCans
                    -> TcS (Int, InertCans)
 kickOutRewritable new_fr new_lhs ics
-  = do { let (kicked_out, ics') = kick_out_rewritable new_fr new_lhs ics
+  = do { let (kicked_out, ics') = kickOutRewritableLHS new_fr new_lhs ics
              n_kicked = workListSize kicked_out
 
        ; unless (n_kicked == 0) $
@@ -1924,194 +665,6 @@ kickOutRewritable new_fr new_lhs ics
 
        ; return (n_kicked, ics') }
 
-kick_out_rewritable :: CtFlavourRole  -- Flavour/role of the equality that
-                                      -- is being added to the inert set
-                    -> CanEqLHS       -- The new equality is lhs ~ ty
-                    -> InertCans
-                    -> (WorkList, InertCans)
--- See Note [kickOutRewritable]
-kick_out_rewritable new_fr new_lhs
-                    ics@(IC { inert_eqs      = tv_eqs
-                            , inert_dicts    = dictmap
-                            , inert_funeqs   = funeqmap
-                            , inert_irreds   = irreds
-                            , inert_insts    = old_insts })
-  | not (new_fr `eqMayRewriteFR` new_fr)
-  = (emptyWorkList, ics)
-        -- If new_fr can't rewrite itself, it can't rewrite
-        -- anything else, so no need to kick out anything.
-        -- (This is a common case: wanteds can't rewrite wanteds)
-        -- Lemma (L2) in Note [Extending the inert equalities]
-
-  | otherwise
-  = (kicked_out, inert_cans_in)
-  where
-    -- inert_safehask stays unchanged; is that right?
-    inert_cans_in = ics { inert_eqs      = tv_eqs_in
-                        , inert_dicts    = dicts_in
-                        , inert_funeqs   = feqs_in
-                        , inert_irreds   = irs_in
-                        , inert_insts    = insts_in }
-
-    kicked_out :: WorkList
-    -- NB: use extendWorkList to ensure that kicked-out equalities get priority
-    -- See Note [Prioritise equalities] (Kick-out).
-    -- The irreds may include non-canonical (hetero-kinded) equality
-    -- constraints, which perhaps may have become soluble after new_lhs
-    -- is substituted; ditto the dictionaries, which may include (a~b)
-    -- or (a~~b) constraints.
-    kicked_out = foldr extendWorkListCt
-                          (emptyWorkList { wl_eqs = tv_eqs_out ++ feqs_out })
-                          ((dicts_out `andCts` irs_out)
-                            `extendCtsList` insts_out)
-
-    (tv_eqs_out, tv_eqs_in) = foldDVarEnv (kick_out_eqs extend_tv_eqs)
-                                          ([], emptyDVarEnv) tv_eqs
-    (feqs_out,   feqs_in)   = foldFunEqs  (kick_out_eqs extend_fun_eqs)
-                                          funeqmap ([], emptyFunEqs)
-    (dicts_out,  dicts_in)  = partitionDicts   kick_out_ct dictmap
-    (irs_out,    irs_in)    = partitionBag     kick_out_ct irreds
-      -- Kick out even insolubles: See Note [Rewrite insolubles]
-      -- Of course we must kick out irreducibles like (c a), in case
-      -- we can rewrite 'c' to something more useful
-
-    -- Kick-out for inert instances
-    -- See Note [Quantified constraints] in GHC.Tc.Solver.Canonical
-    insts_out :: [Ct]
-    insts_in  :: [QCInst]
-    (insts_out, insts_in)
-       | fr_may_rewrite (Given, NomEq)  -- All the insts are Givens
-       = partitionWith kick_out_qci old_insts
-       | otherwise
-       = ([], old_insts)
-    kick_out_qci qci
-      | let ev = qci_ev qci
-      , fr_can_rewrite_ty NomEq (ctEvPred (qci_ev qci))
-      = Left (mkNonCanonical ev)
-      | otherwise
-      = Right qci
-
-    (_, new_role) = new_fr
-
-    fr_tv_can_rewrite_ty :: TyVar -> EqRel -> Type -> Bool
-    fr_tv_can_rewrite_ty new_tv role ty
-      = anyRewritableTyVar True role can_rewrite ty
-                  -- True: ignore casts and coercions
-      where
-        can_rewrite :: EqRel -> TyVar -> Bool
-        can_rewrite old_role tv = new_role `eqCanRewrite` old_role && tv == new_tv
-
-    fr_tf_can_rewrite_ty :: TyCon -> [TcType] -> EqRel -> Type -> Bool
-    fr_tf_can_rewrite_ty new_tf new_tf_args role ty
-      = anyRewritableTyFamApp role can_rewrite ty
-      where
-        can_rewrite :: EqRel -> TyCon -> [TcType] -> Bool
-        can_rewrite old_role old_tf old_tf_args
-          = new_role `eqCanRewrite` old_role &&
-            tcEqTyConApps new_tf new_tf_args old_tf old_tf_args
-              -- it's possible for old_tf_args to have too many. This is fine;
-              -- we'll only check what we need to.
-
-    {-# INLINE fr_can_rewrite_ty #-}   -- perform the check here only once
-    fr_can_rewrite_ty :: EqRel -> Type -> Bool
-    fr_can_rewrite_ty = case new_lhs of
-      TyVarLHS new_tv             -> fr_tv_can_rewrite_ty new_tv
-      TyFamLHS new_tf new_tf_args -> fr_tf_can_rewrite_ty new_tf new_tf_args
-
-    fr_may_rewrite :: CtFlavourRole -> Bool
-    fr_may_rewrite fs = new_fr `eqMayRewriteFR` fs
-        -- Can the new item rewrite the inert item?
-
-    {-# INLINE kick_out_ct #-}   -- perform case on new_lhs here only once
-    kick_out_ct :: Ct -> Bool
-    -- Kick it out if the new CEqCan can rewrite the inert one
-    -- See Note [kickOutRewritable]
-    kick_out_ct = case new_lhs of
-      TyVarLHS new_tv -> \ct -> let fs@(_,role) = ctFlavourRole ct in
-                                fr_may_rewrite fs
-                             && fr_tv_can_rewrite_ty new_tv role (ctPred ct)
-      TyFamLHS new_tf new_tf_args
-        -> \ct -> let fs@(_, role) = ctFlavourRole ct in
-                  fr_may_rewrite fs
-               && fr_tf_can_rewrite_ty new_tf new_tf_args role (ctPred ct)
-
-    extend_tv_eqs :: InertEqs -> CanEqLHS -> EqualCtList -> InertEqs
-    extend_tv_eqs eqs (TyVarLHS tv) cts = extendDVarEnv eqs tv cts
-    extend_tv_eqs eqs other _cts = pprPanic "extend_tv_eqs" (ppr eqs $$ ppr other)
-
-    extend_fun_eqs :: FunEqMap EqualCtList -> CanEqLHS -> EqualCtList
-                   -> FunEqMap EqualCtList
-    extend_fun_eqs eqs (TyFamLHS fam_tc fam_args) cts
-      = insertTcApp eqs fam_tc fam_args cts
-    extend_fun_eqs eqs other _cts = pprPanic "extend_fun_eqs" (ppr eqs $$ ppr other)
-
-    kick_out_eqs :: (container -> CanEqLHS -> EqualCtList -> container)
-                 -> EqualCtList -> ([Ct], container)
-                 -> ([Ct], container)
-    kick_out_eqs extend eqs (acc_out, acc_in)
-      = (eqs_out `chkAppend` acc_out, case listToEqualCtList eqs_in of
-            Nothing -> acc_in
-            Just eqs_in_ecl@(EqualCtList (eq1 :| _))
-                    -> extend acc_in (cc_lhs eq1) eqs_in_ecl)
-      where
-        (eqs_out, eqs_in) = partition kick_out_eq (equalCtListToList eqs)
-
-    -- Implements criteria K1-K3 in Note [Extending the inert equalities]
-    kick_out_eq (CEqCan { cc_lhs = lhs, cc_rhs = rhs_ty
-                        , cc_ev = ev, cc_eq_rel = eq_rel })
-      | not (fr_may_rewrite fs)
-      = False  -- (K0) Keep it in the inert set if the new thing can't rewrite it
-
-      -- Below here (fr_may_rewrite fs) is True
-
-      | TyVarLHS _ <- lhs
-      , fs `eqMayRewriteFR` new_fr
-      = False  -- (K4) Keep it in the inert set if the LHS is a tyvar and
-               -- it can rewrite the work item. See Note [K4]
-
-      | fr_can_rewrite_ty eq_rel (canEqLHSType lhs)
-      = True   -- (K1)
-         -- The above check redundantly checks the role & flavour,
-         -- but it's very convenient
-
-      | kick_out_for_inertness    = True   -- (K2)
-      | kick_out_for_completeness = True   -- (K3)
-      | otherwise                 = False
-
-      where
-        fs = (ctEvFlavour ev, eq_rel)
-        kick_out_for_inertness
-          =    (fs `eqMayRewriteFR` fs)           -- (K2a)
-            && fr_can_rewrite_ty eq_rel rhs_ty    -- (K2b)
-
-        kick_out_for_completeness  -- (K3) and Note [K3: completeness of solving]
-          = case eq_rel of
-              NomEq  -> rhs_ty `eqType` canEqLHSType new_lhs -- (K3a)
-              ReprEq -> is_can_eq_lhs_head new_lhs rhs_ty    -- (K3b)
-
-    kick_out_eq ct = pprPanic "keep_eq" (ppr ct)
-
-    is_can_eq_lhs_head (TyVarLHS tv) = go
-      where
-        go (Rep.TyVarTy tv')   = tv == tv'
-        go (Rep.AppTy fun _)   = go fun
-        go (Rep.CastTy ty _)   = go ty
-        go (Rep.TyConApp {})   = False
-        go (Rep.LitTy {})      = False
-        go (Rep.ForAllTy {})   = False
-        go (Rep.FunTy {})      = False
-        go (Rep.CoercionTy {}) = False
-    is_can_eq_lhs_head (TyFamLHS fun_tc fun_args) = go
-      where
-        go (Rep.TyVarTy {})       = False
-        go (Rep.AppTy {})         = False  -- no TyConApp to the left of an AppTy
-        go (Rep.CastTy ty _)      = go ty
-        go (Rep.TyConApp tc args) = tcEqTyConApps fun_tc fun_args tc args
-        go (Rep.LitTy {})         = False
-        go (Rep.ForAllTy {})      = False
-        go (Rep.FunTy {})         = False
-        go (Rep.CoercionTy {})    = False
-
 kickOutAfterUnification :: TcTyVar -> TcS Int
 kickOutAfterUnification new_tv
   = do { ics <- getInertCans
@@ -2165,69 +718,6 @@ kickOutAfterFillingCoercionHole hole filled_co
         else Right updated_ct
     kick_ct other = Right other
 
-{- Note [kickOutRewritable]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~
-See also Note [inert_eqs: the inert equalities].
-
-When we add a new inert equality (lhs ~N ty) to the inert set,
-we must kick out any inert items that could be rewritten by the
-new equality, to maintain the inert-set invariants.
-
-  - We want to kick out an existing inert constraint if
-    a) the new constraint can rewrite the inert one
-    b) 'lhs' is free in the inert constraint (so that it *will*)
-       rewrite it if we kick it out.
-
-    For (b) we use anyRewritableCanLHS, which examines the types /and
-    kinds/ that are directly visible in the type. Hence
-    we will have exposed all the rewriting we care about to make the
-    most precise kinds visible for matching classes etc. No need to
-    kick out constraints that mention type variables whose kinds
-    contain this LHS!
-
-  - A Derived equality can kick out [D] constraints in inert_eqs,
-    inert_dicts, inert_irreds etc.
-
-  - We don't kick out constraints from inert_solved_dicts, and
-    inert_solved_funeqs optimistically. But when we lookup we have to
-    take the substitution into account
-
-NB: we could in principle avoid kick-out:
-  a) When unifying a meta-tyvar from an outer level, because
-     then the entire implication will be iterated; see
-     Note [The Unification Level Flag]
-
-  b) For Givens, after a unification.  By (GivenInv) in GHC.Tc.Utils.TcType
-     Note [TcLevel invariants], a Given can't include a meta-tyvar from
-     its own level, so it falls under (a).  Of course, we must still
-     kick out Givens when adding a new non-unification Given.
-
-But kicking out more vigorously may lead to earlier unification and fewer
-iterations, so we don't take advantage of these possibilities.
-
-Note [Rewrite insolubles]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose we have an insoluble alpha ~ [alpha], which is insoluble
-because an occurs check.  And then we unify alpha := [Int].  Then we
-really want to rewrite the insoluble to [Int] ~ [[Int]].  Now it can
-be decomposed.  Otherwise we end up with a "Can't match [Int] ~
-[[Int]]" which is true, but a bit confusing because the outer type
-constructors match.
-
-Hence:
- * In the main simplifier loops in GHC.Tc.Solver (solveWanteds,
-   simpl_loop), we feed the insolubles in solveSimpleWanteds,
-   so that they get rewritten (albeit not solved).
-
- * We kick insolubles out of the inert set, if they can be
-   rewritten (see GHC.Tc.Solver.Monad.kick_out_rewritable)
-
- * We rewrite those insolubles in GHC.Tc.Solver.Canonical.
-   See Note [Make sure that insolubles are fully rewritten]
--}
-
-
-
 --------------
 addInertSafehask :: InertCans -> Ct -> InertCans
 addInertSafehask ics item@(CDictCan { cc_class = cls, cc_tyargs = tys })
@@ -2251,7 +741,7 @@ getSafeOverlapFailures
 --------------
 addSolvedDict :: InstanceWhat -> CtEvidence -> Class -> [Type] -> TcS ()
 -- Conditionally add a new item in the solved set of the monad
--- See Note [Solved dictionaries]
+-- See Note [Solved dictionaries] in GHC.Tc.Solver.InertSet
 addSolvedDict what item cls tys
   | isWanted item
   , instanceReturnsDictCon what
@@ -2434,7 +924,7 @@ getUnsolvedInerts
 getHasGivenEqs :: TcLevel           -- TcLevel of this implication
                -> TcS ( HasGivenEqs -- are there Given equalities?
                       , Cts )       -- Insoluble equalities arising from givens
--- See Note [Tracking Given equalities]
+-- See Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
 getHasGivenEqs tclvl
   = do { inerts@(IC { inert_irreds       = irreds
                     , inert_given_eqs    = given_eqs
@@ -2446,7 +936,7 @@ getHasGivenEqs tclvl
                       -- a local equality; so do /not/ add ct_given_here.
 
              -- See Note [HasGivenEqs] in GHC.Tc.Types.Constraint, and
-             -- Note [Tracking Given equalities] in this module
+             -- Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
              has_ge | ge_lvl == tclvl = MaybeGivenEqs
                     | given_eqs       = LocalGivenEqs
                     | otherwise       = NoGivenEqs
@@ -2459,132 +949,6 @@ getHasGivenEqs tclvl
               , text "Insols:" <+> ppr insols]
        ; return (has_ge, insols) }
 
-mentionsOuterVar :: TcLevel -> CtEvidence -> Bool
-mentionsOuterVar tclvl ev
-  = anyFreeVarsOfType (isOuterTyVar tclvl) $
-    ctEvPred ev
-
-isOuterTyVar :: TcLevel -> TyCoVar -> Bool
--- True of a type variable that comes from a
--- shallower level than the ambient level (tclvl)
-isOuterTyVar tclvl tv
-  | isTyVar tv = assertPpr (not (isTouchableMetaTyVar tclvl tv)) (ppr tv <+> ppr tclvl) $
-                 tclvl `strictlyDeeperThan` tcTyVarLevel tv
-    -- ASSERT: we are dealing with Givens here, and invariant (GivenInv) from
-    -- Note Note [TcLevel invariants] in GHC.Tc.Utils.TcType ensures that there can't
-    -- be a touchable meta tyvar.   If this wasn't true, you might worry that,
-    -- at level 3, a meta-tv alpha[3] gets unified with skolem b[2], and thereby
-    -- becomes "outer" even though its level numbers says it isn't.
-  | otherwise  = False  -- Coercion variables; doesn't much matter
-
--- | Returns Given constraints that might,
--- potentially, match the given pred. This is used when checking to see if a
--- Given might overlap with an instance. See Note [Instance and Given overlap]
--- in "GHC.Tc.Solver.Interact"
-matchableGivens :: CtLoc -> PredType -> InertSet -> Cts
-matchableGivens loc_w pred_w inerts@(IS { inert_cans = inert_cans })
-  = filterBag matchable_given all_relevant_givens
-  where
-    -- just look in class constraints and irreds. matchableGivens does get called
-    -- for ~R constraints, but we don't need to look through equalities, because
-    -- canonical equalities are used for rewriting. We'll only get caught by
-    -- non-canonical -- that is, irreducible -- equalities.
-    all_relevant_givens :: Cts
-    all_relevant_givens
-      | Just (clas, _) <- getClassPredTys_maybe pred_w
-      = findDictsByClass (inert_dicts inert_cans) clas
-        `unionBags` inert_irreds inert_cans
-      | otherwise
-      = inert_irreds inert_cans
-
-    matchable_given :: Ct -> Bool
-    matchable_given ct
-      | CtGiven { ctev_loc = loc_g, ctev_pred = pred_g } <- ctEvidence ct
-      = mightEqualLater inerts pred_g loc_g pred_w loc_w
-
-      | otherwise
-      = False
-
-mightEqualLater :: InertSet -> TcPredType -> CtLoc -> TcPredType -> CtLoc -> Bool
--- See Note [What might equal later?]
--- Used to implement logic in Note [Instance and Given overlap] in GHC.Tc.Solver.Interact
-mightEqualLater (IS { inert_cycle_breakers = cbvs })
-                given_pred given_loc wanted_pred wanted_loc
-  | prohibitedSuperClassSolve given_loc wanted_loc
-  = False
-
-  | otherwise
-  = case tcUnifyTysFG bind_fun [flattened_given] [flattened_wanted] of
-      SurelyApart              -> False  -- types that are surely apart do not equal later
-      MaybeApart MARInfinite _ -> False  -- see Example 7 in the Note.
-      _                        -> True
-
-  where
-    in_scope  = mkInScopeSet $ tyCoVarsOfTypes [given_pred, wanted_pred]
-
-    -- NB: flatten both at the same time, so that we can share mappings
-    -- from type family applications to variables, and also to guarantee
-    -- that the fresh variables are really fresh between the given and
-    -- the wanted. Flattening both at the same time is needed to get
-    -- Example 10 from the Note.
-    ([flattened_given, flattened_wanted], var_mapping)
-      = flattenTysX in_scope [given_pred, wanted_pred]
-
-    bind_fun :: BindFun
-    bind_fun tv rhs_ty
-      | isMetaTyVar tv
-      , can_unify tv (metaTyVarInfo tv) rhs_ty
-         -- this checks for CycleBreakerTvs and TyVarTvs; forgetting
-         -- the latter was #19106.
-      = BindMe
-
-         -- See Examples 4, 5, and 6 from the Note
-      | Just (_fam_tc, fam_args) <- lookupVarEnv var_mapping tv
-      , anyFreeVarsOfTypes mentions_meta_ty_var fam_args
-      = BindMe
-
-      | otherwise
-      = Apart
-
-    -- True for TauTv and TyVarTv (and RuntimeUnkTv) meta-tyvars
-    -- (as they can be unified)
-    -- and also for CycleBreakerTvs that mentions meta-tyvars
-    mentions_meta_ty_var :: TyVar -> Bool
-    mentions_meta_ty_var tv
-      | isMetaTyVar tv
-      = case metaTyVarInfo tv of
-          -- See Examples 8 and 9 in the Note
-          CycleBreakerTv
-            | Just tyfam_app <- lookup tv cbvs
-            -> anyFreeVarsOfType mentions_meta_ty_var tyfam_app
-            | otherwise
-            -> pprPanic "mightEqualLater finds an unbound cbv" (ppr tv $$ ppr cbvs)
-          _ -> True
-      | otherwise
-      = False
-
-    -- like canSolveByUnification, but allows cbv variables to unify
-    can_unify :: TcTyVar -> MetaInfo -> Type -> Bool
-    can_unify _lhs_tv TyVarTv rhs_ty  -- see Example 3 from the Note
-      | Just rhs_tv <- tcGetTyVar_maybe rhs_ty
-      = case tcTyVarDetails rhs_tv of
-          MetaTv { mtv_info = TyVarTv } -> True
-          MetaTv {}                     -> False  -- could unify with anything
-          SkolemTv {}                   -> True
-          RuntimeUnk                    -> True
-      | otherwise  -- not a var on the RHS
-      = False
-    can_unify lhs_tv _other _rhs_ty = mentions_meta_ty_var lhs_tv
-
-prohibitedSuperClassSolve :: CtLoc -> CtLoc -> Bool
--- See Note [Solving superclass constraints] in GHC.Tc.TyCl.Instance
-prohibitedSuperClassSolve from_loc solve_loc
-  | GivenOrigin (InstSC given_size) <- ctLocOrigin from_loc
-  , ScOrigin wanted_size <- ctLocOrigin solve_loc
-  = given_size >= wanted_size
-  | otherwise
-  = False
-
 {- Note [Unsolved Derived equalities]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 In getUnsolvedInerts, we return a derived equality from the inert_eqs
@@ -2777,240 +1141,6 @@ dropFromFamAppCache varset
 foldIrreds :: (Ct -> b -> b) -> Cts -> b -> b
 foldIrreds k irreds z = foldr k z irreds
 
-
-{- *********************************************************************
-*                                                                      *
-                   TcAppMap
-*                                                                      *
-************************************************************************
-
-Note [Use loose types in inert set]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Whenever we are looking up an inert dictionary (CDictCan) or function
-equality (CEqCan), we use a TcAppMap, which uses the Unique of the
-class/type family tycon and then a trie which maps the arguments. This
-trie does *not* need to match the kinds of the arguments; this Note
-explains why.
-
-Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'),
-where ty4 and ty4' have different kinds. Let's further assume that both types
-ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that
-one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth
-argument to T is dependent on whichever one changed). Since we are matching
-all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed
-match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too --
-without ever looking at it.
-
-Accordingly, we use LooseTypeMap, which skips the kind check when looking
-up a type. I (Richard E) believe this is just an optimization, and that
-looking at kinds would be harmless.
-
--}
-
-type TcAppMap a = DTyConEnv (ListMap LooseTypeMap a)
-    -- Indexed by tycon then the arg types, using "loose" matching, where
-    -- we don't require kind equality. This allows, for example, (a |> co)
-    -- to match (a).
-    -- See Note [Use loose types in inert set]
-    -- Used for types and classes; hence UniqDFM
-    -- See Note [foldTM determinism] in GHC.Data.TrieMap for why we use DTyConEnv here
-
-isEmptyTcAppMap :: TcAppMap a -> Bool
-isEmptyTcAppMap m = isEmptyDTyConEnv m
-
-emptyTcAppMap :: TcAppMap a
-emptyTcAppMap = emptyDTyConEnv
-
-findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
-findTcApp m tc tys = do { tys_map <- lookupDTyConEnv m tc
-                        ; lookupTM tys tys_map }
-
-delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
-delTcApp m tc tys = adjustDTyConEnv (deleteTM tys) m tc
-
-insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
-insertTcApp m tc tys ct = alterDTyConEnv alter_tm m tc
-  where
-    alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
-
-alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
-alterTcApp m tc tys upd = alterDTyConEnv alter_tm m tc
-  where
-    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
-    alter_tm m_elt = Just (alterTM tys upd (m_elt `orElse` emptyTM))
-
-filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
-filterTcAppMap f m = mapMaybeDTyConEnv one_tycon m
-  where
-    one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
-    one_tycon tm
-      | isEmptyTM filtered_tm = Nothing
-      | otherwise             = Just filtered_tm
-      where
-        filtered_tm = filterTM f tm
-
-tcAppMapToBag :: TcAppMap a -> Bag a
-tcAppMapToBag m = foldTcAppMap consBag m emptyBag
-
-foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
-foldTcAppMap k m z = foldDTyConEnv (foldTM k) z m
-
-
-{- *********************************************************************
-*                                                                      *
-                   DictMap
-*                                                                      *
-********************************************************************* -}
-
-
-{- Note [Tuples hiding implicit parameters]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Consider
-   f,g :: (?x::Int, C a) => a -> a
-   f v = let ?x = 4 in g v
-
-The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
-We must /not/ solve this from the Given (?x::Int, C a), because of
-the intervening binding for (?x::Int).  #14218.
-
-We deal with this by arranging that we always fail when looking up a
-tuple constraint that hides an implicit parameter. Not that this applies
-  * both to the inert_dicts (lookupInertDict)
-  * and to the solved_dicts (looukpSolvedDict)
-An alternative would be not to extend these sets with such tuple
-constraints, but it seemed more direct to deal with the lookup.
-
-Note [Solving CallStack constraints]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-Suppose f :: HasCallStack => blah.  Then
-
-* Each call to 'f' gives rise to
-    [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
-  with a CtOrigin that says "OccurrenceOf f".
-  Remember that HasCallStack is just shorthand for
-    IP "callStack CallStack
-  See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
-
-* We cannonicalise such constraints, in GHC.Tc.Solver.Canonical.canClassNC, by
-  pushing the call-site info on the stack, and changing the CtOrigin
-  to record that has been done.
-   Bind:  s1 = pushCallStack <site-info> s2
-   [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin
-
-* Then, and only then, we can solve the constraint from an enclosing
-  Given.
-
-So we must be careful /not/ to solve 's1' from the Givens.  Again,
-we ensure this by arranging that findDict always misses when looking
-up souch constraints.
--}
-
-type DictMap a = TcAppMap a
-
-emptyDictMap :: DictMap a
-emptyDictMap = emptyTcAppMap
-
-findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
-findDict m loc cls tys
-  | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters]
-  = Nothing
-
-  | Just {} <- isCallStackPred cls tys
-  , OccurrenceOf {} <- ctLocOrigin loc
-  = Nothing             -- See Note [Solving CallStack constraints]
-
-  | otherwise
-  = findTcApp m (classTyCon cls) tys
-
-findDictsByClass :: DictMap a -> Class -> Bag a
-findDictsByClass m cls
-  | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag
-  | otherwise                                     = emptyBag
-
-delDict :: DictMap a -> Class -> [Type] -> DictMap a
-delDict m cls tys = delTcApp m (classTyCon cls) tys
-
-addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
-addDict m cls tys item = insertTcApp m (classTyCon cls) tys item
-
-addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
--- Like addDict, but combines [W] and [D] to [WD]
--- See Note [KeepBoth] in GHC.Tc.Solver.Interact
-addDictCt m cls tys new_ct = alterTcApp m (classTyCon cls) tys xt_ct
-  where
-    new_ct_ev = ctEvidence new_ct
-
-    xt_ct :: Maybe Ct -> Maybe Ct
-    xt_ct (Just old_ct)
-      | CtWanted { ctev_nosh = WOnly } <- old_ct_ev
-      , CtDerived {} <- new_ct_ev
-      = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }})
-      | CtDerived {} <- old_ct_ev
-      , CtWanted { ctev_nosh = WOnly } <- new_ct_ev
-      = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }})
-      where
-        old_ct_ev = ctEvidence old_ct
-
-    xt_ct _ = Just new_ct
-
-addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
-addDictsByClass m cls items
-  = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items)
-  where
-    add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
-    add ct _ = pprPanic "addDictsByClass" (ppr ct)
-
-filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
-filterDicts f m = filterTcAppMap f m
-
-partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
-partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDicts)
-  where
-    k ct (yeses, noes) | f ct      = (ct `consBag` yeses, noes)
-                       | otherwise = (yeses,              add ct noes)
-    add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
-      = addDict m cls tys ct
-    add ct _ = pprPanic "partitionDicts" (ppr ct)
-
-dictsToBag :: DictMap a -> Bag a
-dictsToBag = tcAppMapToBag
-
-foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
-foldDicts = foldTcAppMap
-
-emptyDicts :: DictMap a
-emptyDicts = emptyTcAppMap
-
-
-{- *********************************************************************
-*                                                                      *
-                   FunEqMap
-*                                                                      *
-********************************************************************* -}
-
-type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
-
-emptyFunEqs :: TcAppMap a
-emptyFunEqs = emptyTcAppMap
-
-findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
-findFunEq m tc tys = findTcApp m tc tys
-
-findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
--- Get inert function equation constraints that have the given tycon
--- in their head.  Not that the constraints remain in the inert set.
--- We use this to check for derived interactions with built-in type-function
--- constructors.
-findFunEqsByTyCon m tc
-  | Just tm <- lookupDTyConEnv m tc = foldTM (:) tm []
-  | otherwise                       = []
-
-foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
-foldFunEqs = foldTcAppMap
-
-insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
-insertFunEq m tc tys val = insertTcApp m tc tys val
-
 {-
 ************************************************************************
 *                                                                      *
@@ -3050,7 +1180,7 @@ data TcSEnv
 
       tcs_inerts    :: IORef InertSet, -- Current inert set
 
-      -- See Note [WorkList priorities] and
+      -- See Note [WorkList priorities] in GHC.Tc.Solver.InertSet
       tcs_worklist  :: IORef WorkList -- Current worklist
     }
 
@@ -3497,6 +1627,24 @@ reportUnifications (TcS thing_inside)
 getDefaultInfo ::  TcS ([Type], (Bool, Bool))
 getDefaultInfo = wrapTcS TcM.tcGetDefaultTys
 
+getWorkList :: TcS WorkList
+getWorkList = do { wl_var <- getTcSWorkListRef
+                 ; wrapTcS (TcM.readTcRef wl_var) }
+
+selectNextWorkItem :: TcS (Maybe Ct)
+-- Pick which work item to do next
+-- See Note [Prioritise equalities]
+selectNextWorkItem
+  = do { wl_var <- getTcSWorkListRef
+       ; wl <- readTcRef wl_var
+       ; case selectWorkItem wl of {
+           Nothing -> return Nothing ;
+           Just (ct, new_wl) ->
+    do { -- checkReductionDepth (ctLoc ct) (ctPred ct)
+         -- This is done by GHC.Tc.Solver.Interact.chooseInstance
+       ; writeTcRef wl_var new_wl
+       ; return (Just ct) } } }
+
 -- Just get some environments needed for instance looking up and matching
 -- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -3936,7 +2084,8 @@ emitNewDerivedEq loc role ty1 ty2
        ; traceTcS "Emitting new derived equality" (ppr ev $$ pprCtLoc loc)
        ; updWorkListTcS (extendWorkListEq (mkNonCanonical ev)) }
          -- Very important: put in the wl_eqs
-         -- See Note [Prioritise equalities] (Avoiding fundep iteration)
+         -- See Note [Prioritise equalities] in GHC.Tc.Solver.InertSet
+         -- (Avoiding fundep iteration)
 
 newDerivedNC :: CtLoc -> TcPredType -> TcS CtEvidence
 newDerivedNC loc pred
@@ -3974,18 +2123,6 @@ matchFamTcM tycon args
                                         , text "Coercion:" <+> ppr co ])
 
 {-
-Note [Residual implications]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-The wl_implics in the WorkList are the residual implication
-constraints that are generated while solving or canonicalising the
-current worklist.  Specifically, when canonicalising
-   (forall a. t1 ~ forall a. t2)
-from which we get the implication
-   (forall a. t1 ~ t2)
-See GHC.Tc.Solver.Monad.deferTcSForAllEq
--}
-
-{-
 ************************************************************************
 *                                                                      *
               Breaking type variable cycles
diff --git a/compiler/GHC/Tc/Solver/Rewrite.hs b/compiler/GHC/Tc/Solver/Rewrite.hs
index 9c0d39ec46..13f6c4ce1b 100644
--- a/compiler/GHC/Tc/Solver/Rewrite.hs
+++ b/compiler/GHC/Tc/Solver/Rewrite.hs
@@ -28,6 +28,7 @@ import GHC.Utils.Outputable
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 import GHC.Tc.Solver.Monad as TcS
+import GHC.Tc.Solver.Types
 
 import GHC.Utils.Misc
 import GHC.Data.Maybe
@@ -333,7 +334,7 @@ it expands the synonym and proceeds; if not, it simply returns the
 unexpanded synonym. See also Note [Rewriting synonyms].
 
 Where do we actually perform rewriting within a type? See Note [Rewritable] in
-GHC.Tc.Solver.Monad.
+GHC.Tc.Solver.InertSet.
 
 Note [rewrite_args performance]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
diff --git a/compiler/GHC/Tc/Solver/Types.hs b/compiler/GHC/Tc/Solver/Types.hs
new file mode 100644
index 0000000000..0ff06e21c1
--- /dev/null
+++ b/compiler/GHC/Tc/Solver/Types.hs
@@ -0,0 +1,328 @@
+{-# LANGUAGE DerivingStrategies #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE PatternSynonyms #-}
+
+{-# OPTIONS_GHC -Wno-incomplete-record-updates #-}
+
+-- | Utility types used within the constraint solver
+module GHC.Tc.Solver.Types (
+    -- Inert CDictCans
+    DictMap, emptyDictMap, findDictsByClass, addDict, addDictCt,
+    addDictsByClass, delDict, foldDicts, filterDicts, findDict,
+    dictsToBag, partitionDicts,
+
+    FunEqMap, emptyFunEqs, foldFunEqs, findFunEq, insertFunEq,
+    findFunEqsByTyCon,
+
+    TcAppMap, isEmptyTcAppMap, insertTcApp, alterTcApp, filterTcAppMap,
+
+    EqualCtList, pattern EqualCtList,
+    equalCtListToList, filterEqualCtList, unitEqualCtList,
+    listToEqualCtList, addToEqualCtList,
+  ) where
+
+import GHC.Prelude
+
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Origin
+import GHC.Tc.Utils.TcType
+
+import GHC.Core.Class
+import GHC.Core.Map.Type
+import GHC.Core.Predicate
+import GHC.Core.TyCon
+import GHC.Core.TyCon.Env
+
+import GHC.Data.Bag
+import GHC.Data.Maybe
+import GHC.Data.TrieMap
+import GHC.Utils.Outputable
+import GHC.Utils.Panic
+
+import Data.Foldable
+import Data.List.NonEmpty ( NonEmpty(..), nonEmpty, cons )
+import qualified Data.List.NonEmpty as NE
+
+{- *********************************************************************
+*                                                                      *
+                   TcAppMap
+*                                                                      *
+************************************************************************
+
+Note [Use loose types in inert set]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Whenever we are looking up an inert dictionary (CDictCan) or function
+equality (CEqCan), we use a TcAppMap, which uses the Unique of the
+class/type family tycon and then a trie which maps the arguments. This
+trie does *not* need to match the kinds of the arguments; this Note
+explains why.
+
+Consider the types ty0 = (T ty1 ty2 ty3 ty4) and ty0' = (T ty1' ty2' ty3' ty4'),
+where ty4 and ty4' have different kinds. Let's further assume that both types
+ty0 and ty0' are well-typed. Because the kind of T is closed, it must be that
+one of the ty1..ty3 does not match ty1'..ty3' (and that the kind of the fourth
+argument to T is dependent on whichever one changed). Since we are matching
+all arguments, during the inert-set lookup, we know that ty1..ty3 do indeed
+match ty1'..ty3'. Therefore, the kind of ty4 and ty4' must match, too --
+without ever looking at it.
+
+Accordingly, we use LooseTypeMap, which skips the kind check when looking
+up a type. I (Richard E) believe this is just an optimization, and that
+looking at kinds would be harmless.
+
+-}
+
+type TcAppMap a = DTyConEnv (ListMap LooseTypeMap a)
+    -- Indexed by tycon then the arg types, using "loose" matching, where
+    -- we don't require kind equality. This allows, for example, (a |> co)
+    -- to match (a).
+    -- See Note [Use loose types in inert set]
+    -- Used for types and classes; hence UniqDFM
+    -- See Note [foldTM determinism] in GHC.Data.TrieMap for why we use DTyConEnv here
+
+isEmptyTcAppMap :: TcAppMap a -> Bool
+isEmptyTcAppMap m = isEmptyDTyConEnv m
+
+emptyTcAppMap :: TcAppMap a
+emptyTcAppMap = emptyDTyConEnv
+
+findTcApp :: TcAppMap a -> TyCon -> [Type] -> Maybe a
+findTcApp m tc tys = do { tys_map <- lookupDTyConEnv m tc
+                        ; lookupTM tys tys_map }
+
+delTcApp :: TcAppMap a -> TyCon -> [Type] -> TcAppMap a
+delTcApp m tc tys = adjustDTyConEnv (deleteTM tys) m tc
+
+insertTcApp :: TcAppMap a -> TyCon -> [Type] -> a -> TcAppMap a
+insertTcApp m tc tys ct = alterDTyConEnv alter_tm m tc
+  where
+    alter_tm mb_tm = Just (insertTM tys ct (mb_tm `orElse` emptyTM))
+
+alterTcApp :: forall a. TcAppMap a -> TyCon -> [Type] -> XT a -> TcAppMap a
+alterTcApp m tc tys upd = alterDTyConEnv alter_tm m tc
+  where
+    alter_tm :: Maybe (ListMap LooseTypeMap a) -> Maybe (ListMap LooseTypeMap a)
+    alter_tm m_elt = Just (alterTM tys upd (m_elt `orElse` emptyTM))
+
+filterTcAppMap :: forall a. (a -> Bool) -> TcAppMap a -> TcAppMap a
+filterTcAppMap f m = mapMaybeDTyConEnv one_tycon m
+  where
+    one_tycon :: ListMap LooseTypeMap a -> Maybe (ListMap LooseTypeMap a)
+    one_tycon tm
+      | isEmptyTM filtered_tm = Nothing
+      | otherwise             = Just filtered_tm
+      where
+        filtered_tm = filterTM f tm
+
+tcAppMapToBag :: TcAppMap a -> Bag a
+tcAppMapToBag m = foldTcAppMap consBag m emptyBag
+
+foldTcAppMap :: (a -> b -> b) -> TcAppMap a -> b -> b
+foldTcAppMap k m z = foldDTyConEnv (foldTM k) z m
+
+{- *********************************************************************
+*                                                                      *
+                   DictMap
+*                                                                      *
+********************************************************************* -}
+
+type DictMap a = TcAppMap a
+
+emptyDictMap :: DictMap a
+emptyDictMap = emptyTcAppMap
+
+findDict :: DictMap a -> CtLoc -> Class -> [Type] -> Maybe a
+findDict m loc cls tys
+  | hasIPSuperClasses cls tys -- See Note [Tuples hiding implicit parameters]
+  = Nothing
+
+  | Just {} <- isCallStackPred cls tys
+  , OccurrenceOf {} <- ctLocOrigin loc
+  = Nothing             -- See Note [Solving CallStack constraints]
+
+  | otherwise
+  = findTcApp m (classTyCon cls) tys
+
+findDictsByClass :: DictMap a -> Class -> Bag a
+findDictsByClass m cls
+  | Just tm <- lookupDTyConEnv m (classTyCon cls) = foldTM consBag tm emptyBag
+  | otherwise                                     = emptyBag
+
+delDict :: DictMap a -> Class -> [Type] -> DictMap a
+delDict m cls tys = delTcApp m (classTyCon cls) tys
+
+addDict :: DictMap a -> Class -> [Type] -> a -> DictMap a
+addDict m cls tys item = insertTcApp m (classTyCon cls) tys item
+
+addDictCt :: DictMap Ct -> Class -> [Type] -> Ct -> DictMap Ct
+-- Like addDict, but combines [W] and [D] to [WD]
+-- See Note [KeepBoth] in GHC.Tc.Solver.Interact
+addDictCt m cls tys new_ct = alterTcApp m (classTyCon cls) tys xt_ct
+  where
+    new_ct_ev = ctEvidence new_ct
+
+    xt_ct :: Maybe Ct -> Maybe Ct
+    xt_ct (Just old_ct)
+      | CtWanted { ctev_nosh = WOnly } <- old_ct_ev
+      , CtDerived {} <- new_ct_ev
+      = Just (old_ct { cc_ev = old_ct_ev { ctev_nosh = WDeriv }})
+      | CtDerived {} <- old_ct_ev
+      , CtWanted { ctev_nosh = WOnly } <- new_ct_ev
+      = Just (new_ct { cc_ev = new_ct_ev { ctev_nosh = WDeriv }})
+      where
+        old_ct_ev = ctEvidence old_ct
+
+    xt_ct _ = Just new_ct
+
+addDictsByClass :: DictMap Ct -> Class -> Bag Ct -> DictMap Ct
+addDictsByClass m cls items
+  = extendDTyConEnv m (classTyCon cls) (foldr add emptyTM items)
+  where
+    add ct@(CDictCan { cc_tyargs = tys }) tm = insertTM tys ct tm
+    add ct _ = pprPanic "addDictsByClass" (ppr ct)
+
+filterDicts :: (Ct -> Bool) -> DictMap Ct -> DictMap Ct
+filterDicts f m = filterTcAppMap f m
+
+partitionDicts :: (Ct -> Bool) -> DictMap Ct -> (Bag Ct, DictMap Ct)
+partitionDicts f m = foldTcAppMap k m (emptyBag, emptyDictMap)
+  where
+    k ct (yeses, noes) | f ct      = (ct `consBag` yeses, noes)
+                       | otherwise = (yeses,              add ct noes)
+    add ct@(CDictCan { cc_class = cls, cc_tyargs = tys }) m
+      = addDict m cls tys ct
+    add ct _ = pprPanic "partitionDicts" (ppr ct)
+
+dictsToBag :: DictMap a -> Bag a
+dictsToBag = tcAppMapToBag
+
+foldDicts :: (a -> b -> b) -> DictMap a -> b -> b
+foldDicts = foldTcAppMap
+
+{- Note [Tuples hiding implicit parameters]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Consider
+   f,g :: (?x::Int, C a) => a -> a
+   f v = let ?x = 4 in g v
+
+The call to 'g' gives rise to a Wanted constraint (?x::Int, C a).
+We must /not/ solve this from the Given (?x::Int, C a), because of
+the intervening binding for (?x::Int).  #14218.
+
+We deal with this by arranging that we always fail when looking up a
+tuple constraint that hides an implicit parameter. Not that this applies
+  * both to the inert_dicts (lookupInertDict)
+  * and to the solved_dicts (looukpSolvedDict)
+An alternative would be not to extend these sets with such tuple
+constraints, but it seemed more direct to deal with the lookup.
+
+Note [Solving CallStack constraints]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Suppose f :: HasCallStack => blah.  Then
+
+* Each call to 'f' gives rise to
+    [W] s1 :: IP "callStack" CallStack    -- CtOrigin = OccurrenceOf f
+  with a CtOrigin that says "OccurrenceOf f".
+  Remember that HasCallStack is just shorthand for
+    IP "callStack CallStack
+  See Note [Overview of implicit CallStacks] in GHC.Tc.Types.Evidence
+
+* We cannonicalise such constraints, in GHC.Tc.Solver.Canonical.canClassNC, by
+  pushing the call-site info on the stack, and changing the CtOrigin
+  to record that has been done.
+   Bind:  s1 = pushCallStack <site-info> s2
+   [W] s2 :: IP "callStack" CallStack   -- CtOrigin = IPOccOrigin
+
+* Then, and only then, we can solve the constraint from an enclosing
+  Given.
+
+So we must be careful /not/ to solve 's1' from the Givens.  Again,
+we ensure this by arranging that findDict always misses when looking
+up souch constraints.
+-}
+
+{- *********************************************************************
+*                                                                      *
+                   FunEqMap
+*                                                                      *
+********************************************************************* -}
+
+type FunEqMap a = TcAppMap a  -- A map whose key is a (TyCon, [Type]) pair
+
+emptyFunEqs :: TcAppMap a
+emptyFunEqs = emptyTcAppMap
+
+findFunEq :: FunEqMap a -> TyCon -> [Type] -> Maybe a
+findFunEq m tc tys = findTcApp m tc tys
+
+findFunEqsByTyCon :: FunEqMap a -> TyCon -> [a]
+-- Get inert function equation constraints that have the given tycon
+-- in their head.  Not that the constraints remain in the inert set.
+-- We use this to check for derived interactions with built-in type-function
+-- constructors.
+findFunEqsByTyCon m tc
+  | Just tm <- lookupDTyConEnv m tc = foldTM (:) tm []
+  | otherwise                       = []
+
+foldFunEqs :: (a -> b -> b) -> FunEqMap a -> b -> b
+foldFunEqs = foldTcAppMap
+
+insertFunEq :: FunEqMap a -> TyCon -> [Type] -> a -> FunEqMap a
+insertFunEq m tc tys val = insertTcApp m tc tys val
+
+{- *********************************************************************
+*                                                                      *
+                   EqualCtList
+*                                                                      *
+********************************************************************* -}
+
+{- Note [EqualCtList invariants]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+    * All are equalities
+    * All these equalities have the same LHS
+    * The list is never empty
+    * No element of the list can rewrite any other
+    * Derived before Wanted
+
+From the fourth invariant it follows that the list is
+   - A single [G], or
+   - Zero or one [D] or [WD], followed by any number of [W]
+
+The Wanteds can't rewrite anything which is why we put them last
+-}
+
+newtype EqualCtList = MkEqualCtList (NonEmpty Ct)
+  deriving newtype Outputable
+  -- See Note [EqualCtList invariants]
+
+-- | Pattern synonym for easy unwrapping. NB: unidirectional to
+-- preserve invariants.
+pattern EqualCtList :: NonEmpty Ct -> EqualCtList
+pattern EqualCtList cts <- MkEqualCtList cts
+{-# COMPLETE EqualCtList #-}
+
+unitEqualCtList :: Ct -> EqualCtList
+unitEqualCtList ct = MkEqualCtList (ct :| [])
+
+addToEqualCtList :: Ct -> EqualCtList -> EqualCtList
+-- NB: This function maintains the "derived-before-wanted" invariant of EqualCtList,
+-- but not the others. See Note [EqualCtList invariants]
+addToEqualCtList ct (MkEqualCtList old_eqs)
+  | isWantedCt ct
+  , eq1 :| eqs <- old_eqs
+  = MkEqualCtList (eq1 :| ct : eqs)
+  | otherwise
+  = MkEqualCtList (ct `cons` old_eqs)
+
+filterEqualCtList :: (Ct -> Bool) -> EqualCtList -> Maybe EqualCtList
+filterEqualCtList pred (MkEqualCtList cts)
+  = fmap MkEqualCtList (nonEmpty $ NE.filter pred cts)
+
+equalCtListToList :: EqualCtList -> [Ct]
+equalCtListToList (MkEqualCtList cts) = toList cts
+
+listToEqualCtList :: [Ct] -> Maybe EqualCtList
+-- NB: This does not maintain invariants other than having the EqualCtList be
+-- non-empty
+listToEqualCtList cts = MkEqualCtList <$> nonEmpty cts
diff --git a/compiler/GHC/Tc/Types/Constraint.hs b/compiler/GHC/Tc/Types/Constraint.hs
index ea4b1b2b86..eebdd8fe2b 100644
--- a/compiler/GHC/Tc/Types/Constraint.hs
+++ b/compiler/GHC/Tc/Types/Constraint.hs
@@ -142,7 +142,7 @@ We thus perform an occurs-check. There is, of course, some subtlety:
 
 The occurs check is performed in GHC.Tc.Utils.Unify.checkTypeEq
 and forms condition T3 in Note [Extending the inert equalities]
-in GHC.Tc.Solver.Monad.
+in GHC.Tc.Solver.InertSet.
 
 -}
 
@@ -192,7 +192,7 @@ data Ct
 
   | CEqCan {  -- CanEqLHS ~ rhs
        -- Invariants:
-       --   * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.Monad
+       --   * See Note [inert_eqs: the inert equalities] in GHC.Tc.Solver.InertSet
        --   * Many are checked in checkTypeEq in GHC.Tc.Utils.Unify
        --   * (TyEq:OC) lhs does not occur in rhs (occurs check)
        --               Note [CEqCan occurs check]
@@ -1190,7 +1190,7 @@ data ImplicStatus
 
 data HasGivenEqs -- See Note [HasGivenEqs]
   = NoGivenEqs      -- Definitely no given equalities,
-                    --   except by Note [Let-bound skolems] in GHC.Tc.Solver.Monad
+                    --   except by Note [Let-bound skolems] in GHC.Tc.Solver.InertSet
   | LocalGivenEqs   -- Might have Given equalities, but only ones that affect only
                     --   local skolems e.g. forall a b. (a ~ F b) => ...
   | MaybeGivenEqs   -- Might have any kind of Given equalities; no floating out
@@ -1202,7 +1202,7 @@ data HasGivenEqs -- See Note [HasGivenEqs]
 The GivenEqs data type describes the Given constraints of an implication constraint:
 
 * NoGivenEqs: definitely no Given equalities, except perhaps let-bound skolems
-  which don't count: see Note [Let-bound skolems] in GHC.Tc.Solver.Monad
+  which don't count: see Note [Let-bound skolems] in GHC.Tc.Solver.InertSet
   Examples: forall a. Eq a => ...
             forall a. (Show a, Num a) => ...
             forall a. a ~ Either Int Bool => ...  -- Let-bound skolem
@@ -1648,7 +1648,7 @@ ctEvFlavour (CtDerived {})                  = Derived
 
 -- | Whether or not one 'Ct' can rewrite another is determined by its
 -- flavour and its equality relation. See also
--- Note [Flavours with roles] in "GHC.Tc.Solver.Monad"
+-- Note [Flavours with roles] in GHC.Tc.Solver.InertSet
 type CtFlavourRole = (CtFlavour, EqRel)
 
 -- | Extract the flavour, role, and boxity from a 'CtEvidence'
@@ -1756,7 +1756,7 @@ should rewrite [D] F alpha ~R T a, we could require splitting the first D
 into [D] F alpha ~NO T alpha, [D] F alpha ~R T alpha. Then, we use the R
 half of the split to rewrite the second D, and off we go. This splitting
 would allow the split-off R equality to be rewritten by other equalities,
-thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.Monad.
+thus avoiding the problem in Note [Why R2?] in GHC.Tc.Solver.InertSet.
 
 This infelicity is #19665 and tested in typecheck/should_compile/T19665
 (marked as expect_broken).
diff --git a/compiler/GHC/Tc/Utils/TcType.hs b/compiler/GHC/Tc/Utils/TcType.hs
index 183fe396ef..1a7e80bd96 100644
--- a/compiler/GHC/Tc/Utils/TcType.hs
+++ b/compiler/GHC/Tc/Utils/TcType.hs
@@ -840,7 +840,7 @@ any_rewritable :: Bool    -- Ignore casts and coercions
 -- role-agnostic, and this one must be role-aware. We could make
 -- foldTyCon role-aware, but that may slow down more common usages.
 --
--- See Note [Rewritable] in GHC.Tc.Solver.Monad for a specification for this function.
+-- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 {-# INLINE any_rewritable #-} -- this allows specialization of predicates
 any_rewritable ignore_cos role tv_pred tc_pred should_expand
   = go role emptyVarSet
@@ -889,7 +889,7 @@ anyRewritableTyVar :: Bool     -- Ignore casts and coercions
                    -> EqRel    -- Ambient role
                    -> (EqRel -> TcTyVar -> Bool)  -- check tyvar
                    -> TcType -> Bool
--- See Note [Rewritable] in GHC.Tc.Solver.Monad for a specification for this function.
+-- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 anyRewritableTyVar ignore_cos role pred
   = any_rewritable ignore_cos role pred
       (\ _ _ _ -> False) -- no special check for tyconapps
@@ -906,14 +906,14 @@ anyRewritableTyFamApp :: EqRel   -- Ambient role
                           -- should return True only for type family applications
                       -> TcType -> Bool
   -- always ignores casts & coercions
--- See Note [Rewritable] in GHC.Tc.Solver.Monad for a specification for this function.
+-- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 anyRewritableTyFamApp role check_tyconapp
   = any_rewritable True role (\ _ _ -> False) check_tyconapp (not . isFamFreeTyCon)
 
 -- This version is used by shouldSplitWD. It *does* look in casts
 -- and coercions, and it always expands type synonyms whose RHSs mention
 -- type families.
--- See Note [Rewritable] in GHC.Tc.Solver.Monad for a specification for this function.
+-- See Note [Rewritable] in GHC.Tc.Solver.InertSet for a specification for this function.
 anyRewritableCanEqLHS :: EqRel   -- Ambient role
                       -> (EqRel -> TcTyVar -> Bool)            -- check tyvar
                       -> (EqRel -> TyCon -> [TcType] -> Bool)  -- check type family
diff --git a/compiler/GHC/Tc/Utils/Unify.hs b/compiler/GHC/Tc/Utils/Unify.hs
index 5a4fe715c6..0ad43fe32e 100644
--- a/compiler/GHC/Tc/Utils/Unify.hs
+++ b/compiler/GHC/Tc/Utils/Unify.hs
@@ -1566,7 +1566,7 @@ There are three reasons not to unify:
    between levels 'n' and 'l'.
 
    Exactly what is a "given equality" for the purpose of (UNTOUCHABLE)?
-   Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.Monad
+   Answer: see Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
 
 3. (TYVAR-TV) Unifying TyVarTvs and CycleBreakerTvs
    This precondition looks at the MetaInfo of the unification variable:
@@ -1608,7 +1608,7 @@ Needless to say, all three have wrinkles:
 
   * In the constraint solver, we track where Given equalities occur
     and use that to guard unification in GHC.Tc.Solver.Canonical.unifyTest
-    More details in Note [Tracking Given equalities] in GHC.Tc.Solver.Monad
+    More details in Note [Tracking Given equalities] in GHC.Tc.Solver.InertSet
 
     Historical note: in the olden days (pre 2021) the constraint solver
     also used to unify only if l=n.  Equalities were "floated" out of the
@@ -1704,7 +1704,7 @@ Wanteds and Givens, but either way, deepest wins!  Simple.
   Otherwise it can't.  By putting the deepest variable on the left
   we maximise our changes of eliminating skolem capture.
 
-  See also GHC.Tc.Solver.Monad Note [Let-bound skolems] for another reason
+  See also GHC.Tc.Solver.InertSet Note [Let-bound skolems] for another reason
   to orient with the deepest skolem on the left.
 
   IMPORTANT NOTE: this test does a level-number comparison on
diff --git a/compiler/ghc.cabal.in b/compiler/ghc.cabal.in
index 29762bd79f..d595e26fb2 100644
--- a/compiler/ghc.cabal.in
+++ b/compiler/ghc.cabal.in
@@ -604,8 +604,10 @@ Library
         GHC.Tc.Solver
         GHC.Tc.Solver.Canonical
         GHC.Tc.Solver.Rewrite
+        GHC.Tc.Solver.InertSet
         GHC.Tc.Solver.Interact
         GHC.Tc.Solver.Monad
+        GHC.Tc.Solver.Types
         GHC.Tc.TyCl
         GHC.Tc.TyCl.Build
         GHC.Tc.TyCl.Class