anchor.diff:              | _ ->
                 bound
             in
  +          bound,
             new_problem wl env bound EQ this_flex None tp.loc
                   (if flip then "joining refinements" else "meeting refinements")
         in
  
positive.code: 
        let tx = UF.new_transaction () in
        begin
        match solve_t env eq_prob ({wl with attempting=sub_probs}) with
        | Success _ ->
           let wl = {wl with attempting=rest} in
           let wl = solve_prob' false (TProb tp) None [] wl in
           let _ = List.fold_left (fun wl p -> solve_prob' true p None [] wl) wl bounds_probs in
           UF.commit tx;
           solve env wl
        | Failed (p, msg) ->
           UF.rollback tx;
           giveup env ("failed to solve sub-problems: " ^msg) p
        end
  
      | _ when flip -> failwith (BU.format1 "Impossible: Not a flex-rigid: %s" (prob_to_string env (TProb tp)))
  
negative.code:       let (bound, sub_probs, wl) =
            meet_or_join (if flip then U.mk_conj else U.mk_disj) bounds_typs env wl
        in
        let bound_typ, (eq_prob, wl) =
            let _, flex_u, _ = destruct_flex_t this_flex in
            let bound =
              //We get constraints of the form (x:?u{phi} <: ?u)
  