anchor.diff:          * 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 *)
  -        * option<term>        (* a tactic to apply when checking the expected computation type *)
           * Env.env             (* environment for the body *)
           * term                (* the body itself *)
           * guard_t)            (* accumulated guard from checking the binders *)
  
positive.code:               | _ -> failwith "Impossible: Can't have a let rec annotation but no expected type"
            in
            let bs, envbody, g, _ = tc_binders env bs in
            let copt, tacopt, body, g = match (SS.compress body).n with
                | Tm_ascribed(e, (Inr c, tacopt), _) ->
                  let c, _, g' = tc_comp envbody c in
                  Some c, tc_tactic_opt envbody tacopt, body, Rel.conj_guard g g'
                | _ -> None, None, body, g
            in
            None, bs, [], copt, tacopt, envbody, body, g
  
        | Some t ->
            let t = SS.compress t in
  
negative.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, 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, env, body, g = as_function_typ norm b.sort in
                  Some t, bs, bs', copt, env, body, g
  
                | Tm_arrow(bs_expected, c_expected) ->
                  let bs_expected, c_expected = SS.open_comp bs_expected c_expected in
  