simp instance trace

Stream: lean4

[Sebastien Gouezel]

I am trying to get the instance trace of simp calls in Lean4. In the following example, in mythm I get the trace of the first simp call (in A), but not of the second one (in B). Is there a way to access this trace in the current state of the Lean4 vscode extension, or should I just wait?

class MyClass (α : Type) where
  foo1 : α
  foo2 : α

class MyClass2 (α : Type) [MyClass α] where
  foo_eq : (MyClass.foo1 : α) = MyClass.foo2

class MyClass3 (α : Type) [MyClass α] extends MyClass2 α

@[simp] theorem mysimp (α : Type) [MyClass α] [MyClass3 α] : (MyClass.foo1 : α) = MyClass.foo2 :=
MyClass2.foo_eq

set_option trace.Meta.synthInstance true

theorem mythm (α : Type) [MyClass α] [MyClass3 α] (x : α) : x = x := by
  have A : (MyClass.foo1 : α) = MyClass.foo2 by simp
  have B : (MyClass.foo1 : α) = MyClass.foo2 by simp
  rfl

[Sebastien Gouezel]

It must be a caching mechanism: if I modify the example so that the second simp has to make a genuine new search, then I get the instance trace. So everything is fine!