Reflecting on type class instance search?

Stream: lean4

[David Thrane Christiansen]

Is there a way to write a metaprogram that observes an instance search? I'm working on a written description of how instance search works, and stepping through the intermediate states would be a really nice explanatory tool. But this is only really tenable if I can have a test that keeps it up to date with changes in Lean, like similar ones I use for tracking error messages.

For instance, it would be cool to have a macro like this:

search steps (metas := [m1])
  HMul Int Int m1
  . Mul Int as default

with bullets for the recursive structure of the search, justifications for default instances, etc.

I suspect that this does not exist or would produce absurdly huge traces, but I figured it's worth asking.

[Mauricio Collares]

Is https://github.com/leanprover/lean4/pull/1448 relevant?

[David Thrane Christiansen]

Yes, thanks!