refactor: remove MonadError

src/Lean/Compiler/ImplementedByAttr.lean

@@ -31,7 +31,8 @@ implementedByAttr.setParam env declName impName
 
 end Compiler
 
-def setImplementedBy {m} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) (impName : Name) : m Unit := do
+def setImplementedBy {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+    (declName : Name) (impName : Name) : m Unit := do
 env ← getEnv;
 match Compiler.setImplementedBy env declName impName with
 | Except.ok env   => setEnv env

src/Lean/CoreM.lean

@@ -32,13 +32,9 @@ abbrev CoreM := ReaderT Context $ StateRefT State $ EIO Exception
 instance CoreM.inhabited {α} : Inhabited (CoreM α) :=
 ⟨fun _ _ => throw $ arbitrary _⟩
 
-instance : MonadError CoreM :=
+instance : Ref CoreM :=
 { getRef     := do ctx ← read; pure ctx.ref,
-  withRef    := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x,
-  addContext := fun ref msg => do
-    ctx ← read;
-    s   ← get;
-    pure (ref, MessageData.withContext { env := s.env, mctx := {}, lctx := {}, opts := ctx.options } msg) }
+  withRef    := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x }
 
 instance : MonadEnv CoreM :=
 { getEnv    := do s ← get; pure s.env,
@@ -47,6 +43,9 @@ instance : MonadEnv CoreM :=
 instance : MonadOptions CoreM :=
 { getOptions := do ctx ← read; pure ctx.options }
 
+instance : AddMessageContext CoreM :=
+{ addMessageContext := addMessageContextPartial }
+
 instance : MonadNameGenerator CoreM :=
 { getNGen := do s ← get; pure s.ngen,
   setNGen := fun ngen => modify fun s => { s with ngen := ngen } }
@@ -67,9 +66,6 @@ instance : MonadTrace CoreM :=
 { getTraceState    := do s ← get; pure s.traceState,
   modifyTraceState := fun f => modify $ fun s => { s with traceState := f s.traceState } }
 
-instance : AddMessageDataContext CoreM :=
-{ addMessageDataContext := addMessageDataContextPartial }
-
 @[inline] def CoreM.run {α} (x : CoreM α) (ctx : Context) (s : State) : EIO Exception (α × State) :=
 (x.run ctx).run s
 

src/Lean/Elab/Attributes.lean

@@ -18,7 +18,7 @@ instance Attribute.hasFormat : HasFormat Attribute :=
 
 instance Attribute.inhabited : Inhabited Attribute := ⟨{ name := arbitrary _ }⟩
 
-def elabAttr {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m Attribute := do
+def elabAttr {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m Attribute := do
 -- rawIdent >> many attrArg
 let nameStx := stx.getArg 0;
 attrName ← match nameStx.isIdOrAtom? with
@@ -32,7 +32,7 @@ let args := stx.getArg 1;
 let args := if args.getNumArgs == 0 then Syntax.missing else args;
 pure { name := attrName, args := args }
 
-def elabAttrs {m} [Monad m] [MonadEnv m] [MonadError m] (stx : Syntax) : m (Array Attribute) :=
+def elabAttrs {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (stx : Syntax) : m (Array Attribute) :=
 (stx.getArg 1).foldSepArgsM
   (fun stx attrs => do
     attr ← elabAttr stx;

src/Lean/Elab/Command.lean

@@ -63,21 +63,20 @@ instance : MonadOptions CommandElabM :=
 protected def getRef : CommandElabM Syntax :=
 do ctx ← read; pure ctx.ref
 
-protected def addContext' (msg : MessageData) : CommandElabM MessageData := do
-env ← getEnv; opts ← getOptions;
-pure (MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msg)
+instance : AddMessageContext CommandElabM :=
+{ addMessageContext := addMessageContextPartial }
 
-protected def addContext (ref : Syntax) (msg : MessageData) : CommandElabM (Syntax × MessageData) := do
-ctx ← read;
-let ref := getBetterRef ref ctx.macroStack;
-msg ← addMacroStack msg ctx.macroStack;
-msg ← Command.addContext' msg;
-pure (ref, msg)
-
-instance : MonadError CommandElabM :=
+instance : Ref CommandElabM :=
 { getRef     := Command.getRef,
-  withRef    := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x,
-  addContext := Command.addContext }
+  withRef    := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x }
+
+instance : AddErrorMessageContext CommandElabM :=
+{ add := fun ref msg => do
+  ctx ← read;
+  let ref := getBetterRef ref ctx.macroStack;
+  msg ← addMessageContext msg;
+  msg ← addMacroStack msg ctx.macroStack;
+  pure (ref, msg) }
 
 def mkMessageAux (ctx : Context) (ref : Syntax) (msgData : MessageData) (severity : MessageSeverity) : Message :=
 mkMessageCore ctx.fileName ctx.fileMap msgData severity (ref.getPos.getD ctx.cmdPos)
@@ -115,9 +114,6 @@ liftEIO $ adaptExcept (fun (ex : IO.Error) => Exception.error ctx.ref ex.toStrin
 instance : MonadIO CommandElabM :=
 { liftIO := fun α => liftIO }
 
-instance : AddMessageDataContext CommandElabM :=
-{ addMessageDataContext := addMessageDataContextPartial }
-
 def getScope : CommandElabM Scope := do s ← get; pure s.scopes.head!
 
 def getCurrNamespace : CommandElabM Name := do

src/Lean/Elab/DeclModifiers.lean

@@ -11,7 +11,8 @@ import Lean.Elab.DeclUtil
 namespace Lean
 namespace Elab
 
-def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadError m] (declName : Name) : m Unit := do
+def checkNotAlreadyDeclared {m} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+     (declName : Name) : m Unit := do
 env ← getEnv;
 when (env.contains declName) $
   match privateToUserName? declName with
@@ -73,7 +74,7 @@ instance Modifiers.hasToString : HasToString Modifiers := ⟨toString ∘ format
 
 section Methods
 
-variables {m : Type → Type} [Monad m] [MonadEnv m] [MonadError m]
+variables {m : Type → Type} [Monad m] [MonadEnv m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
 
 def elabModifiers (stx : Syntax) : m Modifiers := do
 let docCommentStx := stx.getArg 0;

src/Lean/Elab/Exception.lean

@@ -30,10 +30,10 @@ throw $ Exception.internal postponeExceptionId
 def throwUnsupportedSyntax {α m} [MonadExceptOf Exception m] : m α :=
 throw $ Exception.internal unsupportedSyntaxExceptionId
 
-def throwIllFormedSyntax {α m} [Monad m] [MonadError m] : m α :=
+def throwIllFormedSyntax {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] : m α :=
 throwError "ill-formed syntax"
 
-def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadError m] (u : Name) : m α :=
+def throwAlreadyDeclaredUniverseLevel {α m} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (u : Name) : m α :=
 throwError ("a universe level named '" ++ toString u ++ "' has already been declared")
 
 -- Throw exception to abort elaboration without producing any error message

src/Lean/Elab/Level.lean

@@ -21,10 +21,12 @@ structure State :=
 
 abbrev LevelElabM := ReaderT Context (EStateM Exception State)
 
-instance : MonadError LevelElabM :=
+instance : Ref LevelElabM :=
 { getRef      := do ctx ← read; pure ctx.ref,
-  withRef     := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x,
-  addContext  := fun ref msg => pure (ref, msg) }
+  withRef     := fun α ref x => adaptReader (fun (ctx : Context) => { ctx with ref := ref }) x }
+
+instance : AddMessageContext LevelElabM :=
+{ addMessageContext  := fun msg => pure msg }
 
 instance : MonadNameGenerator LevelElabM :=
 { getNGen := do s ← get; pure s.ngen,

src/Lean/Elab/Log.lean

@@ -24,7 +24,7 @@ instance monadLogTrans (m n) [MonadLog m] [MonadLift m n] : MonadLog n :=
 export MonadLog (getFileMap getFileName logMessage)
 open MonadLog (getRef)
 
-variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageDataContext m]
+variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageContext m]
 
 def getRefPos : m String.Pos := do
 ref ← getRef;
@@ -41,7 +41,7 @@ let ref  := replaceRef ref currRef;
 let pos  := ref.getPos.getD 0;
 fileMap  ← getFileMap;
 fileName ← getFileName;
-msgData ← addMessageDataContext msgData;
+msgData ← addMessageContext msgData;
 logMessage { fileName := fileName, pos := fileMap.toPosition pos, data := msgData, severity := severity }
 
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=

src/Lean/Elab/Term.lean

@@ -269,15 +269,17 @@ def getFVarLocalDecl! (fvar : Expr) : TermElabM LocalDecl := do
   | some d => pure d
   | none   => unreachable!
 
-instance MonadError : MonadError TermElabM :=
+instance : Ref TermElabM :=
 { getRef     := getRef,
-  withRef    := fun α => withRef,
-  addContext := fun ref msg => do
-    ctx ← read;
-    let ref := getBetterRef ref ctx.macroStack;
-    msg ← addMacroStack msg ctx.macroStack;
-    msg ← addMessageDataContext msg;
-    pure (ref, msg) }
+  withRef    := fun α => withRef }
+
+instance : AddErrorMessageContext TermElabM :=
+{ add := fun ref msg => do
+  ctx ← read;
+  let ref := getBetterRef ref ctx.macroStack;
+  msg ← addMessageContext msg;
+  msg ← addMacroStack msg ctx.macroStack;
+  pure (ref, msg) }
 
 instance monadLog : MonadLog TermElabM :=
 { getRef      := getRef,

src/Lean/Elab/Util.lean

@@ -129,7 +129,8 @@ instance monadMacroAdapterTrans (m n) [MonadMacroAdapter m] [MonadLift m n] : Mo
   getNextMacroScope := liftM (MonadMacroAdapter.getNextMacroScope : m _),
   setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _) }
 
-@[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] (x : MacroM α) : m α := do
+@[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
+    [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : MacroM α) : m α := do
 scp  ← MonadMacroAdapter.getCurrMacroScope;
 env  ← getEnv;
 next ← MonadMacroAdapter.getNextMacroScope;
@@ -140,7 +141,8 @@ match x { currMacroScope := scp, mainModule := env.mainModule, currRecDepth := c
 | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg
 | EStateM.Result.ok a nextMacroScope                       => do MonadMacroAdapter.setNextMacroScope nextMacroScope; pure a
 
-@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] (x : Macro) (stx : Syntax) : m Syntax :=
+@[inline] def adaptMacro {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m]
+    [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m] (x : Macro) (stx : Syntax) : m Syntax :=
 liftMacroM (x stx)
 
 def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syntax) := do

src/Lean/Exception.lean

@@ -24,45 +24,49 @@ def Exception.getRef : Exception → Syntax
 
 instance Exception.inhabited : Inhabited Exception := ⟨Exception.error (arbitrary _) (arbitrary _)⟩
 
-class MonadError (m : Type → Type) extends MonadExceptOf Exception m :=
-(getRef         : m Syntax)
-(addContext     : Syntax → MessageData → m (Syntax × MessageData))
-(withRef    {α} : Syntax → m α → m α)
+class Ref (m : Type → Type) :=
+(getRef      : m Syntax)
+(withRef {α} : Syntax → m α → m α)
 
-export MonadError (getRef addContext withRef)
+export Ref (getRef withRef)
 
-instance ReaderT.monadError {ρ m} [Monad m] [MonadError m] : MonadError (ReaderT ρ m) :=
-{ getRef        := fun _           => getRef,
-  addContext    := fun ref msg _   => addContext ref msg,
-  withRef       := fun α ref x ctx => MonadError.withRef ref (x ctx) }
-
-instance StateRefT.monadError {ω σ m} [Monad m] [MonadError m] : MonadError (StateRefT' ω σ m) :=
-inferInstanceAs (MonadError (ReaderT _ _))
-
-section Methods
-
-variables {m : Type → Type} [Monad m] [MonadError m]
-
-def throwError {α} (msg : MessageData) : m α := do
-ref ← getRef;
-(ref, msg) ← addContext ref msg;
-throw $ Exception.error ref msg
+instance refTrans (m n : Type → Type) [Ref m] [MonadFunctor m m n n] [MonadLift m n] : Ref n :=
+{ getRef  := liftM (getRef : m _),
+  withRef := fun α ref x => monadMap (fun α => withRef ref : forall {α}, m α → m α) x }
 
 def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
 match ref.getPos with
 | some _ => ref
 | _      => oldRef
 
-@[inline] def withRef {α} (ref : Syntax) (x : m α) : m α := do
+@[inline] def withRef {m : Type → Type} [Monad m] [Ref m] {α} (ref : Syntax) (x : m α) : m α := do
 oldRef ← getRef;
 let ref := replaceRef ref oldRef;
-MonadError.withRef ref x
+Ref.withRef ref x
+
+/- Similar to `AddMessageContext`, but for error messages.
+   The default instance just uses `AddMessageContext`.
+   In error messages, we may want to provide additional information (e.g., macro expansion stack),
+   and refine the `(ref : Syntax)`. -/
+class AddErrorMessageContext (m : Type → Type) :=
+(add : Syntax → MessageData → m (Syntax × MessageData))
+
+instance addErrorMessageContextDefault (m : Type → Type) [AddMessageContext m] [Monad m] : AddErrorMessageContext m :=
+{ add := fun ref msg => do
+  msg ← addMessageContext msg;
+  pure (ref, msg) }
+
+section Methods
+
+variables {m : Type → Type} [Monad m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+
+def throwError {α} (msg : MessageData) : m α := do
+ref ← getRef;
+(ref, msg) ← AddErrorMessageContext.add ref msg;
+throw $ Exception.error ref msg
 
 def throwErrorAt {α} (ref : Syntax) (msg : MessageData) : m α := do
-ctxRef ← getRef;
-let ref := replaceRef ref ctxRef;
-(ref, msg) ← addContext ref msg;
-throw $ Exception.error ref msg
+withRef ref $ throwError msg
 
 def ofExcept {ε α} [HasToString ε] (x : Except ε α) : m α :=
 match x with
@@ -88,7 +92,8 @@ instance ReaderT.MonadRecDepth {ρ m} [Monad m] [MonadRecDepth m] : MonadRecDept
 instance StateRefT.monadRecDepth {ω σ m} [Monad m] [MonadRecDepth m] : MonadRecDepth (StateRefT' ω σ m) :=
 inferInstanceAs (MonadRecDepth (ReaderT _ _))
 
-@[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadError m] (x : m α) : m α := do
+@[inline] def withIncRecDepth {α m} [Monad m] [MonadRecDepth m] [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+    (x : m α) : m α := do
 curr ← MonadRecDepth.getRecDepth;
 max  ← MonadRecDepth.getMaxRecDepth;
 when (curr == max) $ throwError maxRecDepthErrorMessage;

src/Lean/Message.lean

@@ -259,20 +259,20 @@ match e with
 
 end KernelException
 
-class AddMessageDataContext (m : Type → Type) :=
-(addMessageDataContext : MessageData → m MessageData)
+class AddMessageContext (m : Type → Type) :=
+(addMessageContext : MessageData → m MessageData)
 
-export AddMessageDataContext (addMessageDataContext)
+export AddMessageContext (addMessageContext)
 
-instance addMessageDataContextTrans (m n) [AddMessageDataContext m] [MonadLift m n] : AddMessageDataContext n :=
-{ addMessageDataContext := fun msg => liftM (addMessageDataContext msg : m _) }
+instance addMessageContextTrans (m n) [AddMessageContext m] [MonadLift m n] : AddMessageContext n :=
+{ addMessageContext := fun msg => liftM (addMessageContext msg : m _) }
 
-def addMessageDataContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
+def addMessageContextPartial {m} [Monad m] [MonadEnv m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
 env ← getEnv;
 opts ← getOptions;
 pure $ MessageData.withContext { env := env, mctx := {}, lctx := {}, opts := opts } msgData
 
-def addMessageDataContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
+def addMessageContextFull {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
 env ← getEnv;
 mctx ← getMCtx;
 lctx ← getLCtx;

src/Lean/Meta/Basic.lean

@@ -123,13 +123,12 @@ instance : MonadLCtx MetaM :=
 instance : MonadMCtx MetaM :=
 { getMCtx := do s ← get; pure s.mctx }
 
-instance : AddMessageDataContext MetaM :=
-{ addMessageDataContext := addMessageDataContextFull }
+instance : AddMessageContext MetaM :=
+{ addMessageContext := addMessageContextFull }
 
-instance : MonadError MetaM :=
+instance : Ref MetaM :=
 { getRef     := getRef,
-  withRef    := fun α => withRef,
-  addContext := fun ref msg => do msg ← addMessageDataContext msg; pure (ref, msg) }
+  withRef    := fun α => withRef }
 
 @[inline] def MetaM.run {α} (x : MetaM α) (ctx : Context := {}) (s : State := {}) : CoreM (α × State) :=
 (x.run ctx).run s

src/Lean/Meta/Match/Match.lean

@@ -88,7 +88,7 @@ partial def toMessageData (alt : Alt) : MetaM MessageData := do
 withExistingLocalDecls alt.fvarDecls do
   let msg : List MessageData := alt.fvarDecls.map fun d => d.toExpr ++ ":(" ++ d.type ++ ")";
   let msg : MessageData := msg ++ " |- " ++ (alt.patterns.map Pattern.toMessageData) ++ " => " ++ alt.rhs;
-  addMessageDataContext msg
+  addMessageContext msg
 
 def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
 { alt with

src/Lean/MonadEnv.lean

@@ -61,7 +61,7 @@ def mkAuxName (baseName : Name) (idx : Nat) : m Name := do
 env ← getEnv;
 pure $ mkAuxNameAux env baseName idx
 
-variables [MonadError m]
+variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
 
 def getConstInfo (constName : Name) : m ConstantInfo := do
 env ← getEnv;
@@ -115,11 +115,13 @@ def addAndCompile [MonadOptions m] (decl : Declaration) : m Unit := do
 addDecl decl;
 compileDecl decl
 
-unsafe def evalConst [MonadError m] (α) (constName : Name) : m α := do
+variables [MonadExceptOf Exception m] [Ref m] [AddErrorMessageContext m]
+
+unsafe def evalConst (α) (constName : Name) : m α := do
 env ← getEnv;
 ofExcept $ env.evalConst α constName
 
-unsafe def evalConstCheck [MonadError m] (α) (typeName : Name) (constName : Name) : m α := do
+unsafe def evalConstCheck (α) (typeName : Name) (constName : Name) : m α := do
 env ← getEnv;
 ofExcept $ env.evalConstCheck α typeName constName
 

src/Lean/Util/Trace.lean

@@ -93,10 +93,10 @@ modifyTraces $ fun _ => {};
 pure oldTraces
 
 section
-variables [AddMessageDataContext m] [MonadOptions m]
+variables [AddMessageContext m] [MonadOptions m]
 
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
-msg ← addMessageDataContext msg;
+msg ← addMessageContext msg;
 modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg)
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit :=