anchor.diff:            (match topt with | None -> "None" | Some t -> Print.term_to_string t)
             (if env.top_level then "true" else "false");
   
  -    let tfun_opt, bs, letrec_binders, c_opt, envbody, body, g_env = expected_function_typ env topt body in
  +    let tfun_opt, bs, letrec_binders, c_opt, envbody, body, g_env =
  +      tc_abs_expected_function_typ env bs topt body in
   
       if Env.debug env Options.Extreme
       then BU.print3 "After expected_function_typ, tfun_opt: %s, c_opt: %s, and expected type in envbody: %s\n"
  
positive.code:           then u
            else failwith ("Universe variable " ^ (Print.univ_to_string u) ^ " not found")
     in if env.lax_universes then U_zero
        else match u with
             | U_unknown -> U.type_u () |> snd
             | _ -> aux u
  
  (* Several complex cases from the main type-checker are factored in to separate functions below *)
  
  (*******************************************************************************************************************)
  (* Type-checking abstractions, aka lambdas                                                                         *)
  
negative.code:     let fail :string -> typ -> 'a = fun msg t ->
          raise_error (Err.expected_a_term_of_type_t_got_a_function env msg t top) (top.pos) in
  
      
      (* whether to try first to use unification for solving sub-typing constraints or only propagate to the SMT solver *)
      let use_eq = env.use_eq in
      (* topt is the expected type of the expression obtained from the env *)
  