unfold essentially loops

Stream: lean4

[Sébastien Michelland]

The following piece of code causes unfold to run for time exponential in the length of either string (while constantly allocating memory). Sorry for the somewhat contrived MWE @Leonardo de Moura, I wasn't able to cut it down any further. Confirmed on yesterday's nightly leanprover/lean4:nightly-2022-06-29.

inductive Wrapper where
  | wrap: Wrapper

def Wrapper.extend: Wrapper → (Unit × Unit)
  | .wrap => ((), ())

mutual
inductive Op where
  | mk: String → Block → Op

inductive Assign where
  | mk : String → Op → Assign

inductive Block where
  | mk: Assign → Block
  | empty: Block
end

mutual
def runOp: Op → Wrapper
  | .mk _ r => let r' := runBlock r; .wrap

def runAssign: Assign → Wrapper
  | .mk _ op => runOp op

def runBlock: Block → Wrapper
  | .mk a => runAssign a
  | .empty => .wrap
end

private def b: Assign := .mk "r" (.mk "APrettyLongString" .empty)

theorem bug: (runAssign b).extend.snd = (runAssign b).extend.snd := by
  --unfold b -- extremely slow
  sorry

[Leonardo de Moura]

@Sébastien Michelland Thanks for reporting this issue. I pushed a fix for it.
https://github.com/leanprover/lean4/commit/14260f454b9b73d85aafef5e7be79c58ce4381b5
The problem was not unfold, but type checking the proof generated using unfold in the kernel.
When checking whether s.i and r.i are definitionally equal, the kernel was always trying to reduce them. However, in your example, this is very expensive, and checking whether s and r are definitionally equal first is a better strategy.
I have another commit that also fixes the problem in the isDefEq for the MetaM monad.

[Sébastien Michelland]

Thanks for the super quick fixes, this is helping a ton. Reducing entire projects never felt so worthwhile :)