anchor.diff:                  if not norm
                   then as_function_typ true (N.unfold_whnf env t)
                   else let _, bs, _, c_opt, tacopt, envbody, body, g = expected_function_typ env None body in
  -                      Some (t, false), bs, [], c_opt, tacopt, envbody, body, g in
  +                      Some t, bs, [], c_opt, tacopt, envbody, body, g in
             as_function_typ false t
       in
   
  
positive.code:                 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
  
                (* 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
  
                | Tm_arrow(bs_expected, c_expected) ->
                  let bs_expected, c_expected = SS.open_comp bs_expected c_expected in
  
negative.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, bs, letrecs, Some c, None, envbody, body, g
  
                | _ -> (* expected type is not a function;
                          try normalizing it first;
  