Heterogenous operation triggers CoeHTCT

Stream: lean4

[Tomas Skrivan]

If you write b + a for (a : α) (b : β), Lean will try to synthesize CoeHTCT α β and CoeHTCT β α. Why is this happening? There is an old thread about this, but the problematic instances do not exist anymore.

I'm asking this, because heterogenout operations fail if you add and instance of Coe (Id α) α.

mwe

instance : Coe (Id α) α := ⟨(λ x => x)⟩

variable {α β : Type} (a : α) (b : β) [HAdd β α α]

set_option synthInstance.maxHeartbeats 150
set_option trace.Meta.synthInstance true
#check b + a

The problem is resolved when you replace Coe with CoeHead or CoeHTCT, which one should be used?