Some grind suggestions result in `try sorry`

Stream: lean4

[Plamen Dimitrov]

If I try a simple reproducer like

def anum34 : (mkRat 3 4).num = 3 := by grind?

this will result in

Try this:
  [apply] grind => sorry

Shouldn't grind instead fail with an error message as it does in all other cases? Suggesting to try sorry sounds like a gimmick of some sort.