anchor.diff:  
   
       let rec expected_function_typ env t0 body
  -        : (option<(typ*bool)> (* any remaining expected type to check against; bool signals to check using teq *)
  +        : (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 *)
  
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:                     //just repackage the expression with this type; t is guaranteed to be alpha equivalent to tfun_computed
                      e, t, guard
                  | _ ->
                      let e, guard' = TcUtil.check_and_ascribe env e tfun_computed t in
                      e, t, Rel.conj_guard guard guard'
             end
  
          | None -> e, tfun_computed, guard in
  
      let c = if env.top_level then   mk_Total tfun else TcUtil.return_value env tfun e in
      let c, g = TcUtil.strengthen_precondition None env e (U.lcomp_of_comp c) guard in
      e, c, g
  
  