anchor.diff:              | [] -> None //seems ill-typed at this point
               | _ -> aux pat_binders more_formals t_res args
               end
  -        in
  -        let formals, t_res = U.arrow_formals t_hd in
  -        aux [] formals t_res args
  +    in
  +    match args with
  +    | [] -> Some ([], t_hd) //this really a pattern, not a quasi_pattern
  +    | _ ->
  +      let formals, t_res = U.arrow_formals t_hd in
  +      aux [] formals t_res args
   
   (******************************************************************************************************)
   (* Main solving algorithm begins here *)
  
positive.code:         let args_rhs, last_arg_rhs = BU.prefix args in
          let rhs' = S.mk_Tm_app rhs_hd args_rhs None rhs.pos in
          let t_lhs, u_lhs, _lhs_args = lhs in
          let lhs', lhs'_last_arg, _wl = //FIXME! dropping the wl here
                let _, t_last_arg, wl = copy_uvar u_lhs (fst <| U.type_u()) wl in
                //FIXME: this may be an implicit arg ... fix qualifier
                let _, lhs', wl = copy_uvar u_lhs (U.arrow [S.null_binder t_last_arg] (S.mk_Total t_res_lhs)) wl in
  
negative.code: //(******************************************************************************************************)
  //(* The case where t1 < u, ..., tn < u: we solve this by taking u=t1\/...\/tn                          *)
  //(******************************************************************************************************)
  // and solve_rigid_flex_meet (env:Env.env) (tp:tprob) (wl:worklist) : option<worklist> =
  //    if Env.debug env <| Options.Other "RelCheck"
  //    then BU.print1 "Trying to solve by meeting refinements:%s\n" (string_of_int tp.pid);
  //    let u, args = U.head_and_args tp.rhs in
  