feat: tune the specialization heuristic to prevent useless specs

[hargoniX]

This PR tunes the specialization heuristic by preventing specializations of HO arguments on sole
parameters. This is sensible because we would re-abstract over the parameter later on anyways so
there is not much use in trying to specialize for them.

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 5279d17 against 0e83422 are in! @hargoniX

Major changes (2)

• 🟥 liasolver//instructions: +639.4M (+16.2%)
• ✅ tests/bench/ interpreted//instructions: -7.3G (-3.4%)

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto 5bd331e85d9d110a29fb3367dbb21854010ffcbd. You can force Mathlib CI using the force-mathlib-ci label. (2025-12-02 11:12:20)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 0e83422fb6337985c3354c263a9510cbcb4b1e05 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-12-02 11:12:21)

[hargoniX]

Not specialising declarations marked as @[specialize] is not acceptable. They might be passing concrete type class parameters to other functions inside of them that need to be specialised.