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 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 t = Util.compress_typ t in
             (match t.n with 
                  | Typ_fun _ -> 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
      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 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
      
  
negative.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, false), bs, [], c_opt, envbody, g in
             as_function_typ false t in
  
      let use_eq = env.use_eq in
  