anchor.diff:                  let _ = match env.letrecs with | [] -> () | _ -> failwith "Impossible" in
                   let bs, envbody, g, _ = tc_binders env bs in
                   let envbody, _ = Env.clear_expected_typ envbody in
  -                Some (t, true), bs, [], None, None, envbody, body, g
  +                Some t, bs, [], None, None, envbody, body, g
   
                 (* CK: add this case since the type may be f:(a -> M b wp){φ}, in which case I drop the refinement *)
                 (* NS: 07/21 dropping the refinement is not sound; we need to check that f validates phi. See Bug #284 *)
                 | Tm_refine (b, _) ->
                   let _, bs, bs', copt, tacopt, env, body, g = as_function_typ norm b.sort in
  -                Some (t, false), bs, bs', copt, tacopt, env, body, g
  +                Some t, bs, bs', copt, tacopt, env, body, g
   
                 | Tm_arrow(bs_expected, c_expected) ->
                   let bs_expected, c_expected = SS.open_comp bs_expected c_expected in
  
positive.code:                 let envbody, bs, g, c = check_actuals_against_formals env bs bs_expected in
                  let envbody, letrecs = if Env.should_verify env then mk_letrec_env envbody bs c else envbody, [] in
                  let envbody = Env.set_expected_typ envbody (U.comp_result c) in
                  Some (t, false), bs, letrecs, Some c, None, envbody, body, g
  
                | _ -> (* expected type is not a function;
                          try normalizing it first;
  
negative.code: 
  
      let rec expected_function_typ env t0 body
          : (option<typ>        (* any remaining expected type to check against *)
          * binders             (* binders from the abstraction checked against the binders in the corresponding Typ_fun, if any *)
          * binders             (* let rec binders, suitably guarded with termination check, if any *)
          * option<comp>        (* the expected comp type for the body *)
  