perf: improve lazy_delta_reduction_step heuristic

It addresses a performance issue reported at
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/performance.20of.20equality.20with.20projections.2Fmutual/near/288083209

src/kernel/type_checker.cpp

@@ -828,6 +828,19 @@ void type_checker::cache_failure(expr const & t, expr const & s) {
         m_st->m_failure.insert(mk_pair(s, t));
 }
 
+/**
+\brief Return `some e'` if `e` is of the form `s.<idx> ...` where `s.<idx>` represents a projection,
+and `e` can be reduced using `whnf_core`.
+*/
+optional<expr> type_checker::try_unfold_proj_app(expr const & e) {
+    expr const & f = get_app_fn(e);
+    if (is_proj(f)) {
+        expr e_new = whnf_core(e);
+        return e_new != e ? optional<expr>(e_new) : none_expr();
+    }
+    return none_expr();
+}
+
 /** \brief Perform one lazy delta-reduction step.
      Return
      - l_true if t_n and s_n are definitionally equal.
@@ -841,9 +854,26 @@ auto type_checker::lazy_delta_reduction_step(expr & t_n, expr & s_n) -> reductio
     if (!d_t && !d_s) {
         return reduction_status::DefUnknown;
     } else if (d_t && !d_s) {
-        t_n = whnf_core(*unfold_definition(t_n), false, true);
+        /* If `s_n` is a projection application, we try to unfold it instead.
+           We added this extra test to address a perfomance issue at defeq tests such as
+           ```lean
+           expensive_term =?= instFoo.1 a
+           ```
+           Without this check, we would keep lazy unfolding `expensive_term` (e.g., it contains function
+           defined using well-founded recursion).
+        */
+        if (auto s_n_new = try_unfold_proj_app(s_n)) {
+            s_n = *s_n_new;
+        } else {
+            t_n = whnf_core(*unfold_definition(t_n), false, true);
+        }
     } else if (!d_t && d_s) {
-        s_n = whnf_core(*unfold_definition(s_n), false, true);
+        /* If `t_n` is a projection application, we try to unfold it instead. See comment above. */
+        if (auto t_n_new = try_unfold_proj_app(t_n)) {
+            t_n = *t_n_new;
+        } else {
+            s_n = whnf_core(*unfold_definition(s_n), false, true);
+        }
     } else {
         int c = compare(d_t->get_hints(), d_s->get_hints());
         if (c < 0) {

src/kernel/type_checker.h

@@ -94,6 +94,7 @@ private:
     bool is_def_eq_core(expr const & t, expr const & s);
     /** \brief Like \c check, but ignores undefined universes */
     expr check_ignore_undefined_universes(expr const & e);
+    optional<expr> try_unfold_proj_app(expr const & e);
 
     template<typename F> optional<expr> reduce_bin_nat_op(F const & f, expr const & e);
     template<typename F> optional<expr> reduce_bin_nat_pred(F const & f, expr const & e);

tests/lean/run/lazyUnfoldingPerfIssue.lean

@@ -0,0 +1,96 @@
+namespace Ex1
+
+inductive T: Type :=
+  | mk: String → Option T → T
+
+def runT: T → Nat
+  | .mk _ none => 0
+  | .mk _ (some t) => runT t
+
+class Run (α: Type) where
+  run: α → Nat
+instance: Run T := ⟨runT⟩
+
+def x := T.mk "PrettyLong" (some <| .mk "PrettyLong" none)
+
+theorem equivalent: Run.run x = Run.run x := by
+  -- simp (config := { dsimp := false, decide := false, etaStruct := .none }) [Run.run]
+  apply Eq.refl (runT x)
+
+example : Run.run x = Run.run x := by
+  simp [Run.run]
+
+end Ex1
+
+namespace Ex2
+
+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
+
+end Ex2
+
+namespace Ex3
+
+inductive ProgramType := | Op | Assign | Block
+
+section
+set_option hygiene false
+notation "Op"     => Program ProgramType.Op
+notation "Assign" => Program ProgramType.Assign
+notation "Block"  => Program ProgramType.Block
+end
+
+inductive Program: (type: ProgramType) → Type :=
+  | mkOp: String → Block → Op
+  | mkAssign: String → Op → Assign
+  | mkBlock: Assign → Block
+  | emptyBlock: Block
+
+def runBase: Program type → Nat
+  | .mkOp _ v => let _ := runBase v; 0
+  | .mkAssign _ t => runBase t
+  | .mkBlock u => runBase u
+  | .emptyBlock => 0
+
+class Run (α: Type) where
+  run: α → Nat
+instance: Run Assign := ⟨runBase⟩
+
+def x: Assign := .mkAssign "PrettyLong" <| .mkOp "PrettyLong" .emptyBlock
+-- Now runs fine
+theorem equivalent: Run.run x = Run.run x := by simp [Run.run]
+
+end Ex3