anchor.diff:      let guard = if env.top_level || not(Options.should_verify env.curmodule.str) 
                   then (Tc.Util.discharge_guard envbody (Rel.conj_guard g guard); {Rel.trivial_guard with implicits=guard.implicits})
                   else let guard = Rel.close_guard (bs@letrec_binders) guard in Rel.conj_guard g guard in 
  -    let tfun, guard = match tfun_opt with 
  -        | Some t -> 
  +    
  +    let tfun_computed = mk_Typ_fun(bs, cbody) (Some ktype) top.pos in
  +    let e = mk_Exp_abs(bs, body) (Some tfun_computed) top.pos  in
  +
  +    let e, tfun, guard = match tfun_opt with 
  +        | Some (t, use_teq) -> 
              let t = Util.compress_typ t in
              (match t.n with 
  -                | Typ_fun _ -> t, guard
  +                | Typ_fun _ -> 
  +                    //we already checked the body to have the expected type; so, no need to check again
  +                    //just repackage the expression with this type; t is guaranteed to be alpha equivalent to tfun_computed
  +                    mk_Exp_abs(bs, body) (Some t) e.pos, t, guard
                   | _ -> 
  -                    let t' = mk_Typ_fun(bs, cbody) (Some ktype) top.pos in
  -                    if Env.debug env Options.Low
  -                    then Util.fprint2 "Adding an additional equality constraint between\nannotated type %s\nand\ncomputed type %s\n" (Print.typ_to_string t) (Print.typ_to_string t');
  -                    let guard' = Rel.teq env t t' in
  -                    t', Rel.conj_guard guard guard')
  -        | None -> mk_Typ_fun(bs, cbody) (Some ktype) top.pos, guard in
  +                    let e, guard' = 
  +                        if use_teq 
  +                        then e, Rel.teq env t tfun_computed 
  +                        else Tc.Util.check_and_ascribe env e tfun_computed t in
  +                    e, t, Rel.conj_guard guard guard')
  +
  +        | None -> e, tfun_computed, guard in
  +
       if Env.debug env Options.Low
       then Util.fprint3 "!!!!!!!!!!!!!!!Annotating lambda with type %s (%s)\nGuard is %s\n" (Print.typ_to_string tfun) (Print.tag_of_typ tfun) (Rel.guard_to_string env guard);
   
  -    let e = mk_Exp_abs(bs, body) (Some tfun) e.pos  in
  -    let e = mk_Exp_ascribed(e, tfun, Const.effect_Tot_lid |> Some) None e.pos in //Important to ascribe, since the SMT encoding requires the type of every abstraction
  +    let e = mk_Exp_ascribed(e, tfun, Some Const.effect_Tot_lid) None e.pos in //Important to ascribe, since the SMT encoding requires the type of every abstraction
       let c = if env.top_level then mk_Total tfun else Tc.Util.return_value env tfun e in
       let c, g = Tc.Util.strengthen_precondition None env e (Tc.Util.lcomp_of_comp c) guard in
       
  
positive.code:                   if not norm
                    then as_function_typ true (whnf env t) 
                    else let _, bs, _, c_opt, envbody, g = expected_function_typ env None in
                         Some t, bs, [], c_opt, envbody, g in
             as_function_typ false t in
  
      let use_eq = env.use_eq in
  
negative.code: 
    | 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 : (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
  