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>
71 lines
2.5 KiB
Text
71 lines
2.5 KiB
Text
class MyClass (α : Type u) where
|
||
point : α
|
||
|
||
/--
|
||
error: This instance has 1 argument that cannot be inferred using typeclass synthesis. Specifically
|
||
|
||
argument 3: `(n : Nat)`
|
||
|
||
These arguments are not instance-implicit and appear neither in another instance-implicit argument nor the return type, so they cannot be inferred using typeclass synthesis.
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
instance bad1 {α : Type} [Inhabited α] (n : Nat) : MyClass α := sorry
|
||
|
||
/--
|
||
error: This instance has 2 arguments that cannot be inferred using typeclass synthesis. Specifically
|
||
|
||
argument 3: `(n : Nat)`
|
||
argument 4: `(m : Nat)`
|
||
|
||
These arguments are not instance-implicit and appear neither in another instance-implicit argument nor the return type, so they cannot be inferred using typeclass synthesis.
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
instance bad2 {α : Type} [Inhabited α] (n m : Nat) : MyClass α := sorry
|
||
|
||
/-- warning: declaration uses `sorry` -/
|
||
#guard_msgs in
|
||
instance good {α : Type} [Inhabited α] : MyClass α := sorry
|
||
|
||
/--
|
||
error: This instance has 4 arguments that cannot be inferred using typeclass synthesis. Specifically
|
||
|
||
argument 2: `{β : Type}`
|
||
argument 3: `(b : Array β)`
|
||
argument 4: `(a : Array α)`
|
||
argument 6: `⦃h : b = b⦄`
|
||
|
||
These arguments are not instance-implicit and appear neither in another instance-implicit argument nor the return type, so they cannot be inferred using typeclass synthesis.
|
||
---
|
||
warning: declaration uses `sorry`
|
||
-/
|
||
#guard_msgs in
|
||
instance bad3 {α β : Type} (b : Array β) (a : Array α) [Inhabited α]
|
||
⦃h : b = b⦄
|
||
-- Note: `usedA` is a dependency of a dependency of a dependency of the return type
|
||
(usedA : Array α) (i : Fin usedA.size) (j : Fin i.val) :
|
||
Nonempty { ar : Array α // ar.size = j.val } := sorry
|
||
|
||
-- The following checks that the error shows up at line containing `attribute`
|
||
-- (and not at line where the decl is defined).
|
||
/-- warning: declaration uses `sorry` -/
|
||
#guard_msgs in
|
||
@[implicit_reducible]
|
||
def bad4 {α : Type} [Inhabited α] (n : Nat) : MyClass α := sorry
|
||
|
||
/--
|
||
error: This instance has 1 argument that cannot be inferred using typeclass synthesis. Specifically
|
||
|
||
argument 3: `(n : Nat)`
|
||
|
||
These arguments are not instance-implicit and appear neither in another instance-implicit argument nor the return type, so they cannot be inferred using typeclass synthesis.
|
||
-/
|
||
#guard_msgs in
|
||
attribute [instance] bad4
|
||
|
||
/-- warning: declaration uses `sorry` -/
|
||
#guard_msgs in
|
||
instance bad5 : sorry := sorry
|