Weird reducibility behaviour

Stream: lean4

[Arthur Adjedj]

I've encoutered something weird in regards to reducibility hints and type-class inferece.

abbrev Atom := Nat

instance instAtomDecEq : DecidableEq Atom := inferInstance

#synth DecidableEq Atom --works

attribute [irreducible] Atom

#synth DecidableEq Atom --doesn't work ?

instance : DecidableEq Atom := instAtomDecEq

#synth DecidableEq Atom --works again ?

I would have expected the second #synth to work here, given that instAtomDecEq is there. Is this the intended behaviour ?