diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index bcbfd9595f..84e36f784d 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -827,6 +827,7 @@ builtin_initialize
   registerTraceClass `Meta.synthInstance
   registerTraceClass `Meta.synthInstance.instances (inherited := true)
   registerTraceClass `Meta.synthInstance.tryResolve (inherited := true)
+  registerTraceClass `Meta.synthInstance.answer (inherited := true)
   registerTraceClass `Meta.synthInstance.resume (inherited := true)
   registerTraceClass `Meta.synthInstance.unusedArgs
   registerTraceClass `Meta.synthInstance.newAnswer
diff --git a/tests/lean/366.lean.expected.out b/tests/lean/366.lean.expected.out
index 4fa16391e6..966e0ef9b9 100644
--- a/tests/lean/366.lean.expected.out
+++ b/tests/lean/366.lean.expected.out
@@ -3,4 +3,5 @@
     [Meta.synthInstance.instances] #[@instInhabitedOfMonad, instInhabitedNat]
   [Meta.synthInstance] ✅ apply instInhabitedNat to Inhabited Nat
     [Meta.synthInstance.tryResolve] ✅ Inhabited Nat ≟ Inhabited Nat
+    [Meta.synthInstance.answer] ✅ Inhabited Nat
   [Meta.synthInstance] result instInhabitedNat
diff --git a/tests/lean/815b.lean.expected.out b/tests/lean/815b.lean.expected.out
index 3b09b50404..3d5fe6616d 100644
--- a/tests/lean/815b.lean.expected.out
+++ b/tests/lean/815b.lean.expected.out
@@ -27,6 +27,7 @@
       [Meta.synthInstance.instances] #[inst✝]
   [Meta.synthInstance] ✅ apply inst✝ to IsSmooth f
     [Meta.synthInstance.tryResolve] ✅ IsSmooth f ≟ IsSmooth f
+    [Meta.synthInstance.answer] ✅ IsSmooth f
   [Meta.synthInstance.resume] propagating IsSmooth f to subgoal IsSmooth f of ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.resume] size: 1
     [Meta.synthInstance.unusedArgs] α → IsSmooth f
@@ -133,6 +134,7 @@
     [Meta.synthInstance.tryResolve] ❌ IsSmooth fun g => g ≟ IsSmooth fun a => ?m
   [Meta.synthInstance] ✅ apply @identity to IsSmooth fun g => g
     [Meta.synthInstance.tryResolve] ✅ IsSmooth fun g => g ≟ IsSmooth fun a => a
+    [Meta.synthInstance.answer] ✅ IsSmooth fun g => g
   [Meta.synthInstance.resume] propagating IsSmooth fun a =>
         a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 1
@@ -144,9 +146,11 @@
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 2
+    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of IsSmooth fun g => g
     [Meta.synthInstance.resume] size: 3
+    [Meta.synthInstance.answer] ✅ IsSmooth fun g => g
   [Meta.synthInstance.resume] propagating IsSmooth fun b a =>
         b a to subgoal IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 4
@@ -158,18 +162,23 @@
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun b a => b a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 8
+    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating α →
         IsSmooth fun a => a to subgoal α → IsSmooth fun g => g of ∀ (a : α), IsSmooth fun g => g a
     [Meta.synthInstance.resume] size: 5
+    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => g a
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 => a_1 a to subgoal ∀ (a : α), IsSmooth fun g => g a of ∀ (a : α), IsSmooth fun g => f (g a)
     [Meta.synthInstance.resume] size: 4
+    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a)
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 =>
           f (a_1 a) to subgoal ∀ (a : α), IsSmooth fun g => f (g a) of ∀ (a : α), IsSmooth fun g => f (g a) d
     [Meta.synthInstance.resume] size: 5
+    [Meta.synthInstance.answer] ✅ ∀ (a : α), IsSmooth fun g => f (g a) d
   [Meta.synthInstance.resume] propagating ∀ (a : α),
         IsSmooth fun a_1 =>
           f (a_1 a) d to subgoal ∀ (a : α), IsSmooth fun g => f (g a) d of IsSmooth fun g a => f (g a) d
     [Meta.synthInstance.resume] size: 6
+    [Meta.synthInstance.answer] ✅ IsSmooth fun g a => f (g a) d
   [Meta.synthInstance] result swap fun a g => f (g a) d