anchor.diff:  let is_pure_effect env l =
     let l = norm_eff_name env l in
     lid_equals l C.effect_PURE_lid
  +
  +let is_ghost_effect env l =
  +  let l = norm_eff_name env l in
  +  lid_equals l C.effect_GHOST_lid
   
   let is_pure_or_ghost_effect env l =
     let l = norm_eff_name env l in
  
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 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)
    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
  