3fc99eef10
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.
19 lines
410 B
Text
19 lines
410 B
Text
structure Foo where
|
|
x : Nat
|
|
y : Nat := 10
|
|
|
|
@[implicit_reducible]
|
|
def f (x : Nat) : Foo :=
|
|
{ x := x + x }
|
|
|
|
@[implicit_reducible]
|
|
def g (x : Nat) : Foo :=
|
|
{ x := x + x }
|
|
|
|
opaque q : Nat → Prop
|
|
|
|
example (h : q (f x).1) : q (g x).1 := by
|
|
-- Projections must not bump transparency setting from `reducible` to `instances`
|
|
-- Thus, the following tactic must fail
|
|
fail_if_success simp [h]
|
|
assumption
|