feat: add AddMessageDataContext

src/Lean/CoreM.lean

@@ -63,16 +63,13 @@ liftM $ (adaptExcept (fun (err : IO.Error) => Exception.error ref (toString err)
 instance : MonadIO CoreM :=
 { liftIO := @liftIOCore }
 
-instance : MonadLCtx CoreM :=
-{ getLCtx := pure {} }
-
-instance : MonadMCtx CoreM :=
-{ getMCtx := pure {} }
-
 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/Command.lean

@@ -113,14 +113,11 @@ 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!
 
-instance : MonadLCtx CommandElabM :=
-{ getLCtx := pure {} }
-
-instance : MonadMCtx CommandElabM :=
-{ getMCtx := pure {} }
-
 instance CommandElabM.monadLog : MonadLog CommandElabM :=
 { getRef      := getRef,
   getFileMap  := do ctx ← read; pure ctx.fileMap,

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] [MonadEnv m] [MonadOptions m] [MonadLCtx m] [MonadMCtx m]
+variables {m : Type → Type} [Monad m] [MonadLog m] [AddMessageDataContext 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 ← addWithContext msgData;
+msgData ← addMessageDataContext msgData;
 logMessage { fileName := fileName, pos := fileMap.toPosition pos, data := msgData, severity := severity }
 
 def logErrorAt (ref : Syntax) (msgData : MessageData) : m Unit :=
@@ -77,11 +77,11 @@ match ex with
 def logTrace (cls : Name) (msgData : MessageData) : m Unit := do
 logInfo (MessageData.tagged cls msgData)
 
-@[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit := do
+@[inline] def trace [MonadOptions m] (cls : Name) (msg : Unit → MessageData) : m Unit := do
 opts ← getOptions;
 when (checkTraceOption opts cls) $ logTrace cls (msg ())
 
-def logDbgTrace (msg : MessageData) : m Unit := do
+def logDbgTrace [MonadOptions m] (msg : MessageData) : m Unit := do
 trace `Elab.debug fun _ => msg
 
 end Elab

src/Lean/Elab/Term.lean

@@ -180,7 +180,7 @@ instance MonadError : MonadError TermElabM :=
     ctx ← read;
     let ref := getBetterRef ref ctx.macroStack;
     let msg := if ctx.macroStackAtErr then addMacroStack msg ctx.macroStack else msg;
-    msg ← addWithContext msg;
+    msg ← addMessageDataContext msg;
     pure (ref, msg) }
 
 instance monadLog : MonadLog TermElabM :=

src/Lean/Environment.lean

@@ -683,4 +683,15 @@ constant isDefEq (env : Environment) (lctx : LocalContext) (a b : Expr) : Bool :
 constant whnf (env : Environment) (lctx : LocalContext) (a : Expr) : Expr := arbitrary _
 
 end Kernel
+
+class MonadEnv (m : Type → Type) :=
+(getEnv    : m Environment)
+(modifyEnv : (Environment → Environment) → m Unit)
+
+export MonadEnv (getEnv modifyEnv)
+
+instance monadEnvFromLift (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n :=
+{ getEnv    := liftM (getEnv : m Environment),
+  modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
+
 end Lean

src/Lean/Message.lean

@@ -219,4 +219,25 @@ match e with
 | other msg                           => "(kernel) " ++ msg
 
 end KernelException
+
+class AddMessageDataContext (m : Type → Type) :=
+(addMessageDataContext : MessageData → m MessageData)
+
+export AddMessageDataContext (addMessageDataContext)
+
+instance addMessageDataContextTrans (m n) [AddMessageDataContext m] [MonadLift m n] : AddMessageDataContext n :=
+{ addMessageDataContext := fun msg => liftM (addMessageDataContext msg : m _) }
+
+def addMessageDataContextPartial {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
+env ← getEnv;
+mctx ← getMCtx;
+lctx ← getLCtx;
+opts ← getOptions;
+pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
+
 end Lean

src/Lean/Meta/Basic.lean

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

src/Lean/Meta/EqnCompiler/Match.lean

@@ -91,7 +91,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;
-  addWithContext msg
+  addMessageDataContext msg
 
 def applyFVarSubst (s : FVarSubst) (alt : Alt) : Alt :=
 { alt with

src/Lean/MonadEnv.lean

@@ -8,16 +8,6 @@ import Lean.Exception
 
 namespace Lean
 
-class MonadEnv (m : Type → Type) :=
-(getEnv    : m Environment)
-(modifyEnv : (Environment → Environment) → m Unit)
-
-export MonadEnv (getEnv modifyEnv)
-
-instance monadEnvFromLift (m n) [MonadEnv m] [MonadLift m n] : MonadEnv n :=
-{ getEnv    := liftM (getEnv : m Environment),
-  modifyEnv := fun f => liftM (modifyEnv f : m Unit) }
-
 section Methods
 
 variables {m : Type → Type} [MonadEnv m]

src/Lean/Util/Trace.lean

@@ -9,13 +9,6 @@ universe u
 
 namespace Lean
 
-def addWithContext {m} [Monad m] [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m] (msgData : MessageData) : m MessageData := do
-env ← getEnv;
-mctx ← getMCtx;
-lctx ← getLCtx;
-opts ← getOptions;
-pure $ MessageData.withContext { env := env, mctx := mctx, lctx := lctx, opts := opts } msgData
-
 open Std (PersistentArray)
 
 structure TraceState :=
@@ -104,10 +97,10 @@ modifyTraces $ fun _ => {};
 pure oldTraces
 
 section
-variables [MonadEnv m] [MonadMCtx m] [MonadLCtx m] [MonadOptions m]
+variables [AddMessageDataContext m] [MonadOptions m]
 
 def addTrace (cls : Name) (msg : MessageData) : m Unit := do
-msg ← addWithContext msg;
+msg ← addMessageDataContext msg;
 modifyTraces $ fun traces => traces.push (MessageData.tagged cls msg)
 
 @[inline] def trace (cls : Name) (msg : Unit → MessageData) : m Unit :=