508a113242
This PR adds infrastructure to help diagnose cases where tactics like `unfold` leave the goal in a state that is type-correct only at `.default` transparency, causing `rw`/`simp` to fail at `.instances` transparency. Changes: - Add a `transparency` parameter to `Meta.check` (defaults to `.all`) - Add `withInstancesTypeCheckNote` which appends a lazy note to tactic errors when the target is not type-correct at `.instances` - Wrap `rw`, `simp`, `dsimp`, and `simp_all` at the Elab level - Add opt-in `linter.tacticCheckInstances` that proactively checks every tactic goal and reports semireducible defs that should be marked `@[implicit_reducible]`, using diagnostic counter diffing between `.default` and `.instances` checks
55 lines
1.5 KiB
Text
55 lines
1.5 KiB
Text
module
|
|
|
|
structure S where
|
|
decls : Array Nat
|
|
|
|
structure E where
|
|
s : S
|
|
|
|
structure Inp (s : S) where
|
|
x : Nat
|
|
|
|
def myF (s : S) (_ : Inp s) : E := ⟨s⟩
|
|
|
|
def composed (s : S) (a b : Nat) : E :=
|
|
let res := myF s ⟨a⟩
|
|
myF res.s ⟨b⟩
|
|
|
|
-- Sanity check: with the linter off (default), no warning is emitted.
|
|
#guard_msgs in
|
|
set_option warn.sorry false in
|
|
example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size)
|
|
(h2 : idx < (composed s a b).s.decls.size) :
|
|
(composed s a b).s.decls[idx]'h2 = s.decls[idx]'h1 := by
|
|
unfold composed
|
|
sorry
|
|
|
|
set_option linter.tacticCheckInstances true
|
|
|
|
/--
|
|
@ +4:2...17
|
|
warning: produced tactic goal is not type-correct at `.instances` transparency; consider using propositional rewriting or marking some of the following as `@[implicit_reducible]`:
|
|
composed
|
|
myF
|
|
|
|
Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size)
|
|
(h2 : idx < (composed s a b).s.decls.size) :
|
|
(composed s a b).s.decls[idx]'h2 = s.decls[idx]'h1 := by
|
|
unfold composed
|
|
rfl
|
|
|
|
/--
|
|
@ +3:2...5
|
|
warning: initial tactic goal is not type-correct at `.instances` transparency; consider rephrasing the goal or marking some of the following as `@[implicit_reducible]`:
|
|
composed
|
|
myF
|
|
|
|
Note: This linter can be disabled with `set_option linter.tacticCheckInstances false`
|
|
-/
|
|
#guard_msgs (positions := true) in
|
|
example (s : S) (a b idx : Nat) (h1 : idx < s.decls.size) :
|
|
(composed s a b).s.decls[idx] = s.decls[idx] := by
|
|
rfl
|