Incorrect `MonadControl m (StateRefT' ω σ m)` instance

Prerequisites

• Put an X between the brackets on this line if you have done all of the following:
  • Check that your issue is not already filed.
  • Reduce the issue to a minimal, self-contained, reproducible test case. Avoid dependencies to mathlib4 or std4.

Description

The MonadControl instance for StateRefT' doesn't work as intended. Specifically, the instance is inferred as ReaderT, which means that the state is not restored by restoreM. Consider the following MWE for TacticM = ReaderT Context $ StateRefT State TermElabM, where the ref state is the goal list:

import Lean

open Lean Meta Elab Tactic

def traceNumGoalsInCoreM {α} (k : TacticM α) : TacticM α := do
  let x ← liftWith (m := CoreM) (fun run => run do
    let a ← k
    logInfo m!"{(← getGoals).length}" -- see the number of goals after `k`
    pure a)
  setGoals [] -- should have no effect, since we restore the tactic state created by `k`
  restoreM x

-- The following close the goal due to `setGoals []`, but shouldn't:

elab "test₁" : tactic => traceNumGoalsInCoreM <| pure ()

example : True := by -- (kernel) declaration has metavariables '_example'
  test₁ -- 1

elab "test₂" : tactic => traceNumGoalsInCoreM do
  appendGoals [(← mkFreshExprMVar none).mvarId!]

example : True := by -- (kernel) declaration has metavariables '_example'
  test₂ -- 2

If we add the following instance above traceNumGoalsInCoreM, patterned off of StateT, the tests do not close the goal, but instead match the logged number of goals as intended:

instance (ω σ : Type) (m : Type → Type) [MonadLiftT (ST ω) m] [Monad m] :
    MonadControl m (StateRefT' ω σ m) where
  stM α      := α × σ
  liftWith f := do let s ← get; liftM (f (fun x => x.run s))
  restoreM x := do let (a, s) ← liftM x; set s; pure a

However, I'm not sure if more care needs to be taken to handle the ref.

Note that this also applies to MonadFunctor.

Context

This caused issues when reducing definitions for hint; see this thread for the discovery of the issue, and this thread for discussion on this issue.

Steps to Reproduce

1. Attempt to restore the state of a monad constructed using StateRefT' using restoreM.

Expected behavior: The state is restored.

Actual behavior: The state is not restored.

Versions

4.3.0; persists in 4.6.0-rc1

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.

Locate the StateRefT' MonadControl and MonadFunctor instances, then run the minimal Lean example using traceNumGoalsInCoreM. Compare the behavior of restoreM with the expected goal-list state restoration, including the suggested StateT-patterned instance. Done means the reproduced tests retain the tactic state instead of closing the goal unexpectedly.