Diamond in MonadExcept

Stream: lean4

[Adam Topaz]

I came across a diamond in core for MonadExcept Exception TacticM. I'm happy to work around it in my current application, and i don't expect anything to be done, but I just wanted to make sure that this is mentioned somewhere.

import Lean

open Lean Elab Tactic

example :
    (inferInstance : MonadExcept Exception TacticM) =
    (instMonadExceptOfMonadExceptOf Exception TacticM) :=
  rfl -- Fails

[Adam Topaz]

I came across this because I had some functions that assumed MonadExcept E M, and a function later on that assumed MonadError M. Now, MonadError M implies MonadExceptOf Exception M which implies MonadExcept Exception M, so I ended up with two nondefeq instances when I tried to apply things to M = TacticM.

[Eric Wieser]

Concerningly this means you can get the wrong catch behavior:

import Lean

open Lean Elab Tactic

example :
    (inferInstance : MonadExcept Exception TacticM) =
    (instMonadExceptOfMonadExceptOf Exception TacticM) := by
  dsimp [instMonadExceptOfMonadExceptOf, inferInstance, instMonadExceptExceptionTacticM, throwThe, throw, tryCatchThe]
  congr
  rfl -- Fails

[Eric Wieser]

A lot of annoying unfolding gets you to

import Lean

open Lean Elab Tactic

example :
    (inferInstance : MonadExcept Exception TacticM) =
    (instMonadExceptOfMonadExceptOf Exception TacticM) := by
  dsimp [instMonadExceptOfMonadExceptOf, inferInstance, instMonadExceptExceptionTacticM, ReaderT.instMonadExceptOf, throwThe, throw, tryCatchThe,
    StateRefT'.instMonadExceptOf, instMonadLiftTOfMonadLift, ReaderT.instMonadLift, liftM, tryCatchThe]
  unfold tryCatchThe
  dsimp [instMonadExceptOfExceptionCoreM, Tactic.tryCatchRestore]
  unfold Tactic.tryCatchRestore instMonadExceptOfMonadExceptOf ReaderT.instMonadExceptOf tryCatchThe StateRefT'.instMonadExceptOf
  dsimp [instMonadExceptOfExceptionCoreM, Tactic.tryCatchRestore]
  unfold tryCatchThe
  dsimp [instMonadExceptOfExceptionCoreM, Tactic.tryCatchRestore]
  /--
  ⊢ { throw := fun {α} => throwThe Exception,
    tryCatch := fun {α} x h => do
      let b ← saveState
      fun r s r_1 s_1 r_2 s_2 =>
        Core.tryCatch (x r s r_1 s_1 r_2 s_2) fun e => (b.restore >>= fun x => h e) r s r_1 s_1 r_2 s_2 } =
  { throw := fun {α} => throwThe Exception,
    tryCatch := fun {α} x handle r s r_1 s_1 r_2 s_2 =>
      Core.tryCatch (x r s r_1 s_1 r_2 s_2) fun e => handle e r s r_1 s_1 r_2 s_2 }
  -/

[Eric Wieser]

So if you write [MonadExcept Exception m] then catch means "restore the state on failure", but if you write [MonadExceptOf Exception m] then it doesn't