; check_result <- checkTypeEq ev eq_rel lhs rhs

        ; case check_result of

             PuFail reason

               | reason `cterHasOnlyProblems` do_not_prevent_rewriting

               ->   do { new_ev <- rewriteEqEvidenceSwapOnly ev eq_rel swapped lhs rhs

                       ; continueWith $ Right $

                              , eq_lhs = lhs , eq_rhs = rhs } }

               | otherwise

               -> -- We can't unify, and this equality should not be used to rewrite

                  -- other constraints (e.g. because it has an occurs check).

                  -- So add it to the inert Irreds.

                            , eq_lhs = lhs

                            , eq_rhs = reductionReducedType rhs_redn } } }

 -- | Some problems prevent /unification/ but not /rewriting/:

 --

 -- Skolem-escape: if we have [W] alpha[2] ~ Maybe b[3]

 do_not_prevent_rewriting :: CheckTyEqResult

 do_not_prevent_rewriting = cteProblem cteSkolemEscape S.<>

                            cteProblem cteConcrete

 ----------------------

 finishCanWithIrred :: CtIrredReason -> CtEvidence

                    -> TcS (StopOrContinue (Either IrredCt a))