Commit 2026-02-19 16:06 2c475ec9

feat: make the unusedInstancesInType linters fire when instances are not used outside of proofs in the type (#32440) This PR adjusts the unusedDecidableInType to prevent false negatives on declarations that only use Decidable* hypotheses in proofs that appear in the type. That is, the linter now fires when the Decidable* linter is unused outside of proofs. This PR also changes the warning message to be more direct, and indicates when the instance appears only in a proof (vs. not appearing at all). We exempt some deprecated lemmas in Mathlib.Analysis.Order.Matrix which the linter now fires on. (Presumably, most prior violations had been cleaned up by #10235, which also detected such lemmas.) Note that this took some tinkering to achieve sufficient performance. We use the following novel(?) "dolorous telescope" strategy (so named due to introducing sorrys) to avoid traversing the whole type:

• when encountering an instance binder of concern, telescope to create an fvar.
• when encountering any other binder, instantiate it with sorry.
• as we proceed, collect the free variables from these expressions which do not appear in proofs. Since the instances of concern are the only free variables, free variable collection avoids traversing many subexpressions by checking for hasFVar, which is a computed field accessible in constant time. Perhaps surprisingly, this is (on net) more performant than using eraseProofs and then detecting dependence via bvars. We also implement an Expr-level early exit for most types by checking if they bind any instance of concern first. (This adds a very small overhead to types which do have an instance of concern, but the check is very fast.) This also adds a profiler category to this linter. Note: we still have yet to optimize (pre)-infotree traversal performance, and have yet to avoid proofs that appear in the value of definitions. However, this PR sets us up to do so.