anchor.diff:   * else if it is GHOST, the return happens in PURE
    *
    * If caller does not provide the m effect, return happens in PURE
  + *
  + * 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)
  +      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
  +  (*
  +   * AR: m is the effect that we are going to do return in
  +   *)
  +  let m =
  +    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 should_return
       then if TcComm.is_total_lcomp lc
  
positive.code:             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
  
  let maybe_assume_result_eq_pure_term env e lc =
    maybe_assume_result_eq_pure_term_in_m env None e lc
  
negative.code:          else PARTIAL_RETURN::lc.cflags
      else lc.cflags
    in
    let refine () : comp * guard_t =
        let c, g_c = TcComm.lcomp_comp lc in
        let u_t =
            match comp_univ_opt c with
            | Some u_t -> u_t
            | None -> env.universe_of env (U.comp_result c)
        in
        if U.is_tot_or_gtot_comp c
        then //AR: insert an M.return
             let retc, g_retc = return_value env m (Some u_t) (U.comp_result c) e in
  