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
104 lines
3.4 KiB
Text
104 lines
3.4 KiB
Text
module
|
|
|
|
set_option backward.isDefEq.respectTransparency.types true
|
|
|
|
/-!
|
|
After `unfold`, the goal may become not type-correct at `instances` transparency
|
|
because hypotheses still refer to the pre-unfolded definition. When `rw`/`simp`
|
|
fails in such a goal, the error message should include a note about the
|
|
type-correctness issue.
|
|
-/
|
|
|
|
structure S where
|
|
decls : Array Nat
|
|
|
|
structure E where
|
|
s : S
|
|
|
|
structure Inp (s : S) where
|
|
x : Nat
|
|
|
|
class C (β : S → Type) (f : (s : S) → β s → E) where
|
|
decl_eq : ∀ (s : S) (input : β s)
|
|
(idx : Nat) (h1 : idx < s.decls.size) (h2 : idx < (f s input).s.decls.size),
|
|
(f s input).s.decls[idx]'h2 = s.decls[idx]'h1
|
|
|
|
def myF (s : S) (_ : Inp s) : E := ⟨s⟩
|
|
|
|
set_option warn.sorry false in
|
|
instance : C Inp myF where
|
|
decl_eq := by intros; sorry
|
|
|
|
def composed (s : S) (a b : Nat) : E :=
|
|
let res := myF s ⟨a⟩
|
|
myF res.s ⟨b⟩
|
|
|
|
section rw
|
|
|
|
-- Without `unfold`, the note should NOT fire (goal is type-correct at `instances`)
|
|
/--
|
|
error: Tactic `rewrite` failed: Did not find an occurrence of the pattern
|
|
(myF ?s ?input).s.decls[?idx]
|
|
in the target expression
|
|
(composed s a b).s.decls[idx] = s.decls[idx]
|
|
|
|
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] = s.decls[idx]
|
|
-/
|
|
#guard_msgs 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
|
|
rw [C.decl_eq (f := myF)]
|
|
|
|
-- With `unfold`, the note SHOULD fire (`h2`'s type no longer matches after unfolding)
|
|
/--
|
|
Note: The target expression is not type-correct under the `instances` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps.
|
|
-/
|
|
#guard_msgs (substring := 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
|
|
rw [C.decl_eq (f := myF)]
|
|
|
|
-- The defeq abuse may already be part of the initial goal.
|
|
/--
|
|
Note: The target expression is not type-correct under the `instances` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps.
|
|
-/
|
|
#guard_msgs (substring := 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
|
|
rw [C.decl_eq (f := myF)]
|
|
|
|
end rw
|
|
|
|
section simp
|
|
|
|
-- Without `unfold`, the note should NOT fire
|
|
/--
|
|
error: `simp` made no progress
|
|
-/
|
|
#guard_msgs 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
|
|
simp (config := { zeta := false })
|
|
|
|
-- With `unfold`, the note SHOULD fire
|
|
/--
|
|
error: `simp` made no progress
|
|
|
|
Note: The target expression is not type-correct under the `instances` transparency level, which may have triggered the failure. This is usually caused by unfolding of semireducible definitions in prior tactic steps. Use `set_option linter.tacticCheckInstances true` to investigate the source of the issue.
|
|
-/
|
|
#guard_msgs 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
|
|
simp (config := { zeta := false })
|
|
|
|
end simp
|