feat: add a check for impossible arguments in instance definitions

[wkrozowski]

This PR adds a check in addInstance that detects arguments which cannot be inferred by the instance synthesis algorithm. Specifically, it flags arguments that are not instance-implicit and do not appear in any subsequent instance-implicit argument or in the return type. Previously, such instances would be silently accepted but could never be synthesised.

[wkrozowski]

!bench

[leanprover-radar]

Benchmark results for ffa2210 against e44351a are in. Significant changes detected! @wkrozowski

• 🟥 build exited with code 2
• 🟥 other exited with code 2

No significant changes detected.

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e44351add937efe4d286669ccd4c33023ca2e60e --onto 4f6bcc5adac8d6234a9e3def3675402cb89823c6. You can force Mathlib CI using the force-mathlib-ci label. (2026-04-08 17:08:10)

[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 e44351add937efe4d286669ccd4c33023ca2e60e --onto 861bc19e0c1c45b5766cc5c9ef0488568368b236. You can force reference manual CI using the force-manual-ci label. (2026-04-08 17:08:12)