This PR improves the logic and performance of the
`checkImpossibleInstance` function to detect more arguments that are
impossible to
infer for typeclass synthesis. It also improves the formatting of the
error messages for `checkImpossibleInstance` and `checkNonClassInstance`
to be more readable.
This integrates [independent (temporarily merged)
work](https://github.com/leanprover-community/batteries/pull/1717) on
these former Batteries linters which has been reverted in Batteries
because of the unprecedented upstreaming of these linters.
We also disable these checks (if the declaration contains any `sorry`s
so that partially completing instances is still possible without being
terrorized by obvious errors. We also swap the order of the checks, such
that now `checkNonClassInstance` is called first - it would be wrong to
warn for synthesis impossibility if the return type isn't even
synthesizable because it is not class-valued.
Co-authored by: @thorimur
---------
Co-authored-by: Wojciech Rozowski <wojciech@lean-fro.org>
This PR adds two validation checks to `addInstance` that provide early
feedback for common mistakes in instance declarations:
1. **Non-class instance check**: errors when an instance target type is
not a type class. This catches the common mistake of writing `instance`
for a plain structure. Previously handled by the `nonClassInstance`
linter in Batteries (`Batteries.Tactic.Lint.TypeClass`), this is now
checked directly at declaration time.
2. **Impossible argument check**: errors when an instance has arguments
that cannot be inferred by instance synthesis. 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.
Supersedes #13237 and #13333.
