anchor.diff:  
     | Exp_abs(bs, body) ->  (* This is the dual of the treatment of application ... see the Exp_app case below. *)
       let fail :string -> typ -> 'a = fun msg t -> raise (Error(Tc.Errors.expected_a_term_of_type_t_got_a_function env msg t top, top.pos)) in
  -    let rec expected_function_typ env t0 = match t0 with 
  +    let rec expected_function_typ env t0 : (option<(typ*bool)> (* any remaining expected type to check against; bool signals to check using teq *)
  +                                            * binders   (* binders from the abstraction checked against the binders in the corresponding Typ_fun, if any *)
  +                                            * binders   (* any remaining binders in the abstraction *)
  +                                            * option<comp> (* the expected comp type for the body *)
  +                                            * env          (* environment for the body *)
  +                                            * guard_t) =   (* accumulated guard from checking the binders *)
  +       match t0 with 
           | None -> (* no expected type; just build a function type from the binders in the term *)
               let _ = match env.letrecs with [] -> () | _ -> failwith "Impossible" in
               let bs, envbody, g = tc_binders env bs 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, bs, [], None, envbody, g
  
                  | Typ_fun(bs', c) -> 
                      (* Two main interesting bits here;
  
negative.code:                  let bs, envbody, g, c = tc_binders ([], env, Rel.trivial_guard, []) bs' c bs in
                   let envbody, letrecs = if Options.should_verify env.curmodule.str then mk_letrec_environment bs envbody else envbody, [] in
                   let envbody = Tc.Env.set_expected_typ envbody (Util.comp_result c) in
                   Some (t, false), bs, letrecs, Some c, envbody, 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 *)
                  | Typ_refine (b, _) -> 
                    let _, bs, bs', copt, env, g = as_function_typ norm b.sort in
                    Some (t, false), bs, bs', copt, env, g
  
                  | _ -> (* expected type is not a function; 
                            try normalizing it first; 
  