failed to synthesize instance MonadAlwaysExcept

Stream: lean4

[Jiacheng Chen]

I am bumping a repo to latest Lean version (leanprover/lean4:v4.7.0-rc2). But I am stucked in the following codes.

namespace Smt
abbrev ReductionM := ReaderT Config MetaM

def traceReduce [Monad m] (e : Expr) (e' : Except ε Expr) : m MessageData :=
  return m!"{e} ⤳ " ++ match e' with
    | .ok e'   => m!"{e'}"
    | .error _ => m!"{bombEmoji}"

partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : ReductionM Expr :=
  let rec visit (e : Expr) : MonadCacheT Expr Expr ReductionM Expr :=
    checkCache e fun _ => Core.withIncRecDepth <| withTraceNode `Smt.reduce (traceReduce e ·) do
...
end Smt

in withTraceNode ``Smt.reduce (traceReduce e ·) do I got a error msg as follows,

failed to synthesize instance
  MonadAlwaysExcept ?m.66383 (MonadCacheT Expr Expr ReductionM)

I think this error mainly comes from the change of withTraceNode mensioned in https://github.com/leanprover/lean4/blob/master/RELEASES.md saying

Lean.withTraceNode and variants got a stronger MonadAlwaysExcept assumption to fix trace trees not being built on elaboration runtime exceptions. Instances for most elaboration monads built on EIO Exception should be synthesized automatically.

I have no idea about how to fix this error and could you give me some instructions? Thx!

[Kim Morrison]

Sorry, not sure about this corner of things. Maybe we can ping @Sebastian Ullrich who added those lines to the release notes?

[Jiacheng Chen]

Sounds good. Thx!

[Sebastian Ullrich]

The missing instance follows the same structure as the others, you can copy it to your project until it manifests in a release: https://github.com/leanprover/lean4/pull/3726/files#diff-4e819de9d9430729a749ddb68313d355c5f04dce7dfb81e9924661414ad3d1b2R206-R208

[Jiacheng Chen]

I have successfully fixed it. Thank you so much! @Sebastian Ullrich