Feature request: clearer error message from `step*` when missing a basic preamble proof step

[mdittmer]

structure Gate where
  limit : Std.U32
  «open» : Bool

def is_open (gate : Gate) : Result Bool := do
  ok gate.«open»

@[step]
theorem is_open_is_sound (gate : Gate) : is_open gate ⦃ r => True ⦄ := by
  step*

yields error message

fail to show termination for
  is_open_is_sound
with errors
failed to infer structural recursion:
Not considering parameter gate of is_open_is_sound:
  it is unchanged in the recursive calls
no parameters suitable for structural recursion

well-founded recursion cannot be used, `is_open_is_sound` does not take any (non-fixed) arguments

which does not give a very clear indication of what went wrong and what to do about it. To be fair, this was a naive proof attempt that is fixed by replacing step* with unfold is_open; step*, but a more helpful error message would be nice.

[sonmarcho]

Yes, this has been a quite annoying issue. But I'm not sure how to fix it because it's unclear how to detect that we're doing a recursive call in a situation where we shouldn't because the user forgot to unfold the definition first.

[oliver-butterley]

Related but tangential, would it be more comfortable UX to write step* [is_open] (or something like this) rather than unfold is_open; step*? I often forgot the relevant unfold and have been confused by the error.