Grind bug: success depends on the order of hypothesis?

Stream: lean4

[Théophile]

I noticed a weird behavior with grind, where it would fail on a super simple proof, but if we swap the order of the hypothesis, then it works. Should I open an issue about it, or am I missing something?

I tried to minimize as much as I could, here is the #mwe:

-- note: if we use only one constructor, the bug disappear
inductive T (a:Type) where
  | constuctor1: T a
  | constuctor2: T a

-- note: if we replace ≤ by a function T.rel, the bug disappear
instance : LE (T a) where
  le := sorry

axiom L: Type
axiom L.pred (l1: L) (t: T α): Prop

-- L.pred stays true when t gets bigger
-- note: if we replace α by Unit, the bug disappear
axiom L.pred_le (l1: L) (t1 t2: T α):
  t1 ≤ t2 → l1.pred t1 → l1.pred t2
grind_pattern L.pred_le => t1 ≤ t2, l1.pred t1

-- from now on, no need for the α to trigger the bug
abbrev T' := T Unit

axiom l (t: T'): L

-- l keeps the same value when t gets bigger
axiom l_le (t1 t2: T'):
  t1 ≤ t2 → l t1 = l t2
grind_pattern l_le => t1 ≤ t2, l t1

-- construction using l and L.pred
abbrev pred (t: T'): Prop :=
  (l t).pred t

-- `pred` stays true when the t grows, `grind` works well
example: t1 ≤ t2 → pred t1 → pred t2 := by
  grind

-- however if we swap the two hypothesis, `grind` fails
-- looking at the e-matching lemmas, L.pred didn't instantiate
example: pred t1 → t1 ≤ t2 → pred t2 := by
  fail_if_success grind -- bug
  -- to make it work, we can swap the hypothesis order
  intro h1 h2
  revert h1
  grind

-- however, if we put the (swapped) hypothesis in an auxiliary predicate, it works again
def is_mono (p: T' → Prop): Prop :=
  ∀ t1 t2,
    p t1 → t1 ≤ t2 → p t2

example: is_mono pred := by
  grind [is_mono]

-- and if we unfold `is_mono` before calling `grind`, it fails again
example: is_mono pred := by
  unfold is_mono
  fail_if_success grind -- bug
  -- need to swap hypothesis to make grind work
  intro t1 t2 h1 h2
  revert h1
  grind

[Kenny Lau]

@Théophile https://github.com/leanprover/lean4/issues/9825

[Bryan Gin-ge Chen]

This is probably different since grind fails deterministically here as far as I can tell.

[Henrik Böving]

Could you open an issue about this please?

[Théophile]

Done https://github.com/leanprover/lean4/issues/9856

[Kim Morrison]

(Just noting that this is now fixed, and will be in the v4.23.0-rc1 release later this week.)

[Kenny Lau]

what was the fix, for my curiosity?

[Henrik Böving]

Its attached at the issue