Elab.async changes the result of elaboration with grind

Stream: lean4

[Eric Wieser]

This bug seems to have returned:

structure Wrapper (α) where val : α

instance {α : Type} [NatCast α] : NatCast (Wrapper α) := sorry

def foo {α : Type} (μ : Wrapper α) (f : α → Nat) : Nat := sorry

macro:max P:term noWs "|[" s:term "]|" : term => `(
  let h : $s ≤ List.length $P := by grind
  0)

macro:max P:term noWs "|[" term "]|" : term => `(foo $P fun x => 0)

theorem bar (a : List ℕ) (i : Fin (a.length - 1)) : 0 ≤ a|[i.val + 1]| :=
  Nat.zero_le _

-- statement below is identical
set_option Elab.async false

/--
error: Ambiguous term
  a|[i.val + 1]|
Possible interpretations:
  foo ?m.12 fun x => 0 : Nat
  ⏎
  let h := ?m.21;
  0 : ?m.24
-/
#guard_msgs in
theorem bar' (a : List ℕ) (i : Fin (a.length - 1)) : 0 ≤ a|[i.val + 1]| :=
  Nat.zero_le _

[Eric Wieser]

(the kernel error is no more perhaps thanks to an assert! guarding it, but the behavior change induced by Elab.async persists)

[Eric Wieser]

#10705 is probably relevant still

[Notification Bot]

3 messages were moved here from #lean4 > Kernel error in list index notation by Eric Wieser.