)]}'
{
  "commit": "e5bda08f9c3daf70515053d7000d5405d256901e",
  "tree": "dca8fae340c31bf6d6193c5fa8e0928cc104392f",
  "parents": [
    "fd0efc4306a7773c2cd4e079ddaa907426d0f5da"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Tue Aug 25 12:25:50 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Tue Aug 25 13:55:09 2026 +0000"
  },
  "message": "fix: try eta-expansion before delta-reduction in the kernel\n\nThis PR fixes `(kernel) deterministic timeout` errors on proof terms whose two sides differ only by eta, such as the ones `simp` produces when rewriting with a function-valued equation. The kernel now answers those definitional equality checks as quickly as `Meta.isDefEq` already did.\n\n`Meta.isExprDefEqExpensive` tries `isDefEqEta` before `whnfCore` and lazy delta-reduction, but `type_checker::is_def_eq_core` only tried `try_eta_expansion` after `lazy_delta_reduction`. So for `f a \u003d?\u003d fun x \u003d\u003e f a x` the kernel delta-normalized `f a` instead of eta-expanding it, and as soon as the unfolded side became a lambda itself, `quick_is_def_eq` committed to `is_def_eq_binding` without backtracking and descended into the normalized subterms. When `f` is a structural recursion over a tree, that is exponential in the tree\u0027s depth: the reproducer in `tests/elab/14803.lean` took 19s at depth 8 and timed out at depth 10, and now takes 0.1s.\n\nSince the kernel has no metavariables, `(fun x \u003d\u003e t) \u003d?\u003d s` holds iff `(fun x \u003d\u003e t) \u003d?\u003d (fun x \u003d\u003e s x)`, so trying eta first cannot lose solutions. The `try_eta_expansion` call after `lazy_delta_reduction` is kept because that reduction updates both sides and may expose a lambda the earlier check did not see.\n\nCloses #14803\n\nCo-authored-by: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "0fae62c2c1a52390cabaa047a3671c77f713bd50",
      "old_mode": 33188,
      "old_path": "src/kernel/type_checker.cpp",
      "new_id": "114f3276514568a35da1f2ec4c00823622cbb169",
      "new_mode": 33188,
      "new_path": "src/kernel/type_checker.cpp"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "a7183fb85a53e0c32dbb42f1a95af59845e077b4",
      "new_mode": 33188,
      "new_path": "tests/elab/14803.lean"
    }
  ]
}