feat: improve tracing messages

src/Init/Lean/Meta/SynthInstance.lean

@@ -159,6 +159,9 @@ do ctx ← read;
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : SynthM Unit :=
 whenM (MonadTracerAdapter.isTracingEnabledFor cls) $ traceCore cls (msg ())
 
+@[inline] def traceM (cls : Name) (mkMsg : SynthM MessageData) : SynthM Unit :=
+whenM (MonadTracerAdapter.isTracingEnabledFor cls) (do msg ← mkMsg; traceCore cls msg)
+
 @[inline] def liftMeta {α} (x : MetaM α) : SynthM α :=
 adaptState (fun (s : State) => (s.toState, s)) (fun s' s => { toState := s', .. s }) x
 
@@ -301,7 +304,7 @@ do mvarType   ← inferType mvar;
   If it succeeds, the result it a new updated metavariable context and a new list of subgoals.
   A subgoal is created for each instance implicit parameter of `inst`. -/
 def tryResolve (mctx : MetavarContext) (mvar : Expr) (inst : Expr) : SynthM (Option (MetavarContext × List Expr)) :=
-withMCtx mctx $ tryResolveCore mvar inst
+traceCtx `Meta.synthInstance.tryResolve $ withMCtx mctx $ tryResolveCore mvar inst
 
 /--
   Assign a precomputed answer to `mvar`.
@@ -330,6 +333,7 @@ def wakeUp (answer : Answer) : Waiter → SynthM Unit
   And then, store it in the tabled entries map, and wakeup waiters. -/
 def addAnswer (cNode : ConsumerNode) : SynthM Unit :=
 do answer ← withMCtx cNode.mctx $ do {
+     traceM `Meta.synthInstance.newAnswer $ do { mvarType ← inferType cNode.mvar; pure mvarType };
      val ← instantiateMVars cNode.mvar;
      abstractMVars val -- assignable metavariables become parameters
    };
@@ -399,7 +403,13 @@ do (cNode, answer) ← getNextToResume;
      result? ← tryAnswer cNode.mctx mvar answer;
      match result? with
      | none      => pure ()
-     | some mctx => consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx := mctx }
+     | some mctx => do
+       withMCtx mctx $ traceM `Meta.synthInstance.resume $ do {
+         goal    ← inferType cNode.mvar;
+         subgoal ← inferType mvar;
+         pure (goal ++ " <== " ++ subgoal)
+       };
+       consume { key := cNode.key, mvar := cNode.mvar, subgoals := rest, mctx := mctx }
 
 def step : SynthM Bool :=
 do s ← get;
@@ -560,6 +570,7 @@ do registerTraceClass `Meta.synthInstance;
    registerTraceClass `Meta.synthInstance.globalInstances;
    registerTraceClass `Meta.synthInstance.newSubgoal;
    registerTraceClass `Meta.synthInstance.tryResolve;
+   registerTraceClass `Meta.synthInstance.resume;
    registerTraceClass `Meta.synthInstance.generate
 
 end Meta

src/Init/Lean/Util/Trace.lean

@@ -42,6 +42,9 @@ modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg)
 @[inline] protected def trace (cls : Name) (msg : Unit → MessageData) : m Unit :=
 whenM (isTracingEnabledFor cls) (addTrace cls (msg ()))
 
+@[inline] protected def traceM (cls : Name) (mkMsg : m MessageData) : m Unit :=
+whenM (isTracingEnabledFor cls) (do msg ← mkMsg; addTrace cls msg)
+
 @[inline] def traceCtx (cls : Name) (ctx : m α) : m α :=
 do b ← isTracingEnabledFor cls;
    if !b then do old ← enableTracing false; a ← ctx; enableTracing old; pure a

tests/lean/run/synth1.lean

@@ -0,0 +1,37 @@
+import Init.Lean.Meta
+open Lean
+open Lean.Meta
+
+class HasCoerce (a b : Type) :=
+(coerce : a → b)
+
+def coerce {a b : Type} [HasCoerce a b] : a → b :=
+@HasCoerce.coerce a b _
+
+instance coerceTrans {a b c : Type} [HasCoerce b c] [HasCoerce a b] : HasCoerce a c :=
+⟨fun x => coerce (coerce x : b)⟩
+
+instance coerceBoolToProp : HasCoerce Bool Prop :=
+⟨fun y => y = true⟩
+
+instance coerceDecidableEq (x : Bool) : Decidable (coerce x) :=
+inferInstanceAs (Decidable (x = true))
+
+instance coerceNatToBool : HasCoerce Nat Bool :=
+⟨fun x => x == 0⟩
+
+instance coerceNatToInt : HasCoerce Nat Int :=
+⟨fun x => Int.ofNat x⟩
+
+def print {α} [HasToString α] (a : α) : MetaM Unit :=
+trace! `Meta.synthInstance (toString a)
+
+set_option trace.Meta.synthInstance true
+set_option trace.Meta.synthInstance.tryResolve false
+
+def tst1 : MetaM Unit :=
+do inst ← mkAppM `HasCoerce #[mkConst `Nat, mkSort levelZero];
+   r ← synthInstance inst;
+   print r
+
+#eval tst1