+             (suppress, m_evdest) = case ctEvidence ct of

+                   -- For this `suppress` stuff

+                   -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint

+                     CtGiven {} -> (False, Nothing)

+                     CtWanted (WantedCt { ctev_rewriters = rws, ctev_dest = dest })

+                                -> (not (isEmptyRewriterSet rws), Just dest)

+         -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty

+       ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds

+                                                      , ppr proposalSequences

+                                                      , ppr successes ])

+     solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out

+     To do this, we slightly-hackily use the `ctev_rewriters` field of the inert,

+     which records that `w` has been rewritten by `kw`.

+     See (WRW3) in Note [Wanteds reewrite Wanteds] in GHC.Tc.Types.Constraint.

+

+   See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint. 

+        -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality

+         -- in GHC.Tc.Types.Constraint wrinkle (PER1)

+       ; cts <- liftZonkTcS $ mapBagM TcM.zonkCtRewriterSet cts

+            ; rewriters   <- TcM.liftZonkM (TcM.zonkRewriterSet (ctEvRewriters ev))

+and that can be used to rewrite other constraints. It satisfies these invariants:

+* We allow Wanteds to rewrite Wanteds, but each Wanted tracks the set of Wanteds

+  it has been rewritten by, in its RewriterSet, stored in the ctev_rewriters

+  field of the CtWanted constructor of CtEvidence.  (Only Wanteds have

+  RewriterSets.)

+* A RewriterSet is just a set of unfilled CoercionHoles. This is sufficient

+  because only equalities (evidenced by coercion holes) are used for rewriting;

+  other (dictionary) constraints cannot ever rewrite.

+

+* The rewriter (in e.g. GHC.Tc.Solver.Rewrite.rewrite) tracks and returns a RewriterSet,

+  consisting of the evidence (a CoercionHole) for any Wanted equalities used in

+  rewriting.

+

+* Then GHC.Tc.Solver.Solve.rewriteEvidence and GHC.Tc.Solver.Equality.rewriteEqEvidence

+  add this RewriterSet to the rewritten constraint's rewriter set.

+  which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled

+* In error reporting, we prioritise Wanteds that have an empty RewriterSet:

+Wrinkles:

+

+(WRW1) When we find a constraint identical to one already in the inert set,

+   we solve one from the other. Other things being equal, keep the one

+   that has fewer (better still no) rewriters.

+   See (CE4) in Note [Combining equalities] in GHC.Tc.Solver.Equality.

+

+   To this accurately we should use `zonkRewriterSet` during canonicalisation,

+   to eliminate rewriters that have now been solved.  Currently we only do so

+   during error reporting; but perhaps we should change that.

+

+(WRW2) When zonk a constraint (with `zonkCt` and `zonkCtEvidence`) we take

+   the opportunity to zonk its `RewriterSet, which eliminates solved ones`.

+   This doesn't guarantee that rewriter sets are always up to date -- see

+   (WRW1) -- but it helps, and it de-clutters debug output.

+

+(WRW3) We use the rewriter set for a slightly different purpose, in (EIK2)

+   of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality.

+   This is a bit of a hack.

+we prioritise constraints that have no rewriters. Here's why.

+(PER1) Before checking for an empty RewriterSet, we zonk the RewriterSet,

+(PER2) Despite the prioritisation, it is hard to be /certain/ that we can't end up

+      = do m_co <- liftZonkM (unpackCoercionHole_maybe hole)

+{-# LANGUAGE DuplicateRecordFields #-}

+

+    -- * Rewriter sets

+  , zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet

+

+    -- * Coercion holes

+  , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe

+

+

+import GHC.Utils.Outputable as Outputable

+import Data.Semigroup

+import Data.Maybe

+

+                    ppr cv Outputable.<> colon

+                    <+> vcat [ ppr t1, ppr t2, ppr role, ppr cv_ty ])

+-- Zonks the ctev_pred and the ctev_rewriters; but not ctev_evar

+-- For ctev_rewriters, see (WRW2) in Note [Wanteds rewrite Wanteds]

+zonkCtEvidence (CtGiven (GivenCt { ctev_pred = pred, ctev_evar = var, ctev_loc = loc }))

+  = do { pred' <- zonkTcType pred

+       ; return (CtGiven (GivenCt { ctev_pred = pred', ctev_evar = var, ctev_loc = loc })) }

+zonkCtEvidence (CtWanted wanted@(WantedCt { ctev_pred = pred, ctev_rewriters = rws }))

+  = do { pred' <- zonkTcType pred

+       ; rws'  <- zonkRewriterSet rws

+       ; return (CtWanted (wanted { ctev_pred = pred', ctev_rewriters = rws' })) }

+%************************************************************************

+%*                                                                      *

+                 Zonking rewriter sets

+*                                                                      *

+************************************************************************

+-}

+

+zonkCtRewriterSet :: Ct -> ZonkM Ct

+zonkCtRewriterSet ct

+  | isGivenCt ct

+  = return ct

+  | otherwise

+  = case ct of

+      CEqCan eq@(EqCt { eq_ev = ev })       -> do { ev' <- zonkCtEvRewriterSet ev

+                                                  ; return (CEqCan (eq { eq_ev = ev' })) }

+      CIrredCan ir@(IrredCt { ir_ev = ev }) -> do { ev' <- zonkCtEvRewriterSet ev

+                                                  ; return (CIrredCan (ir { ir_ev = ev' })) }

+      CDictCan di@(DictCt { di_ev = ev })   -> do { ev' <- zonkCtEvRewriterSet ev

+                                                  ; return (CDictCan (di { di_ev = ev' })) }

+      CQuantCan {}     -> return ct

+      CNonCanonical ev -> do { ev' <- zonkCtEvRewriterSet ev

+                             ; return (CNonCanonical ev') }

+

+zonkCtEvRewriterSet :: CtEvidence -> ZonkM CtEvidence

+zonkCtEvRewriterSet ev@(CtGiven {})

+  = return ev

+zonkCtEvRewriterSet ev@(CtWanted wtd)

+  = do { rewriters' <- zonkRewriterSet (ctEvRewriters ev)

+       ; return (CtWanted $ setWantedCtEvRewriters wtd rewriters') }

+

+-- | Check whether any coercion hole in a RewriterSet is still unsolved.

+-- Does this by recursively looking through filled coercion holes until

+-- one is found that is not yet filled in, at which point this aborts.

+zonkRewriterSet :: RewriterSet -> ZonkM RewriterSet

+zonkRewriterSet (RewriterSet set)

+  = nonDetStrictFoldUniqSet go (return emptyRewriterSet) set

+     -- this does not introduce non-determinism, because the only

+     -- monadic action is to read, and the combining function is

+     -- commutative

+  where

+    go :: CoercionHole -> ZonkM RewriterSet -> ZonkM RewriterSet

+    go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc

+

+    check_hole :: CoercionHole -> ZonkM RewriterSet

+    check_hole hole = do { m_co <- unpackCoercionHole_maybe hole

+                         ; case m_co of

+                             Nothing -> return (unitRewriterSet hole)

+                             Just co -> unUCHM (check_co co) }

+

+    check_ty :: Type -> UnfilledCoercionHoleMonoid

+    check_co :: Coercion -> UnfilledCoercionHoleMonoid

+    (check_ty, _, check_co, _) = foldTyCo folder ()

+

+    folder :: TyCoFolder () UnfilledCoercionHoleMonoid

+    folder = TyCoFolder { tcf_view  = noView

+                        , tcf_tyvar = \ _ tv -> check_ty (tyVarKind tv)

+                        , tcf_covar = \ _ cv -> check_ty (varType cv)

+                        , tcf_hole  = \ _ -> UCHM . check_hole

+                        , tcf_tycobinder = \ _ _ _ -> () }

+

+newtype UnfilledCoercionHoleMonoid = UCHM { unUCHM :: ZonkM RewriterSet }

+

+instance Semigroup UnfilledCoercionHoleMonoid where

+  UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r)

+

+instance Monoid UnfilledCoercionHoleMonoid where

+  mempty = UCHM (return emptyRewriterSet)

+

+

+{-

+************************************************************************

+*                                                                      *

+             Checking for coercion holes

+*                                                                      *

+************************************************************************

+-}

+

+-- | Is a coercion hole filled in?

+isFilledCoercionHole :: CoercionHole -> ZonkM Bool

+isFilledCoercionHole (CoercionHole { ch_ref = ref })

+  = isJust <$> readTcRef ref

+

+-- | Retrieve the contents of a coercion hole. Panics if the hole

+-- is unfilled

+unpackCoercionHole :: CoercionHole -> ZonkM Coercion

+unpackCoercionHole hole

+  = do { contents <- unpackCoercionHole_maybe hole

+       ; case contents of

+           Just co -> return co

+           Nothing -> pprPanic "Unfilled coercion hole" (ppr hole) }

+

+-- | Retrieve the contents of a coercion hole, if it is filled

+unpackCoercionHole_maybe :: CoercionHole -> ZonkM (Maybe Coercion)

+unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref

+

+

+{-

+T3330c.hs:25:38: error: [GHC-25897]

+    • Could not deduce ‘Der f1 ~ f1’

+      from the context: f ~ (f1 :+: g)

+        bound by a pattern with constructor:

+                   RSum :: forall (f :: * -> *) (g :: * -> *).

+                           R f -> R g -> R (f :+: g),

+                 in an equation for ‘plug'’

+        at T3330c.hs:25:8-17

+      Expected: x -> f1 x

+        Actual: x -> Der f1 x

+      ‘f1’ is a rigid type variable bound by

+        a pattern with constructor:

+          RSum :: forall (f :: * -> *) (g :: * -> *).

+                  R f -> R g -> R (f :+: g),

+        in an equation for ‘plug'’

+        at T3330c.hs:25:8-17

+    • The function ‘plug’ is applied to three visible arguments,

+        but its type ‘Rep f => Der f x -> x -> f x’ has only two

+

+T4174.hs:45:12: error: [GHC-25897]

+    • Couldn't match type ‘a’ with ‘SmStep’

+      Expected: m (Field (Way (GHC6'8 minor) n t p) a b)

+        Actual: m (Field (WayOf m) SmStep RtsSpinLock)

+      ‘a’ is a rigid type variable bound by

+        the type signature for:

+          testcase :: forall (m :: * -> *) minor n t p a b.

+                      Monad m =>

+                      m (Field (Way (GHC6'8 minor) n t p) a b)

+        at T4174.hs:44:1-63

+    • Relevant bindings include

+        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)

+          (bound at T4174.hs:45:1)

+

+    • Couldn't match type ‘Bool’ with ‘B’

+        arising from a superclass required to satisfy ‘C Int B’,

+