anchor.diff:                    (a, imp_a), subst, bvs@[x], Env.trivial_guard
   
                   | Tm_uvar _ ->
  -                  let env = Env.set_expected_typ env t_f in
  +                  let use_eq = true in
  +                  let env = Env.set_expected_typ_maybe_eq env t_f use_eq in
                     //
                     //AR: 03/03: When typechecking these uvar args,
                     //  we don't want to solve the deferred constraints here,
  
positive.code:                            (Print.subst_to_string subst)
                             (Print.term_to_string targ);
              let targ, g_ex = check_no_escape (Some head) env fvs targ in
              let env = Env.set_expected_typ env targ in
              let env = {env with use_eq=is_eq bqual} in
              if debug env Options.High
              then BU.print4 "Checking arg (%s) %s at type %s with use_eq:%s\n"
                     (Print.tag_of_term e) (Print.term_to_string e) (Print.term_to_string targ) (string_of_bool env.use_eq);
              let e, c, g_e = tc_term env e in
              let g = Env.conj_guard g_ex <| Env.conj_guard g g_e in
  //                if debug env Options.High then BU.print2 "Guard on this arg is %s;\naccumulated guard is %s\n" (guard_to_string env g_e) (guard_to_string env g);
  
negative.code:     then BU.print1 "Checking pattern: %s\n" (Print.pat_to_string p0);
      let bvs, tms, pat_e, pat, g, erasable =
          check_nested_pattern
              (Env.clear_expected_typ env |> fst)
              (PatternUtils.elaborate_pat env p0)
              pat_t
      in
  