Strange `elab_rules` timeout

Stream: lean4

[Damiano Testa]

Dear All,

I came across a behaviour that I find strange. In the code

import Lean.Elab.Tactic.Basic

open Lean Elab.Tactic

def fn : Option (Name × Name) := some (`a, `b)

syntax "stub" : tactic

elab_rules : tactic | `(tactic| stub) => focus do
  let _ := ← getMainGoal
  let (a, b) := fn.getD default
  guard (0 == 0)   -- if you comment the `guard`, then Lean seems to hang
  let _ := ← match a, b with
    | _, `x => return a
    | `x, _ => return a
    | _, _ => throwError "You should not be here!"

commenting the line with guard makes Lean process the elab_rules block forever. With the guard, it is essentially instantaneous.

Is this expected? Am I doing something wrong?

Thanks!

[Mac Malone]

@Damiano Testa This is definitely a bug. Some further minimization:

import Lean.Elab.Tactic.Basic

open Lean Elab.Tactic

def fn : Option (Name × Name) := some (`a, `b)

def hang : TacticM Unit := do
  let (a, b) := fn.getD default
  guard (0 == 0)   -- if you comment the `guard`, then Lean seems to hang
  discard <|
    match a, b with
    | _, `x => return a
    | `x, _ => return a
    | _, _ => throwError "You should not be here!"

This seems to be caused by some interaction between the let pattern match, the second pattern match, the TacticM monad, and the elaborator/compiler.

[Damiano Testa]

Mac, thanks! I think that this is the first time that I think that I found a bug and it actually is not a feature! :smile:

[Sebastian Ullrich]

Filed as lean4#2359