; 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.