debugging typeclass failure involving timeout

Stream: lean4

[Kevin Buzzard]

In this example (uses mathlib) and more generally in the discussion in that thread, a typeclass search for Zero succeeds with some mathlib imports, but starts failing if more mathlib imports are added. With the bad imports and default heartbeats settings, the search times out, and this is hard for me to debug because if Lean times out then it seems reluctant to output a typeclass trace (even though it must have been doing something!).

In desperation, I switched maxHeartbeats and synthInstance.maxHeartbeats to 0 and left it on while I went for dinner, and to my surprise the Zero was found after 608 seconds (on a fast machine!). I then triumphantly put some profiler and instance trace options on, compiled, and piped the output to a file, but to my disappointment I got this (tl;dr: Stack overflow detected. Aborting.), which gives me no useful information. Note that there is no indication of a stack overflow in the actual Lean code, the only indication that something is wrong is that #synth is taking 10 minutes, a time which is an order of magnitude larger than any other instance synthesis I've ever seen in all my years of using mathlib.

Obviously I can chew my pencil here and try and figure out why the two instances I've isolated are sending typeclass inference off on some wild goose chase, but I would rather the machine just told me the answer. Is there any way to see what typeclass inference is doing in the failing case?