anchor.diff:      if Env.debug env <| Options.Other "RelCheck"
       then BU.print1 "solve:\n\t%s\n" (wl_to_string probs);
       match next_prob probs with
  -       | Some hd, tl, rank ->
  -         let probs = {probs with attempting=tl} in
  -         begin match hd with
  -            | CProb cp ->
  -              solve_c env (maybe_invert cp) probs
  -
  -            | TProb tp ->
  -              if not probs.defer_ok
  -              && rank = flex_rigid
  -              then let tp = {tp with relation=EQ} in
  -                   solve_t' env tp probs
  -              //      match solve_flex_rigid_join env tp probs with
  -              //      | None -> solve_t' env (maybe_invert tp) probs //giveup env "join doesn't exist" hd
  -              //      | Some wl -> solve env wl
  -              else if not probs.defer_ok
  -                   && rigid_flex = rank
  -              then let tp = {tp with relation=EQ} in
  -                   solve_t' env tp probs
  -                   //match solve_rigid_flex_meet env tp probs with
  -                   // | None -> solve_t' env (maybe_invert tp) probs //giveup env "meet doesn't exist" hd
  -                   // | Some wl -> solve env wl
  -              else solve_t' env (maybe_invert tp) probs
  +    | Some hd, tl, rank ->
  +      let probs = {probs with attempting=tl} in
  +      begin match hd with
  +      | CProb cp ->
  +            solve_c env (maybe_invert cp) probs
  +
  +      | TProb tp ->
  +            if (tp.relation = EQ && rank <> flex_flex)
  +            || rank=rigid_rigid
  +            then solve_t' env tp probs
  +            else if probs.defer_ok
  +            then solve env (defer "deferring subtyping or flex_flex" hd probs)
  +            else if tp.relation <> EQ
  +            then solve_rigid_flex_or_flex_rigid_subtyping rank env tp probs
  +            else solve_t' env tp probs //flex_flex eq
  +      end
  +
  +    | None, _, _ ->
  +         begin
  +         match probs.wl_deferred with
  +         | [] ->
  +           Success ([], probs.wl_implicits) //Yay ... done!
  +
  +         | _ ->
  +           let attempt, rest = probs.wl_deferred |> List.partition (fun (c, _, _) -> c < probs.ctr) in
  +           match attempt with
  +            | [] -> //can't solve yet; defer the rest
  +              Success(List.map (fun (_, x, y) -> (x, y)) probs.wl_deferred, probs.wl_implicits)
  +
  +            | _ ->
  +              solve env ({probs with attempting=attempt |> List.map (fun (_, _, y) -> y); wl_deferred=rest})
            end
  -
  -       | None, _, _ ->
  -         match probs.wl_deferred with
  -            | [] ->
  -              Success ([], probs.wl_implicits) //Yay ... done!
  -
  -            | _ ->
  -              let attempt, rest = probs.wl_deferred |> List.partition (fun (c, _, _) -> c < probs.ctr) in
  -              match attempt with
  -                 | [] -> //can't solve yet; defer the rest
  -                   Success(List.map (fun (_, x, y) -> (x, y)) probs.wl_deferred, probs.wl_implicits)
  -
  -                 | _ ->
  -                   solve env ({probs with attempting=attempt |> List.map (fun (_, _, y) -> y); wl_deferred=rest})
   
   and solve_one_universe_eq (env:Env.env) (orig:prob) (u1:universe) (u2:universe) (wl:worklist) : solution =
       match solve_universe_eq (p_pid orig) wl u1 u2 with
  -        | USolved wl ->
  -          solve env (solve_prob orig None [] wl)
  -
  -        | UFailed msg ->
  -          giveup env msg orig
  -
  -        | UDeferred wl ->
  -          solve env (defer "" orig wl)
  +    | USolved wl ->
  +      solve env (solve_prob orig None [] wl)
  +
  +    | UFailed msg ->
  +      giveup env msg orig
  +
  +    | UDeferred wl ->
  +      solve env (defer "" orig wl)
   
   and solve_maybe_uinsts (env:Env.env) (orig:prob) (t1:term) (t2:term) (wl:worklist) : univ_eq_sol =
       let rec aux wl us1 us2 = match us1, us2 with
  
positive.code:               aux (bs@[y, imp]) (bs_terms@[S.bv_to_name y, imp]) formals wl
           in
           aux [] [] formals wl
      in
  
      let imitate_app (orig:prob) (env:Env.env) (wl:worklist)
  
negative.code:     end
      else giveup env msg orig
  
  (******************************************************************************************************)
  (* The case where t1 < u, ..., tn < u: we solve this by taking u=t1\/...\/tn                          *)
  (* The case where u < t1, .... u < tn: we solve this by taking u=t1/\.../\tn                          *)
  (******************************************************************************************************)
  and solve_rigid_flex_or_flex_rigid_subtyping
      (rank:int)
      (env:Env.env) (tp:tprob) (wl:worklist) : solution =
    if Env.debug env <| Options.Other "RelCheck"
    then BU.print1 "Trying to solve by meeting refinements:%s\n" (string_of_int tp.pid);
    let flip = rank = flex_rigid in
    let this_flex, this_rigid = if flip then tp.lhs, tp.rhs else tp.rhs, tp.lhs in
    begin
    match (SS.compress this_rigid).n with
    | Tm_arrow _ ->
      let flex = destruct_flex_t this_flex in
      begin
      match quasi_pattern env flex with
      | None -> giveup env "flex-arrow subtyping, not a quasi pattern" (TProb tp)
      | Some (flex_bs, flex_t) ->
        imitate_arrow (TProb tp) env wl flex flex_bs flex_t tp.relation this_rigid
      end
  
    | _ ->
      let u, _args = U.head_and_args this_flex in
      begin
      match (SS.compress u).n with
      | Tm_uvar ctx_uvar ->
       let equiv t =
           let u', _ = U.head_and_args t in
           match (whnf env u').n with
           | Tm_uvar ctx_uvar' ->
             UF.equiv ctx_uvar.ctx_uvar_head ctx_uvar'.ctx_uvar_head
           | _ -> false
       in
      //find all other constraints of the form t <: u, or if flipped, u <: t
       let bounds_probs, rest =
         wl.attempting |> List.partition
         (function
           | TProb tp ->
             let tp = maybe_invert tp in
             begin
             match tp.rank with
             | Some rank' when rank=rank' ->
               if flip then equiv tp.lhs else equiv tp.rhs
  
             | _ -> false
             end
  
            | _ -> false)
       in
  
       let bounds_typs =
           whnf env this_rigid
           :: List.collect (function
                            | TProb p -> [(if flip
                                           then whnf env (maybe_invert p).rhs
                                           else whnf env (maybe_invert p).lhs)]
                            | _ -> [])
                            bounds_probs
       in
  
       begin
       match meet_or_join (if flip then U.mk_conj else U.mk_disj) bounds_typs env wl with
       | None ->
         giveup env "join/meet doesn't exist" (TProb tp)
  
       | Some (bound, sub_probs, wl) ->
         let eq_prob, wl =
              new_problem wl env bound EQ tp.rhs None tp.loc
                  (if flip then "joining refinements" else "meeting refinements")
         in
         let _ = if Env.debug env <| Options.Other "RelCheck"
                 then let wl' = {wl with attempting=TProb eq_prob::sub_probs} in
                      BU.print1 "After meet/join refinements: %s\n" (wl_to_string wl') in
         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
           solve env wl
         | Failed (p, msg) ->
           giveup env ("failed to solve sub-problems: " ^msg) (TProb tp)
       end
  
      | _ when flip -> failwith (BU.format1 "Impossible: Not a flex-rigid: %s" (prob_to_string env (TProb tp)))
      | _ -> failwith (BU.format1 "Impossible: Not a rigid-flex: %s" (prob_to_string env (TProb tp)))
      end
    end
  
  and imitate_arrow (orig:prob) (env:Env.env) (wl:worklist)
                    (lhs:flex_t) (bs_lhs:binders) (t_res_lhs:term)
                    (rel:rel)
                    (arrow:term)
          : solution =
          let _, u_lhs, _ = lhs in
          let imitate_comp bs bs_terms c wl =
  