Understanding trace.Meta.synthInstance

Stream: lean4

[Filippo A. E. Nuccio]

When I look at the output of

set_option trace.Meta.synthInstance true in
example : 0 = 0 := rfl

I see a strange (to my eyes...) behaviour. Lean is trying to infer two OfNat ?m 0 instances, to make sense of the two 0's, and this makes sense. What I do not understand is

1. Why is it trying twice both for the first and for the second 0? Indeed, on the left, it tries both a OfNat ?m.4 0 and a OfNat ?m.35 0; and both a OfNat ?m.18 0 and a OfNat? m.35 0 on the right (of course, the values 4, 18, 35 might vary).

My trial Perhaps what launches the instance search is actually the = sign, and Lean is trying both with HEq and with Eq: in the first case it looks for two types to which the two zeros should belong (m.4 and m.18), in the second for just one type (m.35).

Comment I guess my trial is false, if I replace the statement with example : 0 ≤ 0 := sorry I still get the same behaviour (plus the one for LE, of course), although HLE does not exist...

2. At any rate, I do not understand why after some trials for the left-hand 0 it gives up, while for the right-hand one it ends up finding OfNat Nat 0. Not only is not clear to me where this asymmetry comes from, but also how can it be happy having only found the instance on the RHS and having abandoned the LHS to its fate...

[Eric Wieser]

(I'll briefly hijack this thread to suggest upvoting lean4#6389, which causes trace.Meta.synthInstance to be much harder to read than it was supposed to be)

[Edward van de Meent]

(the indistinguishability of issue numbers vs pr numbers really doesn't help with reading that sentence)