From 1c641b569a1daa25d424bcc9ccc7fcdd83ea0d19 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 10 Feb 2023 12:27:47 -0800
Subject: [PATCH] chore: synthInstance trace message on cache hit

---
 src/Lean/Meta/SynthInstance.lean | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/Lean/Meta/SynthInstance.lean b/src/Lean/Meta/SynthInstance.lean
index b4311ef5d0..d34db08eec 100644
--- a/src/Lean/Meta/SynthInstance.lean
+++ b/src/Lean/Meta/SynthInstance.lean
@@ -672,6 +672,8 @@ private def preprocessOutParam (type : Expr) : MetaM Expr :=
 def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (Option Expr) := do profileitM Exception "typeclass inference" (← getOptions) do
   let opts ← getOptions
   let maxResultSize := maxResultSize?.getD (synthInstance.maxSize.get opts)
+  withTraceNode `Meta.synthInstance
+    (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
   /-
     We disable eta for structures that are not classes during TC resolution because it allows us to find unintended solutions.
     See discussion at
@@ -685,10 +687,10 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
     let type ← preprocess type
     let s ← get
     match s.cache.synthInstance.find? type with
-    | some result => pure result
+    | some result =>
+      trace[Meta.synthInstance] "result {result} (cached)"
+      pure result
     | none        =>
-      withTraceNode `Meta.synthInstance
-        (return m!"{exceptOptionEmoji ·} {← instantiateMVars type}") do
       let result? ← withNewMCtxDepth (allowLevelAssignments := true) do
         let normType ← preprocessOutParam type
         SynthInstance.main normType maxResultSize