anchor.diff:      let bs, c = SS.open_comp bs c in
       let env0 = env in
       let env, _ = Env.clear_expected_typ env in
  +    (* type checking the binders *)
       let bs, env, g, us = tc_binders env bs in
  +    (* type checking the computation *)
       let c, uc, f = tc_comp env c in
       let e = {U.arrow bs c with pos=top.pos} in
  +    (* checks the SMT pattern associated with this function is properly defined with regard to context *)
       check_smt_pat env e bs c;
  +    (* taking the maximum of the universes of the computation and of all binders *)
       let u = S.U_max (uc::us) in
  +    (* create a universe of level u *)
       let t = mk (Tm_type u) None top.pos in
       let g = Rel.conj_guard g (Rel.close_guard_univs us bs f) in
       value_check_expected_typ env0 e (Inl t) g
  
positive.code:     e, S.mk_Total t |> U.lcomp_of_comp, (Rel.conj_guard g0 g1)
  
    | Tm_name x ->
      let t, rng = 
          if env.use_bv_sorts 
          then x.sort, S.range_of_bv x 
          else Env.lookup_bv env x in
      let x = S.set_range_of_bv ({x with sort=t}) rng in
      FStar.TypeChecker.Common.insert_bv x t;
  
negative.code:           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
  