Elaboration bug?

Stream: lean4

[Marcus Rossel]

The following definition of elabSketch gets stuck on elaboration. Changing basically anything about the function makes it unstuck. Is this a bug in elaboration?

import Lean
open Lean Meta Elab Term

inductive Sketch where
  | any
  | expr (e : Expr)
  | app (fn arg : Sketch)
  | contains (sketch : Sketch)
  | or (sketch₁ sketch₂ : Sketch)

def Sketch.containsMDataName : Name := `Sketch.containsMDataName
def Sketch.orLhsMDataName    : Name := `Sketch.orLhsMDataName
def Sketch.orRhsMDataName    : Name := `Sketch.orRhsMDataName

def Lean.KVMap.containsSketch (kv : KVMap) : Bool :=
  kv.contains Sketch.containsMDataName
  || kv.contains Sketch.orLhsMDataName
  || kv.contains Sketch.orRhsMDataName

def Lean.Expr.containsSketchGadget : Expr → Bool
  | .mdata data e =>
    data.containsSketch || e.containsSketchGadget
  | .app e₁ e₂ | .lam _ e₁ e₂ _ | .forallE _ e₁ e₂ _ =>
    e₁.containsSketchGadget || e₂.containsSketchGadget
  | .letE _ e₁ e₂ e₃ _ =>
    e₁.containsSketchGadget || e₂.containsSketchGadget || e₃.containsSketchGadget
  | _ =>
    false

private def Sketch.containsMData (t : Term) : KVMap :=
  { : KVMap }.setSyntax Sketch.containsMDataName t

private def Sketch.orMData (lhs rhs : Term) : KVMap :=
  { : KVMap } |>.setSyntax Sketch.orLhsMDataName lhs |>.setSyntax Sketch.orRhsMDataName rhs

syntax "[" term "]ₛ" : term        -- Sketch.contains
syntax:min term " |ₛ " term : term -- Sketch.or

elab_rules : term
  | `([$t:term]ₛ)             => return .mdata (Sketch.containsMData t) (← mkFreshExprMVar none)
  | `($lhs:term |ₛ $rhs:term) => return .mdata (Sketch.orMData lhs rhs) (← mkFreshExprMVar none)

partial def elabSketch (stx : TSyntax `term) : TermElabM Sketch := do
  let e ← withoutErrToSorry do elabTerm stx none
  go e
where
  go : Expr → TermElabM Sketch
    | .mvar id                                     => goMVar id
    | .mdata data e                                => goMData data e
    | e@(.lam ..) | e@(.forallE ..) | e@(.letE ..) => goBinder e
    | e                                            => return .expr e
  goMVar (mvarId : MVarId) : TermElabM Sketch := do
    if let some e ← getExprMVarAssignment? mvarId then
      go e
    else
      return .any
  goMData (data : KVMap) (e : Expr) : TermElabM Sketch := do
    if let some (.ofSyntax cont) := data.find Sketch.containsMDataName then
      let s ← elabSketch ⟨cont⟩
      return .contains s
    if let some (.ofSyntax orLhs) := data.find Sketch.orLhsMDataName then
      if let some (.ofSyntax orRhs) := data.find Sketch.orRhsMDataName then
        let lhs ← elabSketch ⟨orLhs⟩
        let rhs ← elabSketch ⟨orRhs⟩
        return .or lhs rhs
    return .expr e
  goBinder (e : Expr) : TermElabM Sketch := do
    if e.containsSketchGadget then
      throwErrorAt stx "sketches may not appear under binders"
    else
      return .expr e

[Marcus Rossel]

Inlining goMVar seems to fix the issue.