Is seeing sorryAx a bug?

Stream: lean4

[Jason Gross]

Is it a bug if I get error messages mentioning sorry when I haven't used sorry myself?

instance has_arr : HasArr Preorder := { Arr := Function }
-- unknown identifier 'HasArr'
-- invalid {...} notation, 'sorryAx' is not a structure

[Leonardo de Moura]

I just pushed a fix for this issue.
We have a mechanism for suppressing error messages mentioning "synthetic sorry"s. It failed in this error message because it contained a name/string instead of an expression. It is fixed now.