feat: add MonadExceptCore

src/Init/Control/EState.lean

@@ -116,7 +116,7 @@ instance {δ} [Backtrackable δ σ] : HasOrelse (EStateM ε σ α) :=
 instance : MonadState σ (EStateM ε σ) :=
 { set := @EStateM.set _ _, get := @EStateM.get _ _, modifyGet := @EStateM.modifyGet _ _ }
 
-instance {δ} [Backtrackable δ σ] : MonadExcept ε (EStateM ε σ) :=
+instance {δ} [Backtrackable δ σ] : MonadExceptCore ε (EStateM ε σ) :=
 { throw := @EStateM.throw _ _, catch := @EStateM.catch _ _ _ _ }
 
 @[inline] def adaptState {σ₁ σ₂} (split : σ → σ₁ × σ₂) (merge : σ₁ → σ₂ → σ) (x : EStateM ε σ₁ α) : EStateM ε σ α :=

src/Init/Control/Except.lean

@@ -9,7 +9,7 @@ prelude
 import Init.Control.Alternative
 import Init.Control.Lift
 import Init.Data.ToString
-universes u v w
+universes u v w u'
 
 inductive Except (ε : Type u) (α : Type v)
 | error : ε → Except
@@ -126,10 +126,39 @@ fun x => ExceptT.mk $ Except.mapError f <$> x
 end ExceptT
 
 /-- An implementation of [MonadError](https://hackage.haskell.org/package/mtl-2.2.2/docs/Control-Monad-Except.html#t:MonadError) -/
+class MonadExceptCore (ε : Type u) (m : Type v → Type w) :=
+(throw {α : Type v} : ε → m α)
+(catch {α : Type v} : m α → (ε → m α) → m α)
+
+abbrev throwThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (e : ε) : m α :=
+MonadExceptCore.throw e
+
+abbrev catchThe (ε : Type u) {m : Type v → Type w} [MonadExceptCore ε m] {α : Type v} (x : m α) (handle : ε → m α) : m α :=
+MonadExceptCore.catch x handle
+
+instance ExceptT.monadExceptParent (m : Type u → Type v) (ε₁ : Type u) (ε₂ : Type u) [Monad m] [MonadExceptCore ε₁ m] : MonadExceptCore ε₁ (ExceptT ε₂ m) :=
+{ throw := fun α e        => ExceptT.mk $ throwThe ε₁ e,
+  catch := fun α x handle => ExceptT.mk $ catchThe ε₁ x handle }
+
+instance ExceptT.monadExceptSelf (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExceptCore ε (ExceptT ε m) :=
+{ throw := fun α e => ExceptT.mk $ pure (Except.error e),
+  catch := @ExceptT.catch ε _ _ }
+
+instance (ε) : MonadExceptCore ε (Except ε) :=
+{ throw := fun α => Except.error,
+  catch := @Except.catch _ }
+
+/-- Similar to `MonadExceptCore`, but `ε` is an outParam for convenience -/
 class MonadExcept (ε : outParam (Type u)) (m : Type v → Type w) :=
 (throw {α : Type v} : ε → m α)
 (catch {α : Type v} : m α → (ε → m α) → m α)
 
+export MonadExcept (throw catch)
+
+instance MonadExceptCore.isMonadExcept (ε : outParam (Type u)) (m : Type v → Type w) [MonadExceptCore ε m] : MonadExcept ε m :=
+{ throw := fun _ e        => throwThe ε e,
+  catch := fun _ x handle => catchThe ε x handle }
+
 namespace MonadExcept
 variables {ε : Type u} {m : Type v → Type w}
 
@@ -146,23 +175,13 @@ catch t₁ $ fun e₁ => catch t₂ $ fun e₂ => throw (if useFirstEx then e₁
 
 end MonadExcept
 
-export MonadExcept (throw catch)
-
-instance (m : Type u → Type v) (ε : Type u) [Monad m] : MonadExcept ε (ExceptT ε m) :=
-{ throw := fun α e => ExceptT.mk $ pure (Except.error e),
-  catch := @ExceptT.catch ε _ _ }
-
-instance (ε) : MonadExcept ε (Except ε) :=
-{ throw := fun α => Except.error, catch := @Except.catch _ }
-
 /-- Adapt a Monad stack, changing its top-most error Type.
 
     Note: This class can be seen as a simplification of the more "principled" definition
     ```
     class MonadExceptFunctor (ε ε' : outParam (Type u)) (n n' : Type u → Type u) :=
     (map {α : Type u} : (∀ {m : Type u → Type u} [Monad m], ExceptT ε m α → ExceptT ε' m α) → n α → n' α)
-    ```
--/
+    `` -/
 class MonadExceptAdapter (ε ε' : outParam (Type u)) (m m' : Type u → Type v) :=
 (adaptExcept {α : Type u} : (ε → ε') → m α → m' α)
 export MonadExceptAdapter (adaptExcept)

src/Init/Control/Option.lean

@@ -63,7 +63,7 @@ namespace OptionT
   (do { some a ← ma | (handle ());
         pure a } : m (Option α))
 
-  instance : MonadExcept Unit (OptionT m) :=
+  instance : MonadExceptCore Unit (OptionT m) :=
   { throw := fun _ _ => OptionT.fail, catch := @OptionT.catch _ _ }
 
   instance (m out) [MonadRun out m] : MonadRun (fun α => out (Option α)) (OptionT m) :=

src/Init/Control/Reader.lean

@@ -64,10 +64,10 @@ instance [Alternative m] : Alternative (ReaderT ρ m) :=
   failure := @ReaderT.failure _ _ _ _,
   orelse  := @ReaderT.orelse _ _ _ _ }
 
+instance (ε) [Monad m] [MonadExceptCore ε m] : MonadExceptCore ε (ReaderT ρ m) :=
+{ throw := fun α => ReaderT.lift ∘ throwThe ε,
+  catch := fun α x c r => catchThe ε (x r) (fun e => (c e) r) }
 
-instance (ε) [Monad m] [MonadExcept ε m] : MonadExcept ε (ReaderT ρ m) :=
-{ throw := fun α => ReaderT.lift ∘ throw,
-  catch := fun α x c r => catch (x r) (fun e => (c e) r) }
 end
 end ReaderT
 

src/Init/Control/State.lean

@@ -80,9 +80,10 @@ fun st => do
   (a, st') ← x st;
   pure (a, join st' ctx)
 
-instance (ε) [MonadExcept ε m] : MonadExcept ε (StateT σ m) :=
-{ throw := fun α => StateT.lift ∘ throw,
-  catch := fun α x c s => catch (x s) (fun e => c e s) }
+instance (ε) [MonadExceptCore ε m] : MonadExceptCore ε (StateT σ m) :=
+{ throw := fun α => StateT.lift ∘ throwThe ε,
+  catch := fun α x c s => catchThe ε (x s) (fun e => c e s) }
+
 end
 end StateT
 

src/Init/System/IO.lean

@@ -35,7 +35,7 @@ fun s => match x s with
 | EStateM.Result.error ex s => h ex s
 
 instance (ε : Type) : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
-instance (ε : Type) : MonadExcept ε (EIO ε) := inferInstanceAs (MonadExcept ε (EStateM ε IO.RealWorld))
+instance (ε : Type) : MonadExceptCore ε (EIO ε) := inferInstanceAs (MonadExceptCore ε (EStateM ε IO.RealWorld))
 instance (α ε : Type) : HasOrelse (EIO ε α) := ⟨MonadExcept.orelse⟩
 instance {ε : Type} {α : Type} [Inhabited ε] : Inhabited (EIO ε α) :=
 inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
@@ -68,7 +68,7 @@ constant allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α := arbitra
 @[extern "lean_io_initializing"]
 constant IO.initializing : IO Bool := arbitrary _
 
-class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExcept IO.Error m
+class MonadIO (m : Type → Type) extends HasMonadLiftT IO m, MonadExceptCore IO.Error m
 
 instance : MonadIO IO := {}
 

src/Lean/Elab/Log.lean

@@ -66,10 +66,10 @@ log stx MessageSeverity.warning msgData
 def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit :=
 log stx MessageSeverity.information msgData
 
-def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
+def throwError {α} [MonadPosInfo m] [MonadExceptCore Exception m] (ref : Syntax) (msgData : MessageData) : m α := do
 msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg)
 
-def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do
+def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExceptCore Exception m] (msgData : MessageData) : m α := do
 cmdPos ← getCmdPos;
 msg ← mkMessageAt msgData MessageSeverity.error cmdPos;
 throw (Exception.error msg)

src/Lean/PrettyPrinter/Formatter.lean

@@ -103,6 +103,8 @@ fold (Array.foldl (fun acc f => f ++ acc) Format.nil) x
 def concatArgs (x : FormatterM Unit) : FormatterM Unit :=
 concat (visitArgs x)
 
+set_option class.instance_max_depth 100 -- TODO delete
+
 /--
   Call an appropriate `[formatter]` depending on the `Parser` `Expr` `p`. After the call, the traverser position
   should be to the left of all nodes produced by `p`, or at the left-most child if there are no other nodes left. -/

src/Lean/PrettyPrinter/Parenthesizer.lean

@@ -152,6 +152,8 @@ instance monadQuotation : MonadQuotation ParenthesizerM := {
   withFreshMacroScope := fun α x => x,
 }
 
+set_option class.instance_max_depth 100 -- TODO delete
+
 /-- Run `x` and parenthesize the result using `mkParen` if necessary. -/
 def maybeParenthesize (mkParen : Syntax → Syntax) (prec : Nat) (x : ParenthesizerM Unit) : ParenthesizerM Unit := do
 stx ← getCur;

tests/lean/run/catchThe.lean

@@ -0,0 +1,33 @@
+import Lean.Meta
+open Lean
+open Lean.Meta
+
+universes u v w
+
+abbrev M := ExceptT String $ MetaM
+
+def testM {α} [HasBeq α] [HasToString α] (x : M α) (expected : α)  : MetaM Unit := do
+r ← x;
+match r with
+| Except.ok a    => unless (a == expected) $ throwOther ("unexpected result " ++ toString a)
+| Except.error e => throwOther ("FAILED: " ++ e)
+
+@[noinline] def act1 : M Nat :=
+throwThe Exception $ Exception.other Syntax.missing "Error at act1"
+
+def g1 : M Nat :=
+catchThe Meta.Exception
+  (catch act1 (fun ex => pure 100))
+  (fun ex => pure 200)
+
+#eval testM g1 200
+
+@[noinline] def act2 : M Nat :=
+throw "hello world"
+
+def g2 : M Nat :=
+catchThe Meta.Exception
+  (catch act2 (fun ex => pure 100))
+  (fun ex => pure 200)
+
+#eval testM g2 100