Zulip Chat Archive
Stream: lean4
Topic: failed to synthesize instance MonadAlwaysExcept
Jiacheng Chen (Mar 21 2024 at 03:00):
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 (Mar 21 2024 at 03:30):
Sorry, not sure about this corner of things. Maybe we can ping @Sebastian Ullrich who added those lines to the release notes?
Jiacheng Chen (Mar 21 2024 at 03:35):
Sounds good. Thx!
Sebastian Ullrich (Mar 21 2024 at 08:39):
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 (Mar 21 2024 at 08:55):
I have successfully fixed it. Thank you so much! @Sebastian Ullrich
Last updated: May 02 2025 at 03:31 UTC