fix: do not hoist `Decidable` values in `pullInstances` This 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. `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. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01NboqU3PVduLZzJU8kjeh9G
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.