GitLab

Marge Bot pushed to branch master at Glasgow Haskell Compiler / GHC

Commits:

22d11fa8

by Simon Peyton Jones at 2025-04-28T18:05:19-04:00

Track rewriter sets more accurately in constraint solving

The key change, which fixed #25440, is to call `recordRewriter` in
GHC.Tc.Solver.Rewrite.rewrite_exact_fam_app.  This missing call meant
that we were secretly rewriting a Wanted with a Wanted, but not really
noticing; and that led to a very bad error message, as you can see
in the ticket.

But of course that led me into rabbit hole of other refactoring around
the RewriteSet code:

* Improve Notes [Wanteds rewrite Wanteds]

* Zonk the RewriterSet in `zonkCtEvidence` rather than only in GHC.Tc.Errors.
  This is tidier anyway (e.g. de-clutters debug output), and helps with the
  next point.

* In GHC.Tc.Solver.Equality.inertsCanDischarge, don't replace a constraint
  with no rewriters with an equal constraint that has many. See
  See (CE4) in Note [Combining equalities]

* Move zonkRewriterSet and friends from GHC.Tc.Zonk.Type into
  GHC.Tc.Zonk.TcType, where they properly belong.

A handful of tests get better error messages.

For some reason T24984 gets 12% less compiler allocation -- good

Metric Decrease:
    T24984

16 changed files:

compiler/GHC/Core/Coercion.hs
compiler/GHC/Tc/Errors.hs
compiler/GHC/Tc/Solver/Default.hs
compiler/GHC/Tc/Solver/Equality.hs
compiler/GHC/Tc/Solver/Monad.hs
compiler/GHC/Tc/Solver/Rewrite.hs
compiler/GHC/Tc/Types/Constraint.hs
compiler/GHC/Tc/Utils/TcMType.hs
compiler/GHC/Tc/Utils/Unify.hs
compiler/GHC/Tc/Zonk/TcType.hs
compiler/GHC/Tc/Zonk/Type.hs
testsuite/tests/indexed-types/should_fail/T3330c.stderr
testsuite/tests/indexed-types/should_fail/T4174.stderr
testsuite/tests/indexed-types/should_fail/T8227.stderr
testsuite/tests/typecheck/should_compile/T25266a.stderr
testsuite/tests/typecheck/should_fail/T18851.stderr

Changes:

compiler/GHC/Core/Coercion.hs

@@ -120,7 +120,8 @@ module GHC.Core.Coercion (
          multToCo, mkRuntimeRepCo,
 -        hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,
 +        hasHeteroKindCoercionHoleTy, hasHeteroKindCoercionHoleCo,
 +        hasThisCoercionHoleTy,
          setCoHoleType
         ) where
@@ -2795,12 +2796,12 @@ has_co_hole_co :: Coercion -> Monoid.Any
  -- | Is there a hetero-kind coercion hole in this type?
  --   (That is, a coercion hole with ch_hetero_kind=True.)
  -- See wrinkle (EIK2) of Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
 -hasCoercionHoleTy :: Type -> Bool
 -hasCoercionHoleTy = Monoid.getAny . has_co_hole_ty
 +hasHeteroKindCoercionHoleTy :: Type -> Bool
 +hasHeteroKindCoercionHoleTy = Monoid.getAny . has_co_hole_ty
  -- | Is there a hetero-kind coercion hole in this coercion?
 -hasCoercionHoleCo :: Coercion -> Bool
 -hasCoercionHoleCo = Monoid.getAny . has_co_hole_co
 +hasHeteroKindCoercionHoleCo :: Coercion -> Bool
 +hasHeteroKindCoercionHoleCo = Monoid.getAny . has_co_hole_co
  hasThisCoercionHoleTy :: Type -> CoercionHole -> Bool
  hasThisCoercionHoleTy ty hole = Monoid.getAny (f ty)

compiler/GHC/Tc/Errors.hs

@@ -466,13 +466,12 @@ mkErrorItem ct
    = do { let loc = ctLoc ct
               flav = ctFlavour ct
 -       ; (suppress, m_evdest) <- case ctEvidence ct of
 -         -- For this `suppress` stuff
 -         -- see Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
 -           CtGiven {} -> return (False, Nothing)
 -           CtWanted (WantedCt { ctev_rewriters = rewriters, ctev_dest = dest })
 -             -> do { rewriters' <- zonkRewriterSet rewriters
 -                   ; return (not (isEmptyRewriterSet rewriters'), Just dest) }
 +             (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)
         ; let m_reason = case ct of
                  CIrredCan (IrredCt { ir_reason = reason }) -> Just reason
@@ -503,7 +502,7 @@ reportWanteds ctxt tc_lvl wc@(WC { wc_simple = simples, wc_impl = implics
                                           , text "tidy_errs =" <+> ppr tidy_errs ])
           -- Catch an awkward (and probably rare) case in which /all/ errors are
 -         -- suppressed: see Wrinkle (WRW2) in Note [Prioritise Wanteds with empty
 +         -- suppressed: see Wrinkle (PER2) in Note [Prioritise Wanteds with empty
           -- RewriterSet] in GHC.Tc.Types.Constraint.
           --
           -- Unless we are sure that an error will be reported some other way
@@ -1821,7 +1820,7 @@ mkTyVarEqErr' ctxt item (tv1, co1) ty2
    -- Incompatible kinds
    -- This is wrinkle (EIK2) in Note [Equalities with incompatible kinds]
    -- in GHC.Tc.Solver.Equality
 -  | hasCoercionHoleCo co1 || hasCoercionHoleTy ty2
 +  | hasHeteroKindCoercionHoleCo co1 || hasHeteroKindCoercionHoleTy ty2
    = return $ mkBlockedEqErr item
    | isSkolemTyVar tv1  -- ty2 won't be a meta-tyvar; we would have

compiler/GHC/Tc/Solver/Default.hs

@@ -1081,9 +1081,9 @@ disambigProposalSequences orig_wanteds wanteds proposalSequences allConsistent
         ; successes <- fmap catMaybes $
                        nestImplicTcS fake_ev_binds_var (pushTcLevel tclvl) $
                        mapM firstSuccess proposalSequences
 -       ; traceTcS "disambigProposalSequences" (vcat [ ppr wanteds
 -                                                    , ppr proposalSequences
 -                                                    , ppr successes ])
 +       ; traceTcS "disambigProposalSequences {" (vcat [ ppr wanteds
 +                                                      , ppr proposalSequences
 +                                                      , ppr successes ])
         -- Step (4) in Note [How type-class constraints are defaulted]
         ; case successes of
             success@(tvs, subst) : rest

compiler/GHC/Tc/Solver/Equality.hs

@@ -1613,54 +1613,63 @@ canEqCanLHSHetero ev eq_rel swapped lhs1 ps_xi1 ki1 xi2 ps_xi2 ki2
  --    NotSwapped:
  --        ev      :: (lhs1:ki1) ~r# (xi2:ki2)
  --        kind_co :: k11 ~# ki2               -- Same orientation as ev
 ---        type_ev :: lhs1 ~r# (xi2 |> sym kind_co)
 +--        new_ev  :: lhs1 ~r# (xi2 |> sym kind_co)
  --    Swapped
  --        ev      :: (xi2:ki2) ~r# (lhs1:ki1)
  --        kind_co :: ki2 ~# ki1               -- Same orientation as ev
 ---        type_ev :: (xi2 |> kind_co) ~r# lhs1
 +--        new_ev  :: (xi2 |> kind_co) ~r# lhs1
 +-- Note that we need the `sym` when we are /not/ swapped; hence `mk_sym_co`
 -  = do { (kind_co, rewriters, unifs_happened) <- mk_kind_eq   -- :: ki1 ~N ki2
 -       ; if unifs_happened
 -              -- Unifications happened, so start again to do the zonking
 -              -- Otherwise we might put something in the inert set that isn't inert
 -         then startAgainWith (mkNonCanonical ev)
 -         else
 -    do { let lhs_redn = mkReflRedn role ps_xi1
 -             rhs_redn = mkGReflRightRedn role xi2 mb_sym_kind_co
 -             mb_sym_kind_co = case swapped of
 -                                NotSwapped -> mkSymCo kind_co
 -                                IsSwapped  -> kind_co
+-
 -       ; traceTcS "Hetero equality gives rise to kind equality"
 -           (ppr swapped $$
 -            ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
 -       ; type_ev <- rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn
+-
 -       ; let new_xi2 = mkCastTy ps_xi2 mb_sym_kind_co
 -       ; canEqCanLHSHomo type_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }}
+-
 -  where
 -    mk_kind_eq :: TcS (CoercionN, RewriterSet, Bool)
 -    -- Returned kind_co has kind (k1 ~ k2) if NotSwapped, (k2 ~ k1) if Swapped
 -    -- Returned Bool = True if unifications happened, so we should retry
 -    mk_kind_eq = case ev of
 +  = case ev of
        CtGiven (GivenCt { ctev_evar = evar, ctev_loc = loc })
          -> do { let kind_co  = mkKindCo (mkCoVarCo evar)
                      pred_ty  = unSwap swapped mkNomEqPred ki1 ki2
                      kind_loc = mkKindEqLoc xi1 xi2 loc
                ; kind_ev <- newGivenEvVar kind_loc (pred_ty, evCoercion kind_co)
                ; emitWorkNC [CtGiven kind_ev]
 -              ; return (givenCtEvCoercion kind_ev, emptyRewriterSet, False) }
 +              ; let kind_co = givenCtEvCoercion kind_ev
 +                    new_xi2 = mkCastTy ps_xi2 (mk_sym_co kind_co)
 +              ; new_ev <- do_rewrite emptyRewriterSet kind_co
 +                -- In the Given case, `new_ev` is canonical, so carry on
 +              ; canEqCanLHSHomo new_ev eq_rel NotSwapped lhs1 ps_xi1 new_xi2 new_xi2 }
        CtWanted {}
 -        -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
 -                                         let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
 -                                         in unSwap swapped (uType uenv') ki1 ki2
 -              ; return (kind_co, rewriterSetFromCts cts, not (null unifs)) }
+-
 +         -> do { (kind_co, cts, unifs) <- wrapUnifierTcS ev Nominal $ \uenv ->
 +                                          let uenv' = updUEnvLoc uenv (mkKindEqLoc xi1 xi2)
 +                                          in unSwap swapped (uType uenv') ki1 ki2
 +               ; if not (null unifs)
 +                 then -- Unifications happened, so start again to do the zonking
 +                      -- Otherwise we might put something in the inert set that isn't inert
 +                      startAgainWith (mkNonCanonical ev)
 +                 else
++
 +            assertPpr (not (isEmptyCts cts)) (ppr ev $$ ppr ki1 $$ ppr ki2) $
 +              -- The constraints won't be empty because the two kinds differ, and there
 +              -- are no unifications, so we must have emitted one or more constraints
 +            do { new_ev <- do_rewrite (rewriterSetFromCts cts) kind_co
 +                 -- The rewritten equality `new_ev` is non-canonical,
 +                 -- so put it straight in the Irreds
 +               ; finishCanWithIrred (NonCanonicalReason (cteProblem cteCoercionHole)) new_ev } }
 +  where
      xi1  = canEqLHSType lhs1
      role = eqRelRole eq_rel
 +    -- Apply mkSymCo when /not/ swapped
 +    mk_sym_co co = case swapped of
 +                      NotSwapped -> mkSymCo co
 +                      IsSwapped  -> co
++
 +    do_rewrite rewriters kind_co
 +      = do { traceTcS "Hetero equality gives rise to kind equality"
 +                 (ppr swapped $$
 +                  ppr kind_co <+> dcolon <+> sep [ ppr ki1, text "~#", ppr ki2 ])
 +           ; rewriteEqEvidence rewriters ev swapped lhs_redn rhs_redn }
 +      where
 +        -- kind_co :: ki1 ~N ki2
 +        lhs_redn    = mkReflRedn role ps_xi1
 +        rhs_redn    = mkGReflRightRedn role xi2 (mk_sym_co kind_co)
++
++
  canEqCanLHSHomo :: CtEvidence          -- lhs ~ rhs
                                         -- or, if swapped: rhs ~ lhs
                  -> EqRel -> SwapFlag
@@ -2044,19 +2053,20 @@ What do we do when we have an equality
  where k1 and k2 differ? Easy: we create a coercion that relates k1 and
  k2 and use this to cast. To wit, from
 -  [X] (tv :: k1) ~ (rhs :: k2)
 +  [X] co1 :: (tv :: k1) ~ (rhs :: k2)
  (where [X] is [G] or [W]), we go to
 -  [X] co :: k1 ~ k2
 -  [X] (tv :: k1) ~ ((rhs |> sym co) :: k1)
 +  co1 = co2 ; sym (GRefl kco)
 +  [X] co2 :: (tv :: k1) ~ ((rhs |> sym kco) :: k1)
 +  [X] kco :: k1 ~ k2
  Wrinkles:
 -(EIK1) When X is W, the new type-level wanted is effectively rewritten by the
 -     kind-level one. We thus include the kind-level wanted in the RewriterSet
 -     for the type-level one. See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
 -     This is done in canEqCanLHSHetero.
 +(EIK1) When X=Wanted, the new type-level wanted for `co` is effectively rewritten by
 +     the kind-level one. We thus include the kind-level wanted in the RewriterSet
 +     for the type-level one. See Note [Wanteds rewrite Wanteds] in
 +     GHC.Tc.Types.Constraint.  This is done in canEqCanLHSHetero.
  (EIK2) Suppose we have [W] (a::Type) ~ (b::Type->Type). The above rewrite will produce
          [W] w  : a ~ (b |> kw)
@@ -2076,13 +2086,17 @@ Wrinkles:
       Instead, it lands in the inert_irreds in the inert set, awaiting solution of
       that `kw`.
 -     (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets
 -     solved. This is done in kickOutAfterFillingCoercionHole, which kicks out
 +  (EIK2a) We must later indeed unify if/when the kind-level wanted, `kw` gets
 +     solved. This is done in `kickOutAfterFillingCoercionHole`, which kicks out
       all equalities whose RHS mentions the filled-in coercion hole.  Note that
       it looks for type family equalities, too, because of the use of unifyTest
       in canEqTyVarFunEq.
 -     (EIK2b) What if the RHS mentions /other/ coercion holes?  How can that happen?  The
 +     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 rewrite Wanteds] in GHC.Tc.Types.Constraint.
++
 +  (EIK2b) What if the RHS mentions /other/ coercion holes?  How can that happen?  The
       main way is like this. Assume F :: forall k. k -> Type
          [W] kw : k  ~ Type
          [W] w  : a ~ F k t
@@ -2093,15 +2107,32 @@ Wrinkles:
       rewriting. Indeed tests JuanLopez only typechecks if we do.  So we'd like to treat
       this kind of equality as canonical.
 -     Hence the ch_hetero_kind field in CoercionHole: it is True of constraints
 -     created by `canEqCanLHSHetero` to fix up hetero-kinded equalities; and False otherwise:
 +  So here is our implementation:
 +     * The `ch_hetero_kind` field in CoercionHole identifies a coercion hole created
 +       by `canEqCanLHSHetero` to fix up hetero-kinded equalities.
++
 +     * An equality constraint is non-canonical if it mentions a /hetero-kind/
 +       CoercionHole on the RHS.  This (and only this) is the (TyEq:CH) invariant
 +       for canonical equalities (see Note [Canonical equalities])
++
 +     * The invariant is checked by the `hasHeterKindCoercionHoleCo` test in
 +       GHC.Tc.Utils.Unify.checkCo; and not satisfying this invariant is what
 +       `cteCoercionHole` in `CheckTyEqResult` means.
 -     * An equality constraint is non-canonical if it mentions a hetero-kind
 -       CoercionHole on the RHS.  See the `hasCoercionHoleCo` test in GHC.Tc.Utils.checkCo.
 +     * These special hetero-kind CoercionHoles are created by the `uType` unifier when
 +       the parent's CtOrigin is KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole
 +       and friends.
 -     * Hetero-kind CoercionHoles are created when the parent's CtOrigin is
 -       KindEqOrigin: see GHC.Tc.Utils.TcMType.newCoercionHole and friends.  We
 -       set this origin, via `mkKindLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`.
 +       We set this origin, via `updUEnvLoc`, in `mk_kind_eq` in `canEqCanLHSHetero`.
++
 +     * We /also/ add the coercion hole to the `RewriterSet` of the constraint,
 +       in `canEqCanLHSHetero`
++
 +     * When filling one of these special hetero-kind coercion holes, we kick out
 +       any IrredCt's that mention this hole; maybe it is now canonical.
 +       See `kickOutAfterFillingCoercionHole`.
++
 +     Gah!  This is bizarrely complicated.
  (EIK3) Suppose we have [W] (a :: k1) ~ (rhs :: k2). We duly follow the
       algorithm detailed here, producing [W] co :: k1 ~ k2, and adding
@@ -2576,17 +2607,17 @@ Suppose we have
  Then we can simply solve g2 from g1, thus g2 := g1.  Easy!
  But it's not so simple:
 -* If t is a type variable, the equalties might be oriented differently:
 +(CE1) If t is a type variable, the equalties might be oriented differently:
        e.g. (g1 :: a~b) and (g2 :: b~a)
    So we look both ways round.  Hence the SwapFlag result to
    inertsCanDischarge.
 -* We can only do g2 := g1 if g1 can discharge g2; that depends on
 +(CE2) We can only do g2 := g1 if g1 can discharge g2; that depends on
    (a) the role and (b) the flavour.  E.g. a representational equality
    cannot discharge a nominal one; a Wanted cannot discharge a Given.
    The predicate is eqCanRewriteFR.
 -* Visibility. Suppose  S :: forall k. k -> Type, and consider unifying
 +(CE3) Visibility. Suppose  S :: forall k. k -> Type, and consider unifying
        S @Type (a::Type)  ~   S @(Type->Type) (b::Type->Type)
    From the first argument we get (Type ~ Type->Type); from the second
    argument we get (a ~ b) which in turn gives (Type ~ Type->Type).
@@ -2601,6 +2632,24 @@ But it's not so simple:
    So when combining two otherwise-identical equalites, we want to
    keep the visible one, and discharge the invisible one.  Hence the
    call to strictly_more_visible.
++
 +(CE4) Suppose we have this set up (#25440):
 +   Inert:     [W] g1: F a ~ a Int    (arising from (F a ~ a Int)
 +   Work item: [W] g2: F alpha ~ F a  (arising from (F alpha ~ F a)
 +   We rewrite g2 with g1, to give
 +              [W] g2{rw:g1} : F alpha ~ a Int
 +   Now if F is injective we can get [W] alpha~a, and hence alpha:=a, and
 +   we kick out g1. Now we have two constraints
 +       [W] g1        : F a ~ a Int  (arising from (F a ~ a Int)
 +       [W] g2{rw:g1} : F a ~ a Int  (arising from (F alpha ~ F a)
 +   If we end up with g2 in the inert set (not g1) we'll get a very confusing
 +   error message that we can solve (F a ~ a Int)
 +       arising from F a ~ F a
++
 +   TL;DR: Better to hang on to `g1` (with no rewriters), in preference
 +   to `g2` (which has a rewriter).
++
 +   See (WRW1) in Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint.
  -}
  tryInertEqs :: EqCt -> SolverStage ()
@@ -2646,21 +2695,27 @@ inertsCanDischarge inerts (EqCt { eq_lhs = lhs_w, eq_rhs = rhs_w
      loc_w  = ctEvLoc ev_w
      flav_w = ctEvFlavour ev_w
      fr_w   = (flav_w, eq_rel)
 +    empty_rw_w = isEmptyRewriterSet (ctEvRewriters ev_w)
      inert_beats_wanted ev_i eq_rel
        = -- eqCanRewriteFR:        see second bullet of Note [Combining equalities]
 -        -- strictly_more_visible: see last bullet of Note [Combining equalities]
          fr_i `eqCanRewriteFR` fr_w
 -        && not ((loc_w `strictly_more_visible` ctEvLoc ev_i)
 -                 && (fr_w `eqCanRewriteFR` fr_i))
 +        && not (prefer_wanted ev_i && (fr_w `eqCanRewriteFR` fr_i))
        where
          fr_i = (ctEvFlavour ev_i, eq_rel)
 -    -- See Note [Combining equalities], final bullet
 +    -- See (CE3) in Note [Combining equalities]
      strictly_more_visible loc1 loc2
         = not (isVisibleOrigin (ctLocOrigin loc2)) &&
           isVisibleOrigin (ctLocOrigin loc1)
 +    prefer_wanted ev_i
 +      =  (loc_w `strictly_more_visible` ctEvLoc ev_i)
 +             -- strictly_more_visible: see (CE3) in Note [Combining equalities]
 +      || (empty_rw_w && not (isEmptyRewriterSet (ctEvRewriters ev_i)))
 +             -- Prefer the one that has no rewriters
 +             -- See (CE4) in Note [Combining equalities]
++
  inertsCanDischarge _ _ = Nothing

compiler/GHC/Tc/Solver/Monad.hs

@@ -150,7 +150,6 @@ import qualified GHC.Tc.Utils.Env      as TcM
+        )
  import GHC.Tc.Zonk.Monad ( ZonkM )
  import qualified GHC.Tc.Zonk.TcType  as TcM
 -import qualified GHC.Tc.Zonk.Type as TcM
  import GHC.Driver.DynFlags
@@ -475,10 +474,14 @@ kickOutAfterUnification tv_list = case nonEmpty tv_list of
         ; return n_kicked }
  kickOutAfterFillingCoercionHole :: CoercionHole -> TcS ()
 --- See Wrinkle (EIK2a) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
 +-- See Wrinkle (EIK2) in Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
  -- It's possible that this could just go ahead and unify, but could there be occurs-check
  -- problems? Seems simpler just to kick out.
  kickOutAfterFillingCoercionHole hole
 +  | not (isHeteroKindCoHole hole)
 +  = return ()  -- Only hetero-kind coercion holes provoke kick-out;
 +               -- see (EIK2b) in Note [Equalities with incompatible kinds]
 +  | otherwise
    = do { ics <- getInertCans
         ; let (kicked_out, ics') = kick_out ics
               n_kicked           = lengthBag kicked_out
@@ -497,14 +500,14 @@ kickOutAfterFillingCoercionHole hole
      kick_out ics@(IC { inert_irreds = irreds })
        = -- We only care about irreds here, because any constraint blocked
          -- by a coercion hole is an irred.  See wrinkle (EIK2a) in
 -        -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Canonical
 +        -- Note [Equalities with incompatible kinds] in GHC.Tc.Solver.Equality
          (irreds_to_kick, ics { inert_irreds = irreds_to_keep })
        where
          (irreds_to_kick, irreds_to_keep) = partitionBag kick_ct irreds
 -    kick_ct :: IrredCt -> Bool
 -         -- True: kick out; False: keep.
 -    kick_ct ct
 +    kick_ct :: IrredCt -> Bool    -- True: kick out; False: keep.
 +    kick_ct ct  -- See (EIK2) in Note [Equalities with incompatible kinds]
 +                -- for this very specific kick-ot stuff
        | IrredCt { ir_ev = ev, ir_reason = reason } <- ct
        , CtWanted (WantedCt { ctev_rewriters = RewriterSet rewriters }) <- ev
        , NonCanonicalReason ctyeq <- reason
@@ -847,17 +850,15 @@ removeInertCt is ct
  -- | Looks up a family application in the inerts.
  lookupFamAppInert :: (CtFlavourRole -> Bool)  -- can it rewrite the target?
 -                  -> TyCon -> [Type] -> TcS (Maybe (Reduction, CtFlavourRole))
 +                  -> TyCon -> [Type] -> TcS (Maybe EqCt)
  lookupFamAppInert rewrite_pred fam_tc tys
    = do { IS { inert_cans = IC { inert_funeqs = inert_funeqs } } <- getInertSet
         ; return (lookup_inerts inert_funeqs) }
    where
      lookup_inerts inert_funeqs
 -      | Just ecl <- findFunEq inert_funeqs fam_tc tys
 -      , Just (EqCt { eq_ev = ctev, eq_rhs = rhs })
 -          <- find (rewrite_pred . eqCtFlavourRole) ecl
 -      = Just (mkReduction (ctEvCoercion ctev) rhs, ctEvFlavourRole ctev)
 -      | otherwise = Nothing
 +      = case findFunEq inert_funeqs fam_tc tys of
 +          Nothing              -> Nothing
 +          Just (ecl :: [EqCt]) -> find (rewrite_pred . eqCtFlavourRole) ecl
  lookupInInerts :: CtLoc -> TcPredType -> TcS (Maybe CtEvidence)
  -- Is this exact predicate type cached in the solved or canonicals of the InertSet?
@@ -1467,8 +1468,8 @@ emitWork cts
           -- c1 is rewritten by another, c2.  When c2 gets solved,
           -- c1 has no rewriters, and can be prioritised; see
           -- Note [Prioritise Wanteds with empty RewriterSet]
 -         -- in GHC.Tc.Types.Constraint wrinkle (WRW1)
 -       ; cts <- wrapTcS $ mapBagM TcM.zonkCtRewriterSet cts
 +         -- in GHC.Tc.Types.Constraint wrinkle (PER1)
 +       ; cts <- liftZonkTcS $ mapBagM TcM.zonkCtRewriterSet cts
         ; updWorkListTcS (extendWorkListCts cts) }
  emitImplication :: Implication -> TcS ()
@@ -2340,7 +2341,7 @@ wrapUnifierX ev role do_unifications
         ; wrapTcS $
           do { defer_ref   <- TcM.newTcRef emptyBag
              ; unified_ref <- TcM.newTcRef []
 -            ; rewriters   <- TcM.zonkRewriterSet (ctEvRewriters ev)
 +            ; rewriters   <- TcM.liftZonkM (TcM.zonkRewriterSet (ctEvRewriters ev))
              ; let env = UE { u_role      = role
                             , u_rewriters = rewriters
                             , u_loc       = ctEvLoc ev

compiler/GHC/Tc/Solver/Rewrite.hs

@@ -150,13 +150,16 @@ bumpDepth (RewriteM thing_inside)
        { let !env' = env { re_loc = bumpCtLocDepth (re_loc env) }
        ; thing_inside env' }
 +recordRewriter :: CtEvidence -> RewriteM ()
 +-- Record that we have rewritten the target with this (equality) evidence
  -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
 --- Precondition: the WantedCtEvidence is for an equality constraint
 -recordRewriter :: WantedCtEvidence -> RewriteM ()
 -recordRewriter (WantedCt { ctev_dest = HoleDest hole })
 -  = RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole)
 -recordRewriter other =
 -  pprPanic "recordRewriter: non-equality constraint" (ppr other)
 +-- Precondition: the CtEvidence is for an equality constraint
 +recordRewriter (CtGiven {})
 +  = return ()
 +recordRewriter (CtWanted (WantedCt { ctev_dest = dest }))
 +  = case dest of
 +      HoleDest hole -> RewriteM $ \env -> updTcRef (re_rewriters env) (`addRewriter` hole)
 +      other         -> pprPanic "recordRewriter: non-equality constraint" (ppr other)
  {- Note [Rewriter EqRels]
  ~~~~~~~~~~~~~~~~~~~~~~~~~
@@ -848,16 +851,18 @@ rewrite_exact_fam_app tc tys
           -- STEP 3: try the inerts
         ; flavour <- getFlavour
 -       ; result2 <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis
 -       ; case result2 of
 -         { Just (redn, (inert_flavour, inert_eq_rel))
 +       ; mb_eq <- liftTcS $ lookupFamAppInert (`eqCanRewriteFR` (flavour, eq_rel)) tc xis
 +       ; case mb_eq of
 +         { Just (EqCt { eq_ev = inert_ev, eq_rhs = inert_rhs, eq_eq_rel = inert_eq_rel })
               -> do { traceRewriteM "rewrite family application with inert"
                                  (ppr tc <+> ppr xis $$ ppr redn)
 -                   ; finish (inert_flavour == Given) (homogenise downgraded_redn) }
 -               -- this will sometimes duplicate an inert in the cache,
 +                   ; recordRewriter inert_ev
 +                   ; finish (isGiven inert_ev) (homogenise downgraded_redn) }
 +               -- This will sometimes duplicate an inert in the cache,
                 -- but avoiding doing so had no impact on performance, and
                 -- it seems easier not to weed out that special case
               where
 +               redn            = mkReduction (ctEvCoercion inert_ev) inert_rhs
                 inert_role      = eqRelRole inert_eq_rel
                 role            = eqRelRole eq_rel
                 downgraded_redn = downgradeRedn role inert_role redn
@@ -1024,11 +1029,8 @@ rewrite_tyvar2 tv fr@(_, eq_rel)
               -> do { traceRewriteM "Following inert tyvar" $
                          vcat [ ppr tv <+> equals <+> ppr rhs_ty
                               , ppr ctev ]
 -                   ; case ctev of
 -                       CtGiven {} -> return ()
 -                       CtWanted wtd ->
 +                   ; recordRewriter ctev
                           -- See Note [Wanteds rewrite Wanteds] in GHC.Tc.Types.Constraint
 -                         recordRewriter wtd
                     ; let rewriting_co1 = ctEvCoercion ctev
                           rewriting_co  = case (ct_eq_rel, eq_rel) of

compiler/GHC/Tc/Types/Constraint.hs

@@ -240,18 +240,24 @@ instance Outputable DictCt where
  {- Note [Canonical equalities]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  An EqCt is a canonical equality constraint, one that can live in the inert set,
 -and that can be used to rewrite other constrtaints. It satisfies these invariants:
 +and that can be used to rewrite other constraints. It satisfies these invariants:
++
    * (TyEq:OC) lhs does not occur in rhs (occurs check)
                Note [EqCt occurs check]
++
    * (TyEq:F) rhs has no foralls
        (this avoids substituting a forall for the tyvar in other types)
++
    * (TyEq:K) typeKind lhs `tcEqKind` typeKind rhs; Note [Ct kind invariant]
++
    * (TyEq:N) If the equality is representational, rhs is not headed by a saturated
      application of a newtype TyCon. See GHC.Tc.Solver.Equality
      Note [No top-level newtypes on RHS of representational equalities].
      (Applies only when constructor of newtype is in scope.)
++
    * (TyEq:U) An EqCt is not immediately unifiable. If we can unify a:=ty, we
      will not form an EqCt (a ~ ty).
++
    * (TyEq:CH) rhs does not mention any coercion holes that resulted from fixing up
      a hetero-kinded equality.  See Note [Equalities with incompatible kinds] in
      GHC.Tc.Solver.Equality, wrinkle (EIK2)
@@ -534,9 +540,12 @@ cteSolubleOccurs   = CTEP (bit 3)   -- Occurs-check under a type function, or in
     -- cteSolubleOccurs must be one bit to the left of cteInsolubleOccurs
     -- See also Note [Insoluble mis-match] in GHC.Tc.Errors
 -cteCoercionHole    = CTEP (bit 4)   -- Coercion hole encountered
 +cteCoercionHole    = CTEP (bit 4)   -- Kind-equality coercion hole encountered
 +                                    -- See (EIK2) in Note [Equalities with incompatible kinds]
++
  cteConcrete        = CTEP (bit 5)   -- Type variable that can't be made concrete
                                      --    e.g. alpha[conc] ~ Maybe beta[tv]
++
  cteSkolemEscape    = CTEP (bit 6)   -- Skolem escape e.g.  alpha[2] ~ b[sk,4]
  cteProblem :: CheckTyEqProblem -> CheckTyEqResult
@@ -2444,19 +2453,29 @@ We thus want Wanteds to rewrite Wanteds in order to accept more programs,
  but we don't want Wanteds to rewrite Wanteds because doing so can create
  inscrutable error messages. To solve this dilemma:
 -* We allow Wanteds to rewrite Wanteds, but...
 +* 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.
 -* 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.)
 +* 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.
  * In error reporting, we simply suppress any errors that have been rewritten
    by /unsolved/ wanteds. This suppression happens in GHC.Tc.Errors.mkErrorItem,
 -  which uses GHC.Tc.Zonk.Type.zonkRewriterSet to look through any filled
 +  which uses `GHC.Tc.Zonk.Type.zonkRewriterSet` to look through any filled
    coercion holes. The idea is that we wish to report the "root cause" -- the
    error that rewrote all the others.
 -* We prioritise Wanteds that have an empty RewriterSet:
 +* In error reporting, we prioritise Wanteds that have an empty RewriterSet:
    see Note [Prioritise Wanteds with empty RewriterSet].
  Let's continue our first example above:
@@ -2471,19 +2490,30 @@ Because Wanteds can rewrite Wanteds, w1 will rewrite w2, yielding
  The {w1} in the second line of output is the RewriterSet of w1.
 -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.
 +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 zonking 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.
  Note [Prioritise Wanteds with empty RewriterSet]
  ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  When extending the WorkList, in GHC.Tc.Solver.InertSet.extendWorkListEq,
 -we priorities constraints that have no rewriters. Here's why.
 +we prioritise constraints that have no rewriters. Here's why.
  Consider this, which came up in T22793:
    inert: {}
@@ -2527,11 +2557,11 @@ GHC.Tc.Solver.InertSet.extendWorkListEq, and extendWorkListEqs.
  Wrinkles
 -(WRW1) Before checking for an empty RewriterSet, we zonk the RewriterSet,
 +(PER1) Before checking for an empty RewriterSet, we zonk the RewriterSet,
    because some of those CoercionHoles may have been filled in since we last
    looked: see GHC.Tc.Solver.Monad.emitWork.
 -(WRW2) Despite the prioritisation, it is hard to be /certain/ that we can't end up
 +(PER2) Despite the prioritisation, it is hard to be /certain/ that we can't end up
    in a situation where all of the Wanteds have rewritten each other. In
    order to report /some/ error in this case, we simply report all the
    Wanteds. The user will get a perhaps-confusing error message, but they've

compiler/GHC/Tc/Utils/TcMType.hs

@@ -49,7 +49,6 @@ module GHC.Tc.Utils.TcMType (
    newCoercionHole, newCoercionHoleO, newVanillaCoercionHole,
    fillCoercionHole, isFilledCoercionHole,
 -  unpackCoercionHole, unpackCoercionHole_maybe,
    checkCoercionHole,
    newImplication,
@@ -115,7 +114,6 @@ import GHC.Tc.Types.CtLoc( CtLoc, ctLocOrigin )
  import GHC.Tc.Utils.Monad        -- TcType, amongst others
  import GHC.Tc.Utils.TcType
  import GHC.Tc.Errors.Types
 -import GHC.Tc.Zonk.Type
  import GHC.Tc.Zonk.TcType
  import GHC.Builtin.Names
@@ -371,6 +369,7 @@ newCoercionHoleO (KindEqOrigin {}) pty = new_coercion_hole True pty
  newCoercionHoleO _ pty                 = new_coercion_hole False pty
  new_coercion_hole :: Bool -> TcPredType -> TcM CoercionHole
 +-- For the Bool, see (EIK2) in Note [Equalities with incompatible kinds]
  new_coercion_hole hetero_kind pred_ty
    = do { co_var <- newEvVar pred_ty
         ; traceTc "New coercion hole:" (ppr co_var <+> dcolon <+> ppr pred_ty)
@@ -1583,7 +1582,7 @@ collect_cand_qtvs_co orig_ty cur_lvl bound = go_co
      go_co dv (SubCo co)              = go_co dv co
      go_co dv (HoleCo hole)
 -      = do m_co <- unpackCoercionHole_maybe hole
 +      = do m_co <- liftZonkM (unpackCoercionHole_maybe hole)
             case m_co of
               Just co -> go_co dv co
               Nothing -> go_cv dv (coHoleCoVar hole)

compiler/GHC/Tc/Utils/Unify.hs

@@ -2649,8 +2649,9 @@ There are five reasons not to unify:
      we can fill beta[tau] := beta[conc]. This is why we call
      'makeTypeConcrete' in startSolvingByUnification.
 -5. (COERCION-HOLE) Confusing coercion holes
 -   Suppose our equality is
 +5. (COERCION-HOLE) rhs does not mention any coercion holes that resulted from
 +    fixing up a hetero-kinded equality.  This is the same as (TyEq:CH) in
 +    Note [Canonical equalities].  Suppose our equality is
       (alpha :: k) ~ (Int |> {co})
     where co :: Type ~ k is an unsolved wanted. Note that this equality
     is homogeneous; both sides have kind k. We refrain from unifying here, because
@@ -3549,7 +3550,7 @@ checkCo flags co =
          -- Check for coercion holes, if unifying.
          -- See (COERCION-HOLE) in Note [Unification preconditions]
          | case lc of { LC_None {} -> False; _ -> True } -- equivalent to "we are unifying"; see Note [TyEqFlags]
 -        , hasCoercionHoleCo co
 +        , hasHeteroKindCoercionHoleCo co
          -> return $ PuFail (cteProblem cteCoercionHole)
          -- Occurs check (can promote)

compiler/GHC/Tc/Zonk/TcType.hs

 +{-# LANGUAGE DuplicateRecordFields #-}
++
  {-
  (c) The University of Glasgow 2006
  (c) The AQUA Project, Glasgow University, 1996-1998
@@ -36,6 +38,13 @@ module GHC.Tc.Zonk.TcType
      -- ** Zonking constraints
    , zonkCt, zonkWC, zonkSimples, zonkImplication
 +    -- * Rewriter sets
 +  , zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet
++
 +    -- * Coercion holes
 +  , isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe
++
++
      -- * Tidying
    , tcInitTidyEnv, tcInitOpenTidyEnv
    , tidyCt, tidyEvVar, tidyDelayedError
@@ -81,7 +90,7 @@ import GHC.Core.Coercion
  import GHC.Core.Predicate
  import GHC.Utils.Constants
 -import GHC.Utils.Outputable
 +import GHC.Utils.Outputable as Outputable
  import GHC.Utils.Misc
  import GHC.Utils.Monad ( mapAccumLM )
  import GHC.Utils.Panic
@@ -89,6 +98,9 @@ import GHC.Utils.Panic
  import GHC.Data.Bag
  import GHC.Data.Pair
 +import Data.Semigroup
 +import Data.Maybe
++
  {- *********************************************************************
  *                                                                      *
                      Writing to metavariables
@@ -366,8 +378,8 @@ checkCoercionHole cv co
         ; return $
           assertPpr (ok cv_ty)
                     (text "Bad coercion hole" <+>
 -                    ppr cv <> colon <+> vcat [ ppr t1, ppr t2, ppr role
 -                                             , ppr cv_ty ])
 +                    ppr cv Outputable.<> colon
 +                    <+> vcat [ ppr t1, ppr t2, ppr role, ppr cv_ty ])
           co }
    | otherwise
    = return co
@@ -494,9 +506,15 @@ zonkCt ct
         ; return (mkNonCanonical fl') }
  zonkCtEvidence :: CtEvidence -> ZonkM CtEvidence
 -zonkCtEvidence ctev
 -  = do { pred' <- zonkTcType (ctEvPred ctev)
 -       ; return (setCtEvPredType ctev pred') }
 +-- 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' })) }
  zonkSkolemInfo :: SkolemInfo -> ZonkM SkolemInfo
  zonkSkolemInfo (SkolemInfo u sk) = SkolemInfo u <$> zonkSkolemInfoAnon sk
@@ -530,6 +548,103 @@ win.
  But c.f Note [Sharing when zonking to Type] in GHC.Tc.Zonk.Type.
 +%************************************************************************
 +%*                                                                      *
 +                 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') }
++
 +-- | Zonk a rewriter set; if a coercion hole in the set has been filled,
 +-- find all the free un-filled coercion holes in the coercion that fills it
 +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)  -- Not filled
 +               Just co -> unUCHM (check_co co) }         -- Filled: look inside
++
 +    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
++
++
 +{-
  %************************************************************************
  %*                                                                      *
                   Tidying

compiler/GHC/Tc/Zonk/Type.hs

@@ -28,12 +28,6 @@ module GHC.Tc.Zonk.Type (
          -- ** 'ZonkEnv', and the 'ZonkT' and 'ZonkBndrT' monad transformers
          module GHC.Tc.Zonk.Env,
 -        -- * Coercion holes
 -        isFilledCoercionHole, unpackCoercionHole, unpackCoercionHole_maybe,
+-
 -        -- * Rewriter sets
 -        zonkRewriterSet, zonkCtRewriterSet, zonkCtEvRewriterSet,
+-
          -- * Tidying
          tcInitTidyEnv, tcInitOpenTidyEnv,
@@ -55,7 +49,6 @@ import GHC.Tc.TyCl.Build ( TcMethInfo, MethInfo )
  import GHC.Tc.Utils.Env ( tcLookupGlobalOnly )
  import GHC.Tc.Utils.TcType
  import GHC.Tc.Utils.Monad ( newZonkAnyType, setSrcSpanA, liftZonkM, traceTc, addErr )
 -import GHC.Tc.Types.Constraint
  import GHC.Tc.Types.Evidence
  import GHC.Tc.Errors.Types
  import GHC.Tc.Zonk.Env
@@ -88,7 +81,6 @@ import GHC.Types.Id
  import GHC.Types.TypeEnv
  import GHC.Types.Basic
  import GHC.Types.SrcLoc
 -import GHC.Types.Unique.Set
  import GHC.Types.Unique.FM
  import GHC.Types.TyThing
@@ -99,7 +91,6 @@ import GHC.Data.Bag
  import Control.Monad
  import Control.Monad.Trans.Class ( lift )
 -import Data.Semigroup
  import Data.List.NonEmpty ( NonEmpty )
  import Data.Foldable ( toList )
@@ -1956,89 +1947,3 @@ finding the free type vars of an expression is necessarily monadic
  operation. (consider /\a -> f @ b, where b is side-effected to a)
  -}
 -{-
 -************************************************************************
 -*                                                                      *
 -             Checking for coercion holes
 -*                                                                      *
 -************************************************************************
 --}
+-
 --- | Is a coercion hole filled in?
 -isFilledCoercionHole :: CoercionHole -> TcM Bool
 -isFilledCoercionHole (CoercionHole { ch_ref = ref })
 -  = isJust <$> readTcRef ref
+-
 --- | Retrieve the contents of a coercion hole. Panics if the hole
 --- is unfilled
 -unpackCoercionHole :: CoercionHole -> TcM 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 -> TcM (Maybe Coercion)
 -unpackCoercionHole_maybe (CoercionHole { ch_ref = ref }) = readTcRef ref
+-
 -zonkCtRewriterSet :: Ct -> TcM 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 -> TcM 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 -> TcM 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 -> TcM RewriterSet -> TcM RewriterSet
 -    go hole m_acc = unionRewriterSet <$> check_hole hole <*> m_acc
+-
 -    check_hole :: CoercionHole -> TcM 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 :: TcM RewriterSet }
+-
 -instance Semigroup UnfilledCoercionHoleMonoid where
 -  UCHM l <> UCHM r = UCHM (unionRewriterSet <$> l <*> r)
+-
 -instance Monoid UnfilledCoercionHoleMonoid where
 -  mempty = UCHM (return emptyRewriterSet)

testsuite/tests/indexed-types/should_fail/T3330c.stderr

+-
 -T3330c.hs:25:43: error: [GHC-18872]
 -    • Couldn't match kind ‘* -> *’ with ‘*’
 -      When matching types
 -        f1 :: * -> *
 -        f1 x :: *
 -      Expected: Der ((->) x) (Der f1 x)
 -        Actual: R f1
 -    • In the first argument of ‘plug’, namely ‘rf’
 +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
        In the first argument of ‘Inl’, namely ‘(plug rf df x)’
        In the expression: Inl (plug rf df x)
      • Relevant bindings include
 -        x :: x (bound at T3330c.hs:25:29)
          df :: Der f1 x (bound at T3330c.hs:25:25)
          rf :: R f1 (bound at T3330c.hs:25:13)
 -        plug' :: R f -> Der f x -> x -> f x (bound at T3330c.hs:25:1)
++

testsuite/tests/indexed-types/should_fail/T4174.stderr

+-
 -T4174.hs:45:12: error: [GHC-18872]
 -    • Couldn't match type ‘False’ with ‘True’
 -        arising from a use of ‘sync_large_objects’
 +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
      • In the expression: sync_large_objects
        In an equation for ‘testcase’: testcase = sync_large_objects
 +    • Relevant bindings include
 +        testcase :: m (Field (Way (GHC6'8 minor) n t p) a b)
 +          (bound at T4174.hs:45:1)
++

testsuite/tests/indexed-types/should_fail/T8227.stderr

@@ -13,12 +13,3 @@ T8227.hs:24:27: error: [GHC-83865]
          absoluteToParam :: Scalar (V a) -> a -> Scalar (V a)
            (bound at T8227.hs:24:1)
 -T8227.hs:24:48: error: [GHC-27958]
 -    • Couldn't match type ‘p0’ with ‘Scalar (V p0)’
 -        arising from a type equality Scalar (V a) ~ Scalar (V p0) -> p0
 -      The type variable ‘p0’ is ambiguous
 -    • In the second argument of ‘arcLengthToParam’, namely ‘eps’
 -      In the expression: arcLengthToParam eps eps
 -      In an equation for ‘absoluteToParam’:
 -          absoluteToParam eps seg = arcLengthToParam eps eps
+-

testsuite/tests/typecheck/should_compile/T25266a.stderr

 -T25266a.hs:10:41: error: [GHC-25897]
 -    • Could not deduce ‘p1 ~ p2’
 +T25266a.hs:10:39: error: [GHC-25897]
 +    • Could not deduce ‘p2 ~ p1’
        from the context: a ~ Int
          bound by a pattern with constructor: T1 :: T Int,
                   in a case alternative
          at T25266a.hs:10:23-24
 -      ‘p1’ is a rigid type variable bound by
 +      ‘p2’ is a rigid type variable bound by
          the inferred type of f :: p1 -> p2 -> T a -> Int
          at T25266a.hs:(9,1)-(11,40)
 -      ‘p2’ is a rigid type variable bound by
 +      ‘p1’ is a rigid type variable bound by
          the inferred type of f :: p1 -> p2 -> T a -> Int
          at T25266a.hs:(9,1)-(11,40)
 -    • In the expression: y
 +    • In the expression: x
        In the first argument of ‘length’, namely ‘[x, y]’
        In the expression: length [x, y]
      • Relevant bindings include

testsuite/tests/typecheck/should_fail/T18851.stderr

+-
  T18851.hs:35:5: error: [GHC-18872]
 -    • Couldn't match type ‘B’ with ‘A’
 -        arising from a superclass required to satisfy ‘C int0 A’,
 +    • Couldn't match type ‘Bool’ with ‘B’
 +        arising from a superclass required to satisfy ‘C Int B’,
          arising from a use of ‘f’
      • In the expression: f @A @B
        In an equation for ‘g’: g = f @A @B
++