anchor.diff:          //               (names_to_string fvs2);
           let uvars, occurs_ok, msg = occurs_check ctx_uv rhs in
           if not occurs_ok
  -        then giveup_or_defer env orig wl (Thunk.mkv <| "occurs-check failed: " ^ (Option.get msg))
  +        then giveup_or_defer env orig wl
  +               Deferred_occur_check_failed
  +               (Thunk.mkv <| "occurs-check failed: " ^ (Option.get msg))
           else if BU.set_is_subset_of fvs2 fvs1
           then let sol = mk_solution env lhs lhs_binders rhs in
                let wl = restrict_all_uvars env ctx_uv lhs_binders uvars wl in
  
positive.code:          in
           let _, occurs_ok, msg = occurs_check u_lhs arrow in
           if not occurs_ok
           then giveup_or_defer env orig wl (mklstr (fun () -> "occurs-check failed: " ^ (Option.get msg)))
           else aux [] [] formals wl
  
  and solve_binders (env:Env.env) (bs1:binders) (bs2:binders) (orig:prob) (wl:worklist)
  
negative.code:            let msg = mklstr (fun () ->
                          BU.format1 "first_order heuristic cannot solve %s; lhs not a quasi-pattern"
                            (prob_to_string env orig)) in
             giveup_or_defer env orig wl Deferred_first_order_heuristic_failed msg
  
          | Some (bs_lhs, t_res_lhs) ->
            if is_app rhs
  