From 5f5d579986e4864147d97523be4f0d01c44ac3fb Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Fri, 24 Nov 2023 19:44:38 +1100 Subject: [PATCH] chore: remove unused MonadBacktrack instance for SimpM (#2943) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit We noticed at https://github.com/leanprover/lean4/pull/2923#discussion_r1400468371 that this instance is not used. It's arguably also incorrect (as it doesn't backtrack the `usedTheorems` field). Seems better to just remove to avoid confusion. Evidence that this is dead code: * After deleting the instance, calling `saveState` in the `SimpM` monad raises an error `failed to synthesize instance MonadBacktrack PUnit SimpM`. * Understanding the `MonadBacktrack` monad leads one to believe that would have happened, via the fact that the only instances for `MonadBacktrack` are either concrete instances (e.g. for `MetaM`, `TacticM`, etc), or a single lifting instance `instance [MonadBacktrack s m] [Monad m] : MonadBacktrack s (ExceptT ε m)`. (This is good and correct behaviour: lifting instances for `MonadBacktrack` would be hard to model.) * Mathlib builds after the instance is removed. Potential evidence that I have not sought, because we don't have sufficient tooling: * Compiling Lean/Std/Mathlib with a debugger, breaking on entering this code. --- src/Lean/Meta/Tactic/Simp/Types.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/Lean/Meta/Tactic/Simp/Types.lean b/src/Lean/Meta/Tactic/Simp/Types.lean index 3247032039..16e08f370f 100644 --- a/src/Lean/Meta/Tactic/Simp/Types.lean +++ b/src/Lean/Meta/Tactic/Simp/Types.lean @@ -45,10 +45,6 @@ structure State where abbrev SimpM := ReaderT Context $ StateRefT State MetaM -instance : MonadBacktrack SavedState SimpM where - saveState := Meta.saveState - restoreState s := s.restore - inductive Step where | visit : Result → Step | done : Result → Step