anchor.diff:                            let u_t_opt = comp_univ_opt c in
                             let x = S.new_bv (Some t.pos) t in
                             let xexp = S.bv_to_name x in
  -                          let cret = return_value env u_t_opt t xexp in
  +                          //AR: M.return
  +                          let cret, gret = return_value env
  +                            (c |> U.comp_effect_name |> Env.norm_eff_name env)
  +                            u_t_opt t xexp in
                             let guard = if apply_guard
                                         then mk_Tm_app f [S.as_arg xexp] f.pos
                                         else f
                             in
                             let eq_ret, _trivial_so_ok_to_discard =
                                 strengthen_precondition (Some <| Err.subtyping_failed env lc.res_typ t)
  -                                                      (Env.set_range env e.pos)
  +                                                      (Env.set_range (Env.push_bvs env [x]) e.pos)
                                                         e  //use e for debugging only
                                                         (TcComm.lcomp_of_comp cret)
                                                         (guard_of_guard_formula <| NonTrivial guard)
                             in
                             let x = {x with sort=lc.res_typ} in
  +                          //AR: M_M bind
                             let c = bind e.pos env (Some e) (TcComm.lcomp_of_comp c) (Some x, eq_ret) in
                             let c, g_lc = TcComm.lcomp_comp c in
                             if Env.debug env <| Options.Extreme
                             then BU.print1 "Strengthened to %s\n" (Normalize.comp_to_string env c);
  -                          c, Env.conj_guard g_c g_lc
  +                          c, Env.conj_guards [g_c; gret; g_lc]
                   end
             in
             let flags = lc.cflags |> List.collect (function
  
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:           | None -> env.universe_of env (U.comp_result c)
        in
        if U.is_tot_or_gtot_comp c
        then //AR: insert a PURE.return, we are in Tot or GTot c
             let retc, g_retc = return_value env C.effect_PURE_lid
               (Some u_t) (U.comp_result c) e in
             let g_c = Env.conj_guard g_c g_retc in
             if not (U.is_pure_comp c) //it started in GTot, so it should end up in Ghost
             then let retc = U.comp_to_comp_typ retc in
                  let retc = {retc with effect_name=C.effect_GHOST_lid; flags=flags} in
                  S.mk_Comp retc, g_c
             else U.comp_set_flags retc flags, g_c
         else //AR: augment c's post-condition with a M.return, where M is c's effect
              let c = Env.unfold_effect_abbrev env c in
              let t = c.result_typ in
              let c = mk_Comp c in
              let x = S.new_bv (Some t.pos) t in
              let xexp = S.bv_to_name x in
              let ret, g_ret = return_value env (c |> U.comp_effect_name) (Some u_t) t xexp in
              let ret = TcComm.lcomp_of_comp <| U.comp_set_flags ret [PARTIAL_RETURN] in
              let eq = U.mk_eq2 u_t t xexp e in
              let eq_ret = weaken_precondition env ret (NonTrivial eq) in
              //AR: this bind is now an M_M bind
              let bind_c, g_bind = TcComm.lcomp_comp (bind e.pos env None (TcComm.lcomp_of_comp c) (Some x, eq_ret)) in
              U.comp_set_flags bind_c flags, Env.conj_guards [g_c; g_ret; g_bind]
    in
    if not should_return then lc
    else TcComm.mk_lcomp lc.eff_name lc.res_typ flags refine
  