MetaLCtxM and mvar depth

[lecopivo]

There seems to be some odd interaction between MetaLCtxM monad and meta variable depth.

lsimp used to panic on

import SciLean.Tactic.CompiledTactics
import SciLean.Tactic.LSimp.Elab
import SciLean.Util.RewriteBy

variable (i : ℕ)

#check (fun x : ℕ => (if i = 0 then 1 else 0)) rewrite_by lsimp

This panic was fixed in 1d70152 by calling withoutModifyingLCtx before withNewMCtxDepth.

I should investigate what is going on and fix MetatLCtxM accordingly.