)]}'
{
  "commit": "cf6043a7191d4f4b64ce4e28f1250d2d91ebe19d",
  "tree": "885c291cd9a3f61b71b10e2f2bdd595d93c35377",
  "parents": [
    "79cf0e44e8aac9aceb09d68a8d2c8078bb10986d"
  ],
  "author": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 11 11:42:07 2026 +0000"
  },
  "committer": {
    "name": "Sebastian Ullrich",
    "email": "sebasti@nullri.ch",
    "time": "Fri Sep 11 12:24:59 2026 +0000"
  },
  "message": "fix: do not hoist `Decidable` values in `pullInstances`\n\nThis PR stops the compiler from hoisting a `Decidable` value out of the branch or thunk it occurs in, which ran the decision procedure even where the source does not. Since #8309 this also affected `if` branches, so for example the pointer-equality shortcut of a hash-consing equality test ran its structural fallback on every comparison.\n\n`pullInstances` pulls every `let` of class type out of `cases` alternatives and lambdas, assuming it is a cheap dictionary. A saturated `Decidable` is instead the outcome of a decision procedure. Lifting out of a `cases` on `Decidable` used to be disabled, which kept such values inside `if` branches as a side effect; #8309 removed that guard once `if` became a `cases` on `Bool`. Lambdas were never covered, so a `Unit` thunk guarding a decision procedure already had it evaluated eagerly.\n\nCo-Authored-By: Claude Opus 5 \u003cnoreply@anthropic.com\u003e\nClaude-Session: https://claude.ai/code/session_01NboqU3PVduLZzJU8kjeh9G\n",
  "tree_diff": [
    {
      "type": "modify",
      "old_id": "f46817a9d195fbc3c49a757f7d1ff7261b036d94",
      "old_mode": 33188,
      "old_path": "src/Lean/Compiler/LCNF/PullLetDecls.lean",
      "new_id": "a3154908375a1319ecce1999c23de04f870aa6ba",
      "new_mode": 33188,
      "new_path": "src/Lean/Compiler/LCNF/PullLetDecls.lean"
    },
    {
      "type": "add",
      "old_id": "0000000000000000000000000000000000000000",
      "old_mode": 0,
      "old_path": "/dev/null",
      "new_id": "ec8346d3f80ea6af63f7b871ed6cb156c9e36966",
      "new_mode": 33188,
      "new_path": "tests/elab/pullInstancesDecidable.lean"
    }
  ]
}