trace messages for type class resolution instantiate metavariables that they shouldn't

Description

The type class trace messages sometimes show assignments to metavariables that they shouldn't.

In particular this applies to

• The outer trace node indicating the goal of the type class search
• "apply {inst.val} to {mvar}"
• withTraceNodeBefore `Meta.synthInstance.tryResolve (do
  return m!"{mvarTypeBody} ≟ {instTypeBody}")

Context

When using

set_option trace.Meta.synthInstance true

Steps to Reproduce

write

set_option trace.Meta.synthInstance true

#synth HAdd Nat Nat _

Expected behavior:
trace shows

[Meta.synthInstance] ✅ HAdd Nat Nat ?m.4 ▼
  [] new goal HAdd Nat Nat _tc.0 ▼
    [instances] #[@instHAdd] 
  [] ✅ apply @instHAdd to HAdd Nat Nat ?m.5 ▼
    [tryResolve] ✅ HAdd Nat Nat ?m.5 ≟ HAdd ?m.8 ?m.8 ?m.8 
    [] new goal Add Nat ▼
      [instances] #[instAddNat] 
  [] ✅ apply instAddNat to Add Nat ▼
    [tryResolve] ✅ Add Nat ≟ Add Nat 
    [answer] ✅ Add Nat 
  [resume] propagating Add Nat to subgoal Add Nat of HAdd Nat Nat Nat ▼
    [] size: 1 
    [answer] ✅ HAdd Nat Nat Nat 
  [] result instHAdd 

Actual behavior:
trace shows

[Meta.synthInstance] ✅ HAdd Nat Nat Nat ▼
  [] new goal HAdd Nat Nat _tc.0 ▼
    [instances] #[@instHAdd] 
  [] ✅ apply @instHAdd to HAdd Nat Nat Nat ▼
    [tryResolve] ✅ HAdd Nat Nat Nat ≟ HAdd Nat Nat Nat 
    [] new goal Add Nat ▼
      [instances] #[instAddNat] 
  [] ✅ apply instAddNat to Add Nat ▼
    [tryResolve] ✅ Add Nat ≟ Add Nat 
  [resume] propagating Add Nat to subgoal Add Nat of HAdd Nat Nat Nat ▼
    [] size: 1 
  [] result instHAdd 

Versions

All (4.8.0)

isDefEq faces the same problem, but does it correctly
It can be fixed using withTraceNodeBefore, or withMCtx mctxBefore do addMessageContext
I fix this here #4277.

Start with the Meta.synthInstance trace path and reproduce the issue using set_option trace.Meta.synthInstance true and #synth HAdd Nat Nat _. Compare the outer goal, apply, and tryResolve messages with the expected trace, and inspect withTraceNodeBefore, withMCtx, and addMessageContext; done means those messages no longer show assignments from the surrounding metavariable context.