anchor.diff:   *
    * This forces the lcomp thunk and recreates it to keep the callers same
    *)
  -let maybe_assume_result_eq_pure_term_in_m env (m_opt:option<lident>) (e:term) (lc:lcomp) : lcomp =
  -  let should_return =
  -      not (env.lax)
  -   && Env.lid_exists env C.effect_GTot_lid //we're not too early in prims
  -   && should_return env (Some e) lc
  -   && not (TcComm.is_lcomp_partial_return lc)
  -  in
  +let assume_result_eq_pure_term_in_m env (m_opt:option<lident>) (e:term) (lc:lcomp) : lcomp =
     (*
      * AR: m is the effect that we are going to do return in
      *)
  
positive.code:         (e2:term)
          (x, lc2)
     : lcomp =
     let lc2 =
          let eff1 = Env.norm_eff_name env lc1.eff_name in
          let eff2 = Env.norm_eff_name env lc2.eff_name in
          if (not (is_pure_or_ghost_effect env eff1)
              || should_not_inline_lc lc1)
          && is_pure_or_ghost_effect env eff2
          then
            let env_x =
              match x with
              | None -> env
              | Some x -> Env.push_bv env x in
            //AR: use c1's effect to return c2 into
            maybe_assume_result_eq_pure_term_in_m env_x (eff1 |> Some) e2 lc2
          else lc2 in //the resulting computation is still pure/ghost and inlineable; no need to insert a return
     bind r env e1opt lc1 (x, lc2)
  
  
negative.code:     if m_opt |> is_none || Options.ml_ish () || is_ghost_effect env lc.eff_name
      then C.effect_PURE_lid
      else m_opt |> must in
  
    let flags =
      if TcComm.is_total_lcomp lc then RETURN::lc.cflags else PARTIAL_RETURN::lc.cflags in
  
    let refine () : comp * guard_t =
        let c, g_c = TcComm.lcomp_comp lc in
        let u_t =
  