48729abf4a
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>
47 lines
1.1 KiB
Text
47 lines
1.1 KiB
Text
/-! Registering an instance whose target type is not a class should warn. -/
|
||
|
||
structure Foo where
|
||
x : Nat
|
||
|
||
class Bar where
|
||
x : Nat
|
||
|
||
/--
|
||
error: The declaration `instFoo` should not be an instance as its return type `Foo` is not a type class.
|
||
-/
|
||
#guard_msgs in
|
||
instance instFoo : Foo := ⟨0⟩
|
||
|
||
-- Applying @[instance] to a non-class def should also warn
|
||
def instFoo2 : Foo := ⟨1⟩
|
||
|
||
/--
|
||
error: The declaration `instFoo2` should not be an instance as its return type `Foo` is not a type class.
|
||
-/
|
||
#guard_msgs in
|
||
attribute [instance] instFoo2
|
||
|
||
-- No warning for a proper class instance
|
||
#guard_msgs in
|
||
instance : Bar := ⟨0⟩
|
||
|
||
-- No warning for a class instance with parameters
|
||
class Baz (α : Type) where
|
||
x : α
|
||
|
||
#guard_msgs in
|
||
instance : Baz Nat := ⟨0⟩
|
||
|
||
-- Warning for non-class with parameters
|
||
structure Qux (α : Type) where
|
||
x : α
|
||
|
||
/--
|
||
error: The declaration `instQux` should not be an instance as its return type `Qux Nat` is not a type class.
|
||
-/
|
||
#guard_msgs in
|
||
instance instQux : Qux Nat := ⟨0⟩
|
||
|
||
/-- warning: declaration uses `sorry` -/
|
||
#guard_msgs in
|
||
instance bad : ∀ n : Nat, sorry := by sorry
|