anchor.diff:            as_function_typ false t
       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 *)
       let env, topt = Env.clear_expected_typ env in
   
       if Env.debug env Options.High
  
positive.code:                                                   S.range_of_bv hd))
                      | _ -> ()
                 end;
                 let expected_t = SS.subst subst hd_expected.sort in
                 let t, g = match (U.unmeta hd.sort).n with
                      | Tm_unknown -> expected_t, g
                      | _ ->
                        if Env.debug env Options.High then BU.print1 "Checking binder %s\n" (Print.bv_to_string hd);
                        let t, _, g1 = tc_tot_or_gtot_term env hd.sort in
  
negative.code:     let env = instantiate_both env in
      match top.n with
          | Tm_let((true, lbs), e2) ->
             (* replace bound variables in terms and of universes with new names (free variables) *)
  (*open*)   let lbs, e2 = SS.open_let_rec lbs e2 in
  
             (* expected types for top level definitions are stored in the lbs and we therefore just
              * remove previous, unrelated, expected type in env
              * the expected type is defined within lbs
              * *)
             let env0, topt = Env.clear_expected_typ env in
             let lbs, rec_env = build_let_rec_env true env0 lbs in
             (* now we type check each let rec *)
             let lbs, g_lbs = check_let_recs rec_env lbs in
             let g_lbs = Rel.solve_deferred_constraints env g_lbs |> Rel.resolve_implicits in
  
  