anchor.diff:   *)
   let mk_wp_return env (ed:S.eff_decl) (u_a:universe) (a:typ) (e:term) (r:Range.range)
   : comp
  -= let ret_wp = ed |> U.get_return_vc_combinator in
  -  let wp = mk_Tm_app
  -    (inst_effect_fun_with [u_a] env ed ret_wp)
  -    [S.as_arg a; S.as_arg e]
  -    r in
  -  mk_comp ed u_a a wp [RETURN]
  -
  += let c =
  +    if not <| Env.lid_exists env C.effect_GTot_lid //we're still in prims, not yet having fully defined the primitive effects
  +    then mk_Total a
  +    else if U.is_unit a
  +    then S.mk_Total' a (Some U_zero)
  +    else let wp =
  +           if env.lax
  +           && Options.ml_ish() //NS: Disabling this optimization temporarily
  +           then S.tun
  +           else let ret_wp = ed |> U.get_return_vc_combinator in
  +                N.normalize [Env.Beta; Env.NoFullNorm] env
  +                            (mk_Tm_app (inst_effect_fun_with [u_a] env ed ret_wp)
  +                                       [S.as_arg a; S.as_arg e]
  +                                       e.pos) in
  +         mk_comp ed u_a a wp [RETURN]
  +  in
  +  if debug env <| Options.Other "Return"
  +  then BU.print3 "(%s) returning %s at comp type %s\n"
  +                    (Range.string_of_range e.pos)
  +                    (P.term_to_string e)
  +                    (N.comp_to_string env c);
  +  c
   
   (*
    * Build the M.return comp for an indexed effect
  
positive.code:        | _ -> true)                              &&
       not (should_not_inline_lc lc)                   //condition (d)
  
  let return_value env u_t_opt t v =
    let c =
      if not <| Env.lid_exists env C.effect_GTot_lid //we're still in prims, not yet having fully defined the primitive effects
      then mk_Total t
      else if U.is_unit t
      then S.mk_Total' t (Some U_zero)
      else let m = Env.get_effect_decl env C.effect_PURE_lid in //if Tot isn't fully defined in prims yet, then just return (Total t)
           let u_t =
               match u_t_opt with
               | None -> env.universe_of env t
               | Some u_t -> u_t
           in
           let wp =
              if env.lax
              && Options.ml_ish() //NS: Disabling this optimization temporarily
              then S.tun
              else let ret_wp = m |> U.get_return_vc_combinator in
                   N.normalize [Env.Beta; Env.NoFullNorm]
                              env
                              (mk_Tm_app (inst_effect_fun_with [u_t] env m ret_wp)
                                         [S.as_arg t; S.as_arg v]
                                         v.pos) in
           mk_comp m u_t t wp [RETURN]
    in
    if debug env <| Options.Other "Return"
    then BU.print3 "(%s) returning %s at comp type %s\n"
                      (Range.string_of_range v.pos)
                      (P.term_to_string v)
                      (N.comp_to_string env c);
    c
  
  (* private *)
  
  
negative.code:               //we are not inlining e, rather just adding (fun (x:res_t) -> p x) at the end
                if is_res_t_refinement then
                  let x = S.new_bv (Some res_t.pos) res_t in
                  //AR: build M.return, where M is c's effect
                  let cret, gret = return_value env (c |> U.comp_effect_name |> Env.norm_eff_name env)
                    (comp_univ_opt c) res_t (S.bv_to_name x) in
                    //AR: an M_M bind
                  let lc = bind e.pos env (Some e) (TcComm.lcomp_of_comp c) (Some x, TcComm.lcomp_of_comp cret) in
                  if Env.debug env <| Options.Extreme
                  then BU.print4 "weaken_result_type::strengthen_trivial: inserting a return for e: %s, c: %s, t: %s, and then post return lc: %s\n"
                                 (Print.term_to_string e) (Print.comp_to_string c) (Print.term_to_string t) (TcComm.lcomp_to_string lc);
                  let c, g_lc = TcComm.lcomp_comp lc in
                  set_result_typ c, Env.conj_guards [g_c; gret; g_lc]
                else begin
                  if Env.debug env <| Options.Extreme
                  then BU.print2 "weaken_result_type::strengthen_trivial: res_t:%s is not a refinement, leaving c:%s as is\n"
  