chore: fix tests

`Expr.equal` takes binder names into account.

src/Lean/Elab/Tactic/DiscrTreeKey.lean

@@ -18,21 +18,22 @@ private def mkKey (e : Expr) (simp : Bool) : MetaM (Array Key) := do
   let (_, _, type) ← withReducible <| forallMetaTelescopeReducing e
   let type ← whnfR type
   if simp then
-    if let some (_, lhs, _) := type.eq? then
-      mkPath lhs simpDtConfig
-    else if let some (lhs, _) := type.iff? then
-      mkPath lhs simpDtConfig
-    else if let some (_, lhs, _) := type.ne? then
-      mkPath lhs simpDtConfig
-    else if let some p := type.not? then
-      match p.eq? with
-      | some (_, lhs, _) =>
-        mkPath lhs simpDtConfig
-      | _ => mkPath p simpDtConfig
-    else
-      mkPath type simpDtConfig
+    withSimpGlobalConfig do
+      if let some (_, lhs, _) := type.eq? then
+        mkPath lhs
+      else if let some (lhs, _) := type.iff? then
+        mkPath lhs
+      else if let some (_, lhs, _) := type.ne? then
+        mkPath lhs
+      else if let some p := type.not? then
+        match p.eq? with
+        | some (_, lhs, _) =>
+          mkPath lhs
+        | _ => mkPath p
+      else
+        mkPath type
   else
-    mkPath type {}
+    mkPath type
 
 private def getType (t : TSyntax `term) : TermElabM Expr := do
   if let `($id:ident) := t then

src/Lean/Elab/Tactic/Ext.lean

@@ -195,9 +195,6 @@ structure ExtTheorems where
   erased  : PHashSet Name := {}
   deriving Inhabited
 
-/-- Discrimation tree settings for the `ext` extension. -/
-def extExt.config : WhnfCoreConfig := {}
-
 /-- The environment extension to track `@[ext]` theorems. -/
 builtin_initialize extExtension :
     SimpleScopedEnvExtension ExtTheorem ExtTheorems ←
@@ -211,7 +208,7 @@ builtin_initialize extExtension :
 ordered from high priority to low. -/
 @[inline] def getExtTheorems (ty : Expr) : MetaM (Array ExtTheorem) := do
   let extTheorems := extExtension.getState (← getEnv)
-  let arr ← extTheorems.tree.getMatch ty extExt.config
+  let arr ← extTheorems.tree.getMatch ty
   let erasedArr := arr.filter fun thm => !extTheorems.erased.contains thm.declName
   -- Using insertion sort because it is stable and the list of matches should be mostly sorted.
   -- Most ext theorems have default priority.
@@ -258,7 +255,7 @@ builtin_initialize registerBuiltinAttribute {
       but this theorem proves{indentD declTy}"
     let some (ty, lhs, rhs) := declTy.eq? | failNotEq
     unless lhs.isMVar && rhs.isMVar do failNotEq
-    let keys ← withReducible <| DiscrTree.mkPath ty extExt.config
+    let keys ← withReducible <| DiscrTree.mkPath ty
     let priority ← liftCommandElabM <| Elab.liftMacroM do evalPrio (prio.getD (← `(prio| default)))
     extExtension.add {declName, keys, priority} kind
     -- Realize iff theorem

src/Lean/Elab/Tactic/Simp.lean

@@ -91,7 +91,7 @@ def elabSimpConfig (optConfig : Syntax) (kind : SimpKind) : TacticM Meta.Simp.Co
   | .simpAll => return (← elabSimpConfigCtxCore optConfig).toConfig
   | .dsimp   => return { (← elabDSimpConfigCore optConfig) with }
 
-private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
+private def addDeclToUnfoldOrTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (e : Expr) (post : Bool) (inv : Bool) (kind : SimpKind) : MetaM SimpTheorems := do
   if e.isConst then
     let declName := e.constName!
     let info ← getConstInfo declName
@@ -108,7 +108,7 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     let fvarId := e.fvarId!
     let decl ← fvarId.getDecl
     if (← isProp decl.type) then
-      thms.add id #[] e (post := post) (inv := inv)
+      thms.add id #[] e (post := post) (inv := inv) (config := config)
     else if !decl.isLet then
       throwError "invalid argument, variable is not a proposition or let-declaration"
     else if inv then
@@ -116,9 +116,9 @@ private def addDeclToUnfoldOrTheorem (thms : SimpTheorems) (id : Origin) (e : Ex
     else
       return thms.addLetDeclToUnfold fvarId
   else
-    thms.add id #[] e (post := post) (inv := inv)
+    thms.add id #[] e (post := post) (inv := inv) (config := config)
 
-private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
+private def addSimpTheorem (config : Meta.ConfigWithKey) (thms : SimpTheorems) (id : Origin) (stx : Syntax) (post : Bool) (inv : Bool) : TermElabM SimpTheorems := do
   let thm? ← Term.withoutModifyingElabMetaStateWithInfo <| withRef stx do
     let e ← Term.elabTerm stx none
     Term.synthesizeSyntheticMVars (postpone := .no) (ignoreStuckTC := true)
@@ -132,7 +132,7 @@ private def addSimpTheorem (thms : SimpTheorems) (id : Origin) (stx : Syntax) (p
     else
       return some (#[], e)
   if let some (levelParams, proof) := thm? then
-    thms.add id levelParams proof (post := post) (inv := inv)
+    thms.add id levelParams proof (post := post) (inv := inv) (config := config)
   else
     return thms
 
@@ -212,7 +212,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
             match (← resolveSimpIdTheorem? term) with
             | .expr e  =>
               let name ← mkFreshId
-              thms ← addDeclToUnfoldOrTheorem thms (.stx name arg) e post inv kind
+              thms ← addDeclToUnfoldOrTheorem ctx.indexConfig thms (.stx name arg) e post inv kind
             | .simproc declName =>
               simprocs ← simprocs.add declName post
             | .ext (some ext₁) (some ext₂) _ =>
@@ -224,7 +224,7 @@ def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (simprocs : Simp.SimprocsAr
               simprocs  := simprocs.push (← ext₂.getSimprocs)
             | .none    =>
               let name ← mkFreshId
-              thms ← addSimpTheorem thms (.stx name arg) term post inv
+              thms ← addSimpTheorem ctx.indexConfig thms (.stx name arg) term post inv
           else if arg.getKind == ``Lean.Parser.Tactic.simpStar then
             starArg := true
           else
@@ -329,7 +329,7 @@ def mkSimpContext (stx : Syntax) (eraseLocal : Bool) (kind := SimpKind.simp)
     let hs ← getPropHyps
     for h in hs do
       unless simpTheorems.isErased (.fvar h) do
-        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr
+        simpTheorems ← simpTheorems.addTheorem (.fvar h) (← h.getDecl).toExpr (config := ctx.indexConfig)
     let ctx := ctx.setSimpTheorems simpTheorems
     return { ctx, simprocs, dischargeWrapper }
 

src/Lean/Elab/Tactic/Simproc.lean

@@ -25,7 +25,7 @@ def elabSimprocPattern (stx : Syntax) : MetaM Expr := do
 
 def elabSimprocKeys (stx : Syntax) : MetaM (Array Meta.SimpTheoremKey) := do
   let pattern ← elabSimprocPattern stx
-  DiscrTree.mkPath pattern simpDtConfig
+  withSimpGlobalConfig <| DiscrTree.mkPath pattern
 
 def checkSimprocType (declName : Name) : CoreM Bool := do
   let decl ← getConstInfo declName

src/Lean/Meta/ACLt.lean

@@ -32,6 +32,9 @@ inductive ReduceMode where
   | reduceSimpleOnly
   | none
 
+private def config : ConfigWithKey :=
+  { transparency := .reducible, iota := false, proj := .no : Config }.toConfigWithKey
+
 mutual
 
 /--
@@ -61,8 +64,8 @@ where
       -- Drawback: cost.
       return e
     else match mode with
-      | .reduce => DiscrTree.reduce e {}
-      | .reduceSimpleOnly => DiscrTree.reduce e { iota := false, proj := .no }
+      | .reduce => DiscrTree.reduce e
+      | .reduceSimpleOnly => withConfigWithKey config <| DiscrTree.reduce e
       | .none => return e
 
   lt (a b : Expr) : MetaM Bool := do

src/Lean/Meta/Basic.lean

@@ -27,6 +27,51 @@ namespace Lean.Meta
 
 builtin_initialize isDefEqStuckExceptionId : InternalExceptionId ← registerInternalExceptionId `isDefEqStuck
 
+def TransparencyMode.toUInt64 : TransparencyMode → UInt64
+  | .all       => 0
+  | .default   => 1
+  | .reducible => 2
+  | .instances => 3
+
+def EtaStructMode.toUInt64 : EtaStructMode → UInt64
+  | .all        => 0
+  | .notClasses => 1
+  | .none       => 2
+
+/--
+Configuration for projection reduction. See `whnfCore`.
+-/
+inductive ProjReductionKind where
+  /-- Projections `s.i` are not reduced at `whnfCore`. -/
+  | no
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnfCore` is used at `s` during the process.
+  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations).
+  -/
+  | yes
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnf` is used at `s` during the process.
+  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
+  -/
+  | yesWithDelta
+  /--
+  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
+  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
+  This option is stronger than `yes`, but weaker than `yesWithDelta`.
+  We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
+  When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
+  we only want to unify negation (and not all other field operations as well).
+  Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
+  -/
+  | yesWithDeltaI
+  deriving DecidableEq, Inhabited, Repr
+
+def ProjReductionKind.toUInt64 : ProjReductionKind → UInt64
+  | .no  => 0
+  | .yes => 1
+  | .yesWithDelta => 2
+  | .yesWithDeltaI => 3
+
 /--
 Configuration flags for the `MetaM` monad.
 Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not.
@@ -118,9 +163,64 @@ structure Config where
   - `max u w =?= mav u ?v` is solved with `?v := w` ignoring the solution `?v := max u w`
   -/
   univApprox : Bool := true
+  /-- If `true`, reduce recursor/matcher applications, e.g., `Nat.rec true (fun _ _ => false) Nat.zero` reduces to `true` -/
+  iota : Bool := true
+  /-- If `true`, reduce terms such as `(fun x => t[x]) a` into `t[a]` -/
+  beta : Bool := true
+  /-- Control projection reduction at `whnfCore`. -/
+  proj : ProjReductionKind := .yesWithDelta
+  /--
+  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
+  We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
+  Recall that
+  ```
+  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
+  ```
+  is type correct, but
+  ```
+  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
+  ```
+  is not.
+  -/
+  zeta : Bool := true
+  /--
+  Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
+  -/
+  zetaDelta : Bool := true
+  deriving Inhabited
+
+/-- Convert `isDefEq` and `WHNF` relevant parts into a key for caching results -/
+private def Config.toKey (c : Config) : UInt64 :=
+  c.transparency.toUInt64 |||
+  (c.foApprox.toUInt64 <<< 2) |||
+  (c.ctxApprox.toUInt64 <<< 3) |||
+  (c.quasiPatternApprox.toUInt64 <<< 4) |||
+  (c.constApprox.toUInt64 <<< 5) |||
+  (c.isDefEqStuckEx.toUInt64 <<< 6) |||
+  (c.unificationHints.toUInt64 <<< 7) |||
+  (c.proofIrrelevance.toUInt64 <<< 8) |||
+  (c.assignSyntheticOpaque.toUInt64 <<< 9) |||
+  (c.offsetCnstrs.toUInt64 <<< 10) |||
+  (c.iota.toUInt64 <<< 11) |||
+  (c.beta.toUInt64 <<< 12) |||
+  (c.zeta.toUInt64 <<< 13) |||
+  (c.zetaDelta.toUInt64 <<< 14) |||
+  (c.univApprox.toUInt64 <<< 15) |||
+  (c.etaStruct.toUInt64 <<< 16) |||
+  (c.proj.toUInt64 <<< 18)
+
+/-- Configuration with key produced by `Config.toKey`. -/
+structure ConfigWithKey where
+  private mk ::
+  config : Config
+  key    : UInt64
+  deriving Inhabited
+
+def Config.toConfigWithKey (c : Config) : ConfigWithKey :=
+  { config := c, key := c.toKey }
 
 /--
-  Function parameter information cache.
+Function parameter information cache.
 -/
 structure ParamInfo where
   /-- The binder annotation for the parameter. -/
@@ -178,7 +278,6 @@ def ParamInfo.isStrictImplicit (p : ParamInfo) : Bool :=
 def ParamInfo.isExplicit (p : ParamInfo) : Bool :=
   p.binderInfo == BinderInfo.default
 
-
 /--
   Function information cache. See `ParamInfo`.
 -/
@@ -192,11 +291,12 @@ structure FunInfo where
   resultDeps : Array Nat       := #[]
 
 /--
-  Key for the function information cache.
+Key for the function information cache.
 -/
 structure InfoCacheKey where
-  /-- The transparency mode used to compute the `FunInfo`. -/
-  transparency : TransparencyMode
+  private mk ::
+  /-- key produced using `Config.toKey`. -/
+  configKey : UInt64
   /-- The function being cached information about. It is quite often an `Expr.const`. -/
   expr         : Expr
   /--
@@ -207,11 +307,10 @@ structure InfoCacheKey where
   nargs?       : Option Nat
   deriving Inhabited, BEq
 
-namespace InfoCacheKey
-instance : Hashable InfoCacheKey :=
-  ⟨fun ⟨transparency, expr, nargs⟩ => mixHash (hash transparency) <| mixHash (hash expr) (hash nargs)⟩
-end InfoCacheKey
+instance : Hashable InfoCacheKey where
+  hash := fun { configKey, expr, nargs? } => mixHash (hash configKey) <| mixHash (hash expr) (hash nargs?)
 
+-- Remark: we don't need to store `Config.toKey` because typeclass resolution uses a fixed configuration.
 structure SynthInstanceCacheKey where
   localInsts        : LocalInstances
   type              : Expr
@@ -231,38 +330,50 @@ structure AbstractMVarsResult where
 
 abbrev SynthInstanceCache := PersistentHashMap SynthInstanceCacheKey (Option AbstractMVarsResult)
 
-abbrev InferTypeCache := PersistentExprStructMap Expr
+-- Key for `InferType` and `WHNF` caches
+structure ExprConfigCacheKey where
+  private mk ::
+  expr      : Expr
+  configKey : UInt64
+  deriving Inhabited
+
+instance : BEq ExprConfigCacheKey where
+  beq a b :=
+    Expr.equal a.expr b.expr &&
+    a.configKey == b.configKey
+
+instance : Hashable ExprConfigCacheKey where
+  hash := fun { expr, configKey } => mixHash (hash expr) (hash configKey)
+
+abbrev InferTypeCache := PersistentHashMap ExprConfigCacheKey Expr
 abbrev FunInfoCache   := PersistentHashMap InfoCacheKey FunInfo
-abbrev WhnfCache      := PersistentExprStructMap Expr
+abbrev WhnfCache      := PersistentHashMap ExprConfigCacheKey Expr
+
+structure DefEqCacheKey where
+  private mk ::
+  lhs       : Expr
+  rhs       : Expr
+  configKey : UInt64
+  deriving Inhabited, BEq
+
+instance : Hashable DefEqCacheKey where
+  hash := fun { lhs, rhs, configKey } => mixHash (hash lhs) <| mixHash (hash rhs) (hash configKey)
 
 /--
-  A mapping `(s, t) ↦ isDefEq s t` per transparency level.
-  TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
-  We should also investigate the impact on memory consumption. -/
-structure DefEqCache where
-  reducible : PersistentHashMap (Expr × Expr) Bool := {}
-  instances : PersistentHashMap (Expr × Expr) Bool := {}
-  default   : PersistentHashMap (Expr × Expr) Bool := {}
-  all       : PersistentHashMap (Expr × Expr) Bool := {}
-  deriving Inhabited
-
-/--
-  A cache for `inferType` at transparency levels `.default` an `.all`.
+A mapping `(s, t) ↦ isDefEq s t`.
+TODO: consider more efficient representations (e.g., a proper set) and caching policies (e.g., imperfect cache).
+We should also investigate the impact on memory consumption.
 -/
-structure InferTypeCaches where
-  default   : InferTypeCache
-  all       : InferTypeCache
-  deriving Inhabited
+abbrev DefEqCache := PersistentHashMap DefEqCacheKey Bool
 
 /--
-  Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
+Cache datastructures for type inference, type class resolution, whnf, and definitional equality.
 -/
 structure Cache where
-  inferType      : InferTypeCaches := ⟨{}, {}⟩
+  inferType      : InferTypeCache := {}
   funInfo        : FunInfoCache := {}
   synthInstance  : SynthInstanceCache := {}
-  whnfDefault    : WhnfCache := {} -- cache for closed terms and `TransparencyMode.default`
-  whnfAll        : WhnfCache := {} -- cache for closed terms and `TransparencyMode.all`
+  whnf           : WhnfCache := {}
   defEqTrans     : DefEqCache := {} -- transient cache for terms containing mvars or using nonstandard configuration options, it is frequently reset.
   defEqPerm      : DefEqCache := {} -- permanent cache for terms not containing mvars and using standard configuration options
   deriving Inhabited
@@ -333,6 +444,7 @@ register_builtin_option maxSynthPendingDepth : Nat := {
 -/
 structure Context where
   private config    : Config               := {}
+  private configKey : UInt64               := config.toKey
   /-- Local context -/
   lctx              : LocalContext         := {}
   /-- Local instances in `lctx`. -/
@@ -483,17 +595,27 @@ variable [MonadControlT MetaM n] [Monad n]
 @[inline] def modifyCache (f : Cache → Cache) : MetaM Unit :=
   modify fun { mctx, cache, zetaDeltaFVarIds, postponed, diag } => { mctx, cache := f cache, zetaDeltaFVarIds, postponed, diag }
 
-@[inline] def modifyInferTypeCacheDefault (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨f icd, ica⟩, c1, c2, c3, c4, c5, c6⟩
-
-@[inline] def modifyInferTypeCacheAll (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
-  modifyCache fun ⟨⟨icd, ica⟩, c1, c2, c3, c4, c5, c6⟩ => ⟨⟨icd, f ica⟩, c1, c2, c3, c4, c5, c6⟩
+@[inline] def modifyInferTypeCache (f : InferTypeCache → InferTypeCache) : MetaM Unit :=
+  modifyCache fun ⟨ic, c1, c2, c3, c4, c5⟩ => ⟨f ic, c1, c2, c3, c4, c5⟩
 
 @[inline] def modifyDefEqTransientCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqTrans, c6⟩ => ⟨c1, c2, c3, c4, c5, f defeqTrans, c6⟩
+  modifyCache fun ⟨c1, c2, c3, c4, defeqTrans, c5⟩ => ⟨c1, c2, c3, c4, f defeqTrans, c5⟩
 
 @[inline] def modifyDefEqPermCache (f : DefEqCache → DefEqCache) : MetaM Unit :=
-  modifyCache fun ⟨c1, c2, c3, c4, c5, c6, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, c6, f defeqPerm⟩
+  modifyCache fun ⟨c1, c2, c3, c4, c5, defeqPerm⟩ => ⟨c1, c2, c3, c4, c5, f defeqPerm⟩
+
+def mkExprConfigCacheKey (expr : Expr) : MetaM ExprConfigCacheKey :=
+  return { expr, configKey := (← read).configKey }
+
+def mkDefEqCacheKey (lhs rhs : Expr) : MetaM DefEqCacheKey := do
+  let configKey := (← read).configKey
+  if Expr.quickLt lhs rhs then
+    return { lhs, rhs, configKey }
+  else
+    return { lhs := rhs, rhs := lhs, configKey }
+
+def mkInfoCacheKey (expr : Expr) (nargs? : Option Nat) : MetaM InfoCacheKey :=
+  return { expr, nargs?, configKey := (← read).configKey }
 
 @[inline] def resetDefEqPermCaches : MetaM Unit :=
   modifyDefEqPermCache fun _ => {}
@@ -538,6 +660,9 @@ def getLocalInstances : MetaM LocalInstances :=
 def getConfig : MetaM Config :=
   return (← read).config
 
+def getConfigWithKey : MetaM ConfigWithKey :=
+  return (← getConfig).toConfigWithKey
+
 def resetZetaDeltaFVarIds : MetaM Unit :=
   modify fun s => { s with zetaDeltaFVarIds := {} }
 
@@ -941,7 +1066,16 @@ def elimMVarDeps (xs : Array Expr) (e : Expr) (preserveOrder : Bool := false) :
 
 /-- `withConfig f x` executes `x` using the updated configuration object obtained by applying `f`. -/
 @[inline] def withConfig (f : Config → Config) : n α → n α :=
-  mapMetaM <| withReader (fun ctx => { ctx with config := f ctx.config })
+  mapMetaM <| withReader fun ctx =>
+    let config := f ctx.config
+    let configKey := config.toKey
+    { ctx with config, configKey }
+
+@[inline] def withConfigWithKey (c : ConfigWithKey) : n α → n α :=
+  mapMetaM <| withReader fun ctx =>
+    let config := c.config
+    let configKey := c.key
+    { ctx with config, configKey }
 
 @[inline] def withCanUnfoldPred (p : Config → ConstantInfo → CoreM Bool) : n α → n α :=
   mapMetaM <| withReader (fun ctx => { ctx with canUnfold? := p })
@@ -961,8 +1095,15 @@ Executes `x` tracking zetaDelta reductions `Config.trackZetaDelta := true`
 @[inline] def withoutProofIrrelevance (x : n α) : n α :=
   withConfig (fun cfg => { cfg with proofIrrelevance := false }) x
 
+@[inline] private def Context.setTransparency (ctx : Context) (transparency : TransparencyMode) : Context :=
+  let config := { ctx.config with transparency }
+  -- Recall that `transparency` is stored in the first 2 bits
+  let configKey : UInt64 := ((ctx.configKey >>> (2 : UInt64)) <<< 2) ||| transparency.toUInt64
+  { ctx with config, configKey }
+
 @[inline] def withTransparency (mode : TransparencyMode) : n α → n α :=
-  withConfig (fun config => { config with transparency := mode })
+  -- We avoid `withConfig` for performance reasons.
+  mapMetaM <| withReader (·.setTransparency mode)
 
 /-- `withDefault x` executes `x` using the default transparency setting. -/
 @[inline] def withDefault (x : n α) : n α :=
@@ -983,13 +1124,10 @@ or type class instances are unfolded.
 Execute `x` ensuring the transparency setting is at least `mode`.
 Recall that `.all > .default > .instances > .reducible`.
 -/
-@[inline] def withAtLeastTransparency (mode : TransparencyMode) (x : n α) : n α :=
-  withConfig
-    (fun config =>
-      let oldMode := config.transparency
-      let mode    := if oldMode.lt mode then mode else oldMode
-      { config with transparency := mode })
-    x
+@[inline] def withAtLeastTransparency (mode : TransparencyMode) : n α → n α :=
+  mapMetaM <| withReader fun ctx =>
+    let modeOld := ctx.config.transparency
+    ctx.setTransparency <| if modeOld.lt mode then mode else modeOld
 
 /-- Execute `x` allowing `isDefEq` to assign synthetic opaque metavariables. -/
 @[inline] def withAssignableSyntheticOpaque (x : n α) : n α :=
@@ -1011,8 +1149,8 @@ def getTheoremInfo (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
 
 private def getDefInfoTemp (info : ConstantInfo) : MetaM (Option ConstantInfo) := do
   match (← getTransparency) with
-  | TransparencyMode.all => return some info
-  | TransparencyMode.default => return some info
+  | .all => return some info
+  | .default => return some info
   | _ =>
     if (← isReducible info.name) then
       return some info

src/Lean/Meta/DiscrTree.lean

@@ -305,16 +305,13 @@ def hasNoindexAnnotation (e : Expr) : Bool :=
 
 /--
 Reduction procedure for the discrimination tree indexing.
-The parameter `config` controls how aggressively the term is reduced.
-The parameter at type `DiscrTree` controls this value.
-See comment at `DiscrTree`.
 -/
-partial def reduce (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
-  let e ← whnfCore e config
+partial def reduce (e : Expr) : MetaM Expr := do
+  let e ← whnfCore e
   match (← unfoldDefinition? e) with
-  | some e => reduce e config
+  | some e => reduce e
   | none => match e.etaExpandedStrict? with
-    | some e => reduce e config
+    | some e => reduce e
     | none   => return e
 
 /--
@@ -333,24 +330,24 @@ private def isBadKey (fn : Expr) : Bool :=
   | _           => true
 
 /--
-  Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
-  is a bad key (see comment at `isBadKey`).
-  We use this method instead of `reduce` for root terms at `pushArgs`. -/
-private partial def reduceUntilBadKey (e : Expr) (config : WhnfCoreConfig) : MetaM Expr := do
+Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
+is a bad key (see comment at `isBadKey`).
+We use this method instead of `reduce` for root terms at `pushArgs`. -/
+private partial def reduceUntilBadKey (e : Expr) : MetaM Expr := do
   let e ← step e
   match e.etaExpandedStrict? with
-  | some e => reduceUntilBadKey e config
+  | some e => reduceUntilBadKey e
   | none   => return e
 where
   step (e : Expr) := do
-    let e ← whnfCore e config
+    let e ← whnfCore e
     match (← unfoldDefinition? e) with
     | some e' => if isBadKey e'.getAppFn then return e else step e'
     | none    => return e
 
 /-- whnf for the discrimination tree module -/
-def reduceDT (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM Expr :=
-  if root then reduceUntilBadKey e config else reduce e config
+def reduceDT (e : Expr) (root : Bool) : MetaM Expr :=
+  if root then reduceUntilBadKey e else reduce e
 
 /- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
 
@@ -372,11 +369,11 @@ In this issue, we have a local hypotheses `(h : ∀ p : α × β, f p p.2 = p.2)
 For example, it was introduced by another tactic. Thus, when populating the discrimination tree explicit arguments provided to `simp` (e.g., `simp [h]`),
 we use `noIndexAtArgs := true`. See comment: https://github.com/leanprover/lean4/issues/2670#issuecomment-1758889365
 -/
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (noIndexAtArgs : Bool) : MetaM (Key × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
-    let e ← reduceDT e root config
+    let e ← reduceDT e root
     let fn := e.getAppFn
     let push (k : Key) (nargs : Nat) (todo : Array Expr): MetaM (Key × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
@@ -422,23 +419,23 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : Whnf
     | _ => return (.other, todo)
 
 @[inherit_doc pushArgs]
-partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (config : WhnfCoreConfig) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
+partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) (noIndexAtArgs : Bool) : MetaM (Array Key) := do
   if todo.isEmpty then
     return keys
   else
     let e    := todo.back!
     let todo := todo.pop
-    let (k, todo) ← pushArgs root todo e config noIndexAtArgs
-    mkPathAux false todo (keys.push k) config noIndexAtArgs
+    let (k, todo) ← pushArgs root todo e noIndexAtArgs
+    mkPathAux false todo (keys.push k) noIndexAtArgs
 
 private def initCapacity := 8
 
 @[inherit_doc pushArgs]
-def mkPath (e : Expr) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (Array Key) := do
+def mkPath (e : Expr) (noIndexAtArgs := false) : MetaM (Array Key) := do
   withReducible do
     let todo : Array Expr := .mkEmpty initCapacity
     let keys : Array Key := .mkEmpty initCapacity
-    mkPathAux (root := true) (todo.push e) keys config noIndexAtArgs
+    mkPathAux (root := true) (todo.push e) keys noIndexAtArgs
 
 private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
   if h : i < keys.size then
@@ -492,23 +489,23 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
       let c := insertAux keys v 1 c
       { root := d.root.insert k c }
 
-def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config noIndexAtArgs
+def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
   return d.insertCore keys v
 
 /--
 Inserts a value into a discrimination tree,
 but only if its key is not of the form `#[*]` or `#[=, *, *, *]`.
 -/
-def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (config : WhnfCoreConfig) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
-  let keys ← mkPath e config noIndexAtArgs
+def insertIfSpecific [BEq α] (d : DiscrTree α) (e : Expr) (v : α) (noIndexAtArgs := false) : MetaM (DiscrTree α) := do
+  let keys ← mkPath e noIndexAtArgs
   return if keys == #[Key.star] || keys == #[Key.const `Eq 3, Key.star, Key.star, Key.star] then
     d
   else
     d.insertCore keys v
 
-private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) := do
-  let e ← reduceDT e root config
+private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
+  let e ← reduceDT e root
   unless root do
     -- See pushArgs
     if let some v := toNatLit? e then
@@ -580,11 +577,11 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
   | .forallE _ d _ _ => return (.arrow, #[d])
   | _ => return (.other, #[])
 
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root) (config := config)
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := true) (root := root)
 
-private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) : MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := false) (root := root) (config := config)
+private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
+  getKeyArgs e (isMatch := false) (root := root)
 
 private def getStarResult (d : DiscrTree α) : Array α :=
   let result : Array α := .mkEmpty initCapacity
@@ -595,7 +592,7 @@ private def getStarResult (d : DiscrTree α) : Array α :=
 private abbrev findKey (cs : Array (Key × Trie α)) (k : Key) : Option (Key × Trie α) :=
   cs.binSearch (k, default) (fun a b => a.1 < b.1)
 
-private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) := do
+private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
   match c with
   | .node vs cs =>
     if todo.isEmpty then
@@ -606,48 +603,48 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
       let e     := todo.back!
       let todo  := todo.pop
       let first := cs[0]! /- Recall that `Key.star` is the minimal key -/
-      let (k, args) ← getMatchKeyArgs e (root := false) config
+      let (k, args) ← getMatchKeyArgs e (root := false)
       /- We must always visit `Key.star` edges since they are wildcards.
          Thus, `todo` is not used linearly when there is `Key.star` edge
          and there is an edge for `k` and `k != Key.star`. -/
       let visitStar (result : Array α) : MetaM (Array α) :=
         if first.1 == .star then
-          getMatchLoop todo first.2 result config
+          getMatchLoop todo first.2 result
         else
           return result
       let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
         match findKey cs k with
         | none   => return result
-        | some c => getMatchLoop (todo ++ args) c.2 result config
+        | some c => getMatchLoop (todo ++ args) c.2 result
       let result ← visitStar result
       match k with
       | .star  => return result
       | _      => visitNonStar k args result
 
-private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) (config : WhnfCoreConfig) : MetaM (Array α) :=
+private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
   match d.root.find? k with
   | none   => return result
-  | some c => getMatchLoop args c result config
+  | some c => getMatchLoop args c result
 
-private def getMatchCore (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Array α) :=
+private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
   withReducible do
     let result := getStarResult d
-    let (k, args) ← getMatchKeyArgs e (root := true) config
+    let (k, args) ← getMatchKeyArgs e (root := true)
     match k with
     | .star  => return (k, result)
-    | _      => return (k, (← getMatchRoot d k args result config))
+    | _      => return (k, (← getMatchRoot d k args result))
 
 /--
   Find values that match `e` in `d`.
 -/
-def getMatch (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) :=
-  return (← getMatchCore d e config).2
+def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
+  return (← getMatchCore d e).2
 
 /--
   Similar to `getMatch`, but returns solutions that are prefixes of `e`.
   We store the number of ignored arguments in the result.-/
-partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array (α × Nat)) := do
-  let (k, result) ← getMatchCore d e config
+partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α × Nat)) := do
+  let (k, result) ← getMatchCore d e
   let result := result.map (·, 0)
   if !e.isApp then
     return result
@@ -669,7 +666,7 @@ where
     | _               => return false
 
   go (e : Expr) (numExtra : Nat) (result : Array (α × Nat)) : MetaM (Array (α × Nat)) := do
-    let result := result ++ (← getMatchCore d e config).2.map (., numExtra)
+    let result := result ++ (← getMatchCore d e).2.map (., numExtra)
     if e.isApp then
       go e.appFn! (numExtra + 1) result
     else
@@ -678,8 +675,8 @@ where
 /--
 Return the root symbol for `e`, and the number of arguments after `reduceDT`.
 -/
-def getMatchKeyRootFor (e : Expr) (config : WhnfCoreConfig) : MetaM (Key × Nat) := do
-  let e ← reduceDT e (root := true) config
+def getMatchKeyRootFor (e : Expr) : MetaM (Key × Nat) := do
+  let e ← reduceDT e (root := true)
   let numArgs := e.getAppNumArgs
   let key := match e.getAppFn with
     | .lit v         => .lit v
@@ -716,17 +713,17 @@ We use this method to simulate Lean 3's indexing.
 
 The natural number in the result is the number of arguments in `e` after `reduceDT`.
 -/
-def getMatchLiberal (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α × Nat) := do
+def getMatchLiberal (d : DiscrTree α) (e : Expr) : MetaM (Array α × Nat) := do
   withReducible do
     let result := getStarResult d
-    let (k, numArgs) ← getMatchKeyRootFor e config
+    let (k, numArgs) ← getMatchKeyRootFor e
     match k with
     | .star  => return (result, numArgs)
     | _      => return (getAllValuesForKey d k result, numArgs)
 
-partial def getUnify (d : DiscrTree α) (e : Expr) (config : WhnfCoreConfig) : MetaM (Array α) :=
+partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
   withReducible do
-    let (k, args) ← getUnifyKeyArgs e (root := true) config
+    let (k, args) ← getUnifyKeyArgs e (root := true)
     match k with
     | .star => d.root.foldlM (init := #[]) fun result k c => process k.arity #[] c result
     | _ =>
@@ -750,7 +747,7 @@ where
       else
         let e     := todo.back!
         let todo  := todo.pop
-        let (k, args) ← getUnifyKeyArgs e (root := false) config
+        let (k, args) ← getUnifyKeyArgs e (root := false)
         let visitStar (result : Array α) : MetaM (Array α) :=
           let first := cs[0]!
           if first.1 == .star then

src/Lean/Meta/ExprDefEq.lean

@@ -2079,50 +2079,37 @@ Structure for storing defeq cache key information.
 -/
 structure DefEqCacheKeyInfo where
   kind : DefEqCacheKind
-  key  : Expr × Expr
+  key  : DefEqCacheKey
 
 private def mkCacheKey (t s : Expr) : MetaM DefEqCacheKeyInfo := do
   let kind ← getDefEqCacheKind t s
-  let key := if Expr.quickLt t s then (t, s) else (s, t)
+  let key ← mkDefEqCacheKey t s
   return { key, kind }
 
 private def getCachedResult (keyInfo : DefEqCacheKeyInfo) : MetaM LBool := do
   let cache ← match keyInfo.kind with
     | .transient => pure (← get).cache.defEqTrans
     | .permanent => pure (← get).cache.defEqPerm
-  let cache := match (← getTransparency) with
-    | .reducible => cache.reducible
-    | .instances => cache.instances
-    | .default   => cache.default
-    | .all       => cache.all
   match cache.find? keyInfo.key with
   | some val => return val.toLBool
   | none => return .undef
 
-def DefEqCache.update (cache : DefEqCache) (mode : TransparencyMode) (key : Expr × Expr) (result : Bool) : DefEqCache :=
-  match mode with
-  | .reducible => { cache with reducible := cache.reducible.insert key result }
-  | .instances => { cache with instances := cache.instances.insert key result }
-  | .default   => { cache with default   := cache.default.insert key result }
-  | .all       => { cache with all       := cache.all.insert key result }
-
 private def cacheResult (keyInfo : DefEqCacheKeyInfo) (result : Bool) : MetaM Unit := do
-  let mode ← getTransparency
   let key := keyInfo.key
   match keyInfo.kind with
-  | .permanent => modifyDefEqPermCache fun c => c.update mode key result
+  | .permanent => modifyDefEqPermCache fun c => c.insert key result
   | .transient =>
     /-
     We must ensure that all assigned metavariables in the key are replaced by their current assignments.
     Otherwise, the key is invalid after the assignment is "backtracked".
     See issue #1870 for an example.
     -/
-    let key := (← instantiateMVars key.1, ← instantiateMVars key.2)
-    modifyDefEqTransientCache fun c => c.update mode key result
+    let key ← mkDefEqCacheKey (← instantiateMVars key.lhs) (← instantiateMVars key.rhs)
+    modifyDefEqTransientCache fun c => c.insert key result
 
 private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   if backward.isDefEq.lazyWhnfCore.get (← getOptions) then
-    whnfCore e (config := { proj := .yesWithDeltaI })
+    withConfig (fun ctx => { ctx with proj := .yesWithDeltaI }) <| whnfCore e
   else
     whnfCore e
 

src/Lean/Meta/FunInfo.lean

@@ -10,13 +10,13 @@ import Lean.Meta.InferType
 namespace Lean.Meta
 
 @[inline] private def checkFunInfoCache (fn : Expr) (maxArgs? : Option Nat) (k : MetaM FunInfo) : MetaM FunInfo := do
-  let t ← getTransparency
-  match (← get).cache.funInfo.find? ⟨t, fn, maxArgs?⟩ with
-  | some finfo => pure finfo
+  let key ← mkInfoCacheKey fn maxArgs?
+  match (← get).cache.funInfo.find? key with
+  | some finfo => return finfo
   | none       => do
     let finfo ← k
-    modify fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert ⟨t, fn, maxArgs?⟩ finfo } }
-    pure finfo
+    modify fun s => { s with cache := { s.cache with funInfo := s.cache.funInfo.insert key finfo } }
+    return finfo
 
 @[inline] private def whenHasVar {α} (e : Expr) (deps : α) (k : α → α) : α :=
   if e.hasFVar then k deps else deps

src/Lean/Meta/InferType.lean

@@ -97,8 +97,8 @@ private def inferConstType (c : Name) (us : List Level) : MetaM Expr := do
 private def inferProjType (structName : Name) (idx : Nat) (e : Expr) : MetaM Expr := do
   let structType ← inferType e
   let structType ← whnf structType
-  let failed {α} : Unit → MetaM α := fun _ =>
-    throwError "invalid projection{indentExpr (mkProj structName idx e)} from type {structType}"
+  let failed {α} : Unit → MetaM α := fun _ => do
+    throwError "invalid projection{indentExpr (mkProj structName idx e)}\nfrom type{indentExpr structType}"
   matchConstStructure structType.getAppFn failed fun structVal structLvls ctorVal =>
     let structTypeArgs := structType.getAppArgs
     if structVal.numParams + structVal.numIndices != structTypeArgs.size then
@@ -165,24 +165,27 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
   | none   => fvarId.throwUnknown
 
 @[inline] private def checkInferTypeCache (e : Expr) (inferType : MetaM Expr) : MetaM Expr := do
-  match (← getTransparency) with
-  | .default =>
-    match (← get).cache.inferType.default.find? e with
+  if e.hasMVar then
+    inferType
+  else
+    let key ← mkExprConfigCacheKey e
+    match (← get).cache.inferType.find? key with
     | some type => return type
     | none =>
       let type ← inferType
-      unless e.hasMVar || type.hasMVar do
-        modifyInferTypeCacheDefault fun c => c.insert e type
+      unless type.hasMVar do
+        modifyInferTypeCache fun c => c.insert key type
       return type
-  | .all =>
-    match (← get).cache.inferType.all.find? e with
-    | some type => return type
-    | none =>
-      let type ← inferType
-      unless e.hasMVar || type.hasMVar do
-        modifyInferTypeCacheAll fun c => c.insert e type
-      return type
-  | _ => panic! "checkInferTypeCache: transparency mode not default or all"
+
+private def defaultConfig : ConfigWithKey :=
+  { : Config }.toConfigWithKey
+
+private def allConfig : ConfigWithKey :=
+  { transparency := .all : Config }.toConfigWithKey
+
+@[inline] def withInferTypeConfig (x : MetaM α) : MetaM α := do
+  let cfg := if (← getTransparency) == .all then allConfig else defaultConfig
+  withConfigWithKey cfg x
 
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
@@ -201,7 +204,7 @@ def inferTypeImp (e : Expr) : MetaM Expr :=
     | .forallE ..    => checkInferTypeCache e (inferForallType e)
     | .lam ..        => checkInferTypeCache e (inferLambdaType e)
     | .letE ..       => checkInferTypeCache e (inferLambdaType e)
-  withIncRecDepth <| withAtLeastTransparency TransparencyMode.default (infer e)
+  withIncRecDepth <| withInferTypeConfig (infer e)
 
 /--
   Return `LBool.true` if given level is always equivalent to universe level zero.

src/Lean/Meta/Instances.lean

@@ -72,9 +72,6 @@ structure Instances where
   erased        : PHashSet Name := {}
   deriving Inhabited
 
-/-- Configuration for the discrimination tree module -/
-def tcDtConfig : WhnfCoreConfig := {}
-
 def addInstanceEntry (d : Instances) (e : InstanceEntry) : Instances :=
   match e.globalName? with
   | some n => { d with discrTree := d.discrTree.insertCore e.keys e, instanceNames := d.instanceNames.insert n e, erased := d.erased.erase n }
@@ -98,7 +95,7 @@ private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
   let type ← inferType e
   withNewMCtxDepth do
     let (_, _, type) ← forallMetaTelescopeReducing type
-    DiscrTree.mkPath type tcDtConfig
+    DiscrTree.mkPath type
 
 /--
 Compute the order the arguments of `inst` should be synthesized.

src/Lean/Meta/LazyDiscrTree.lean

@@ -184,9 +184,9 @@ private def elimLooseBVarsByBeta (e : Expr) : CoreM Expr :=
       else
         return .continue)
 
-private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig) :
+private def getKeyArgs (e : Expr) (isMatch root : Bool) :
     MetaM (Key × Array Expr) := do
-  let e ← DiscrTree.reduceDT e root config
+  let e ← DiscrTree.reduceDT e root
   unless root do
     -- See pushArgs
     if let some v := toNatLit? e then
@@ -259,9 +259,9 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) (config : WhnfCoreConfig
 /-
 Given an expression we are looking for patterns that match, return the key and sub-expressions.
 -/
-private abbrev getMatchKeyArgs (e : Expr) (root : Bool) (config : WhnfCoreConfig) :
+private abbrev getMatchKeyArgs (e : Expr) (root : Bool) :
     MetaM (Key × Array Expr) :=
-  getKeyArgs e (isMatch := true) (root := root) (config := config)
+  getKeyArgs e (isMatch := true) (root := root)
 
 end MatchClone
 
@@ -313,8 +313,6 @@ discriminator key is computed and processing the remaining
 terms is deferred until demanded by a match.
 -/
 structure LazyDiscrTree (α : Type) where
-  /-- Configuration for normalization. -/
-  config : Lean.Meta.WhnfCoreConfig := {}
   /-- Backing array of trie entries.  Should be owned by this trie. -/
   tries : Array (LazyDiscrTree.Trie α) := #[default]
   /-- Map from discriminator trie roots to the index. -/
@@ -332,12 +330,12 @@ open Lean.Meta.DiscrTree (mkNoindexAnnotation hasNoindexAnnotation reduceDT)
 /--
 Specialization of Lean.Meta.DiscrTree.pushArgs
 -/
-private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) (config : WhnfCoreConfig) :
+private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) :
     MetaM (Key × Array Expr) := do
   if hasNoindexAnnotation e then
     return (.star, todo)
   else
-    let e ← reduceDT e root config
+    let e ← reduceDT e root
     let fn := e.getAppFn
     let push (k : Key) (nargs : Nat) (todo : Array Expr) : MetaM (Key × Array Expr) := do
       let info ← getFunInfoNArgs fn nargs
@@ -389,8 +387,8 @@ private def initCapacity := 8
 /--
 Get the root key and rest of terms of an expression using the specified config.
 -/
-private def rootKey (cfg: WhnfCoreConfig) (e : Expr) : MetaM (Key × Array Expr) :=
-  pushArgs true (Array.mkEmpty initCapacity) e cfg
+private def rootKey (e : Expr) : MetaM (Key × Array Expr) :=
+  pushArgs true (Array.mkEmpty initCapacity) e
 
 private partial def buildPath (op : Bool → Array Expr → Expr → MetaM (Key × Array Expr)) (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
   if todo.isEmpty then
@@ -407,9 +405,9 @@ Create a key path from an expression using the function used for patterns.
 This differs from Lean.Meta.DiscrTree.mkPath and targetPath in that the expression
 should uses free variables rather than meta-variables for holes.
 -/
-def patternPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+def patternPath (e : Expr) : MetaM (Array Key) := do
   let todo : Array Expr := .mkEmpty initCapacity
-  let op root todo e := pushArgs root todo e config
+  let op root todo e := pushArgs root todo e
   buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /--
@@ -417,21 +415,21 @@ Create a key path from an expression we are matching against.
 
 This should have mvars instantiated where feasible.
 -/
-def targetPath (e : Expr) (config : WhnfCoreConfig) : MetaM (Array Key) := do
+def targetPath (e : Expr) : MetaM (Array Key) := do
   let todo : Array Expr := .mkEmpty initCapacity
   let op root todo e := do
-        let (k, args) ← MatchClone.getMatchKeyArgs e root config
+        let (k, args) ← MatchClone.getMatchKeyArgs e root
         pure (k, todo ++ args)
   buildPath op (root := true) (todo.push e) (.mkEmpty initCapacity)
 
 /- Monad for finding matches while resolving deferred patterns. -/
 @[reducible]
-private def MatchM α := ReaderT WhnfCoreConfig (StateRefT (Array (Trie α)) MetaM)
+private def MatchM α := StateRefT (Array (Trie α)) MetaM
 
 private def runMatch (d : LazyDiscrTree α) (m : MatchM α β)  : MetaM (β × LazyDiscrTree α) := do
-  let { config := c, tries := a, roots := r } := d
-  let (result, a) ← withReducible $ (m.run c).run a
-  pure (result, { config := c, tries := a, roots := r})
+  let { tries := a, roots := r } := d
+  let (result, a) ← withReducible <| m.run a
+  return (result, { tries := a, roots := r})
 
 private def setTrie (i : TrieIndex) (v : Trie α) : MatchM α Unit :=
   modify (·.set! i v)
@@ -444,7 +442,7 @@ private def newTrie [Monad m] [MonadState (Array (Trie α)) m] (e : LazyEntry α
 private def addLazyEntryToTrie (i:TrieIndex) (e : LazyEntry α) : MatchM α Unit :=
   modify (·.modify i (·.pushPending e))
 
-private def evalLazyEntry (config : WhnfCoreConfig)
+private def evalLazyEntry
     (p : Array α × TrieIndex × Std.HashMap Key TrieIndex)
     (entry : LazyEntry α)
     : MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
@@ -456,7 +454,7 @@ private def evalLazyEntry (config : WhnfCoreConfig)
   else
     let e    := todo.back!
     let todo := todo.pop
-    let (k, todo) ← withLCtx lctx.1 lctx.2 $ pushArgs false todo e config
+    let (k, todo) ← withLCtx lctx.1 lctx.2 <| pushArgs false todo e
     if k == .star then
       if starIdx = 0 then
         let starIdx ← newTrie (todo, lctx, v)
@@ -477,26 +475,25 @@ private def evalLazyEntry (config : WhnfCoreConfig)
 This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
 accordingly.
 -/
-private partial def evalLazyEntries (config : WhnfCoreConfig)
+private partial def evalLazyEntries
     (values : Array α) (starIdx : TrieIndex) (children : Std.HashMap Key TrieIndex)
     (entries : Array (LazyEntry α)) :
     MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
   let mut values := values
   let mut starIdx := starIdx
   let mut children := children
-  entries.foldlM (init := (values, starIdx, children)) (evalLazyEntry config)
+  entries.foldlM (init := (values, starIdx, children)) evalLazyEntry
 
 private def evalNode (c : TrieIndex) :
     MatchM α (Array α × TrieIndex × Std.HashMap Key TrieIndex) := do
   let .node vs star cs pending := (←get).get! c
   if pending.size = 0 then
-    pure (vs, star, cs)
+    return (vs, star, cs)
   else
-    let config ← read
     setTrie c default
-    let (vs, star, cs) ← evalLazyEntries config vs star cs pending
+    let (vs, star, cs) ← evalLazyEntries vs star cs pending
     setTrie c <| .node vs star cs #[]
-    pure (vs, star, cs)
+    return (vs, star, cs)
 
 def dropKeyAux (next : TrieIndex) (rest : List Key) :
     MatchM α Unit :=
@@ -723,11 +720,11 @@ private def push (d : PreDiscrTree α) (k : Key) (e : LazyEntry α) : PreDiscrTr
   d.modifyAt k (·.push e)
 
 /-- Convert a pre-discrimination tree to a lazy discrimination tree. -/
-private def toLazy (d : PreDiscrTree α) (config : WhnfCoreConfig := {}) : LazyDiscrTree α :=
+private def toLazy (d : PreDiscrTree α) : LazyDiscrTree α :=
   let { roots, tries } := d
   -- Adjust trie indices so the first value is reserved (so 0 is never a valid trie index)
   let roots := roots.fold (init := roots) (fun m k n => m.insert k (n+1))
-  { config, roots, tries := #[default] ++ tries.map (.node {} 0 {}) }
+  { roots, tries := #[default] ++ tries.map (.node {} 0 {}) }
 
 /-- Merge two discrimination trees. -/
 protected def append (x y : PreDiscrTree α) : PreDiscrTree α :=
@@ -756,12 +753,12 @@ namespace InitEntry
 /--
 Constructs an initial entry from an expression and value.
 -/
-def fromExpr (expr : Expr) (value : α) (config : WhnfCoreConfig := {}) : MetaM (InitEntry α) := do
+def fromExpr (expr : Expr) (value : α) : MetaM (InitEntry α) := do
   let lctx ← getLCtx
   let linst ← getLocalInstances
   let lctx := (lctx, linst)
-  let (key, todo) ← LazyDiscrTree.rootKey config expr
-  pure <| { key, entry := (todo, lctx, value) }
+  let (key, todo) ← LazyDiscrTree.rootKey expr
+  return { key, entry := (todo, lctx, value) }
 
 /--
 Creates an entry for a subterm of an initial entry.
@@ -769,11 +766,11 @@ Creates an entry for a subterm of an initial entry.
 This is slightly more efficient than using `fromExpr` on subterms since it avoids a redundant call
 to `whnf`.
 -/
-def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) (config : WhnfCoreConfig := {}) :
+def mkSubEntry (e : InitEntry α) (idx : Nat) (value : α) :
     MetaM (InitEntry α) := do
   let (todo, lctx, _) := e.entry
-  let (key, todo) ← LazyDiscrTree.rootKey config todo[idx]!
-  pure <| { key, entry := (todo, lctx, value) }
+  let (key, todo) ← LazyDiscrTree.rootKey todo[idx]!
+  return { key, entry := (todo, lctx, value) }
 
 end InitEntry
 

src/Lean/Meta/SynthInstance.lean

@@ -207,7 +207,7 @@ def getInstances (type : Expr) : MetaM (Array Instance) := do
     | none   => throwError "type class instance expected{indentExpr type}"
     | some className =>
       let globalInstances ← getGlobalInstancesIndex
-      let result ← globalInstances.getUnify type tcDtConfig
+      let result ← globalInstances.getUnify type
       -- Using insertion sort because it is stable and the array `result` should be mostly sorted.
       -- Most instances have default priority.
       let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority

src/Lean/Meta/Tactic/Rfl.lean

@@ -19,9 +19,6 @@ namespace Lean.Meta.Rfl
 
 open Lean Meta
 
-/-- Discrimation tree settings for the `refl` extension. -/
-def reflExt.config : WhnfCoreConfig := {}
-
 /-- Environment extensions for `refl` lemmas -/
 initialize reflExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
@@ -42,7 +39,7 @@ initialize registerBuiltinAttribute {
     if let .app (.const ``Eq [_]) _ := rel then
       throwError "@[refl] attribute may not be used on `Eq.refl`."
     unless ← withNewMCtxDepth <| isDefEq lhs rhs do fail
-    let key ← DiscrTree.mkPath rel reflExt.config
+    let key ← DiscrTree.mkPath rel
     reflExt.add (decl, key) kind
 }
 
@@ -91,7 +88,7 @@ def _root_.Lean.MVarId.applyRfl (goal : MVarId) : MetaM Unit := goal.withContext
     goal.setType (.app t.appFn! lhs)
     let s ← saveState
     let mut ex? := none
-    for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+    for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
       try
         let gs ← goal.apply (← mkConstWithFreshMVarLevels lem)
         if gs.isEmpty then return () else
@@ -123,7 +120,7 @@ def _root_.Lean.MVarId.liftReflToEq (mvarId : MVarId) : MetaM MVarId := do
   if rel.isAppOf `Eq then
     -- No need to lift Eq to Eq
     return mvarId
-  for lem in ← (reflExt.getState (← getEnv)).getMatch rel reflExt.config do
+  for lem in ← (reflExt.getState (← getEnv)).getMatch rel do
     let res ← observing? do
       -- First create an equality relating the LHS and RHS
       -- and reduce the goal to proving that LHS is related to LHS.

src/Lean/Meta/Tactic/Simp/Main.lean

@@ -239,9 +239,10 @@ def withNewLemmas {α} (xs : Array Expr) (f : SimpM α) : SimpM α := do
     withFreshCache do
       let mut s ← getSimpTheorems
       let mut updated := false
+      let ctx ← getContext
       for x in xs do
         if (← isProof x) then
-          s ← s.addTheorem (.fvar x.fvarId!) x
+          s ← s.addTheorem (.fvar x.fvarId!) x (config := ctx.indexConfig)
           updated := true
       if updated then
         withSimpTheorems s f
@@ -832,7 +833,7 @@ def simpTargetStar (mvarId : MVarId) (ctx : Simp.Context) (simprocs : SimprocsAr
   for h in (← getPropHyps) do
     let localDecl ← h.getDecl
     let proof  := localDecl.toExpr
-    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof
+    let simpTheorems ← ctx.simpTheorems.addTheorem (.fvar h) proof (config := ctx.indexConfig)
     ctx := ctx.setSimpTheorems simpTheorems
   match (← simpTarget mvarId ctx simprocs discharge? (stats := stats)) with
   | (none, stats) => return (TacticResultCNM.closed, stats)

src/Lean/Meta/Tactic/Simp/Rewrite.lean

@@ -203,7 +203,7 @@ def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (tag :
 where
   /-- For `(← getConfig).index := true`, use discrimination tree structure when collecting `simp` theorem candidates. -/
   rewriteUsingIndex? : SimpM (Option Result) := do
-    let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+    let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -221,7 +221,7 @@ where
   Only the root symbol is taken into account. Most of the structure of the discrimination tree is ignored.
   -/
   rewriteNoIndex? : SimpM (Option Result) := do
-    let (candidates, numArgs) ← s.getMatchLiberal e (getDtConfig (← getConfig))
+    let (candidates, numArgs) ← withSimpIndexConfig <| s.getMatchLiberal e
     if candidates.isEmpty then
       trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"
       return none
@@ -245,7 +245,7 @@ where
 
   diagnoseWhenNoIndex (thm : SimpTheorem) : SimpM Unit := do
     if (← isDiagnosticsEnabled) then
-      let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+      let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
       for (candidate, _) in candidates do
         if unsafe ptrEq thm candidate then
           return ()

src/Lean/Meta/Tactic/Simp/SimpAll.lean

@@ -42,7 +42,8 @@ private def initEntries : M Unit := do
     unless simpThms.isErased (.fvar h) do
       let localDecl ← h.getDecl
       let proof  := localDecl.toExpr
-      simpThms ← simpThms.addTheorem (.fvar h) proof
+      let ctx := (← get).ctx
+      simpThms ← simpThms.addTheorem (.fvar h) proof (config := ctx.indexConfig)
       modify fun s => { s with ctx := s.ctx.setSimpTheorems simpThms }
       if hsNonDeps.contains h then
         -- We only simplify nondependent hypotheses
@@ -95,7 +96,7 @@ private partial def loop : M Bool := do
         trace[Meta.Tactic.simp.all] "entry.id: {← ppOrigin entry.id}, {entry.type} => {typeNew}"
         let mut simpThmsNew := (← getSimpTheorems).eraseTheorem (.fvar entry.fvarId)
         let idNew ← mkFreshId
-        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew)
+        simpThmsNew ← simpThmsNew.addTheorem (.other idNew) (← mkExpectedTypeHint proofNew typeNew) (config := ctx.indexConfig)
         modify fun s => { s with
           modified         := true
           ctx              := ctx.setSimpTheorems simpThmsNew

src/Lean/Meta/Tactic/Simp/SimpTheorems.lean

@@ -204,8 +204,18 @@ structure SimpTheorems where
   toUnfoldThms : PHashMap Name (Array Name) := {}
   deriving Inhabited
 
-/-- Configuration for the discrimination tree. -/
-def simpDtConfig : WhnfCoreConfig := { iota := false, proj := .no, zetaDelta := false }
+/--
+Configuration for `MetaM` used to process global simp theorems
+-/
+def simpGlobalConfig : ConfigWithKey :=
+  { iota         := false
+    proj         := .no
+    zetaDelta    := false
+    transparency := .reducible
+  : Config }.toConfigWithKey
+
+@[inline] def withSimpGlobalConfig : MetaM α → MetaM α :=
+  withConfigWithKey simpGlobalConfig
 
 partial def SimpTheorems.eraseCore (d : SimpTheorems) (thmId : Origin) : SimpTheorems :=
   let d := { d with erased := d.erased.insert thmId, lemmaNames := d.lemmaNames.erase thmId }
@@ -298,7 +308,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
   | s, t => return s == t
 
 private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
-  let lhs ← DiscrTree.reduceDT lhs (root := true) simpDtConfig
+  let lhs ← withSimpGlobalConfig <| DiscrTree.reduceDT lhs (root := true)
   if lhs == rhs && lhs.isFVar then
     throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"
 
@@ -381,11 +391,11 @@ private def mkSimpTheoremCore (origin : Origin) (e : Expr) (levelParams : Array
   assert! origin != .fvar ⟨.anonymous⟩
   let type ← instantiateMVars (← inferType e)
   withNewMCtxDepth do
-    let (_, _, type) ← withReducible <| forallMetaTelescopeReducing type
+    let (_, _, type) ← forallMetaTelescopeReducing type
     let type ← whnfR type
     let (keys, perm) ←
       match type.eq? with
-      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs simpDtConfig noIndexAtArgs, ← isPerm lhs rhs)
+      | some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs noIndexAtArgs, ← isPerm lhs rhs)
       | none => throwError "unexpected kind of 'simp' theorem{indentExpr type}"
     return { origin, keys, perm, post, levelParams, proof, priority := prio, rfl := (← isRflProof proof) }
 
@@ -394,7 +404,7 @@ private def mkSimpTheoremsFromConst (declName : Name) (post : Bool) (inv : Bool)
   let us := cinfo.levelParams.map mkLevelParam
   let origin := .decl declName post inv
   let val := mkConst declName us
-  withReducible do
+  withSimpGlobalConfig do
     let type ← inferType val
     checkTypeIsProp type
     if inv || (← shouldPreprocess type) then
@@ -464,18 +474,10 @@ private def preprocessProof (val : Expr) (inv : Bool) : MetaM (Array Expr) := do
   return ps.toArray.map fun (val, _) => val
 
 /-- Auxiliary method for creating simp theorems from a proof term `val`. -/
-def mkSimpTheorems (id : Origin) (levelParams : Array Name) (proof : Expr) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) :=
+private def mkSimpTheorems (id : Origin) (levelParams : Array Name) (proof : Expr) (post := true) (inv := false) (prio : Nat := eval_prio default) : MetaM (Array SimpTheorem) :=
   withReducible do
     (← preprocessProof proof inv).mapM fun val => mkSimpTheoremCore id val levelParams val post prio (noIndexAtArgs := true)
 
-/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/
-def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr) (inv := false) (post := true) (prio : Nat := eval_prio default) : MetaM SimpTheorems := do
-  if proof.isConst then
-    s.addConst proof.constName! post inv prio
-  else
-    let simpThms ← mkSimpTheorems id levelParams proof post inv prio
-    return simpThms.foldl addSimpTheoremEntry s
-
 /--
 Reducible functions and projection functions should always be put in `toUnfold`, instead
 of trying to use equational theorems.
@@ -533,14 +535,25 @@ def SimpTheorems.addDeclToUnfold (d : SimpTheorems) (declName : Name) : MetaM Si
   else
     return d.addDeclToUnfoldCore declName
 
+/-- Auxiliary method for adding a local simp theorem to a `SimpTheorems` datastructure. -/
+def SimpTheorems.add (s : SimpTheorems) (id : Origin) (levelParams : Array Name) (proof : Expr)
+        (inv := false) (post := true) (prio : Nat := eval_prio default)
+        (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheorems := do
+  if proof.isConst then
+    -- Recall that we use `simpGlobalConfig` for processing global declarations.
+    s.addConst proof.constName! post inv prio
+  else
+    let simpThms ← withConfigWithKey config <| mkSimpTheorems id levelParams proof post inv prio
+    return simpThms.foldl addSimpTheoremEntry s
+
 abbrev SimpTheoremsArray := Array SimpTheorems
 
-def SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) : MetaM SimpTheoremsArray :=
+def SimpTheoremsArray.addTheorem (thmsArray : SimpTheoremsArray) (id : Origin) (h : Expr) (config : ConfigWithKey := simpGlobalConfig) : MetaM SimpTheoremsArray :=
   if thmsArray.isEmpty then
     let thms : SimpTheorems := {}
-    return #[ (← thms.add id #[] h) ]
+    return #[ (← thms.add id #[] h (config := config)) ]
   else
-    thmsArray.modifyM 0 fun thms => thms.add id #[] h
+    thmsArray.modifyM 0 fun thms => thms.add id #[] h (config := config)
 
 def SimpTheoremsArray.eraseTheorem (thmsArray : SimpTheoremsArray) (thmId : Origin) : SimpTheoremsArray :=
   thmsArray.map fun thms => thms.eraseCore thmId

src/Lean/Meta/Tactic/Simp/Simproc.lean

@@ -213,7 +213,7 @@ def SimprocEntry.tryD (s : SimprocEntry) (numExtraArgs : Nat) (e : Expr) : SimpM
   | .inr proc => return (← proc e).addExtraArgs extraArgs
 
 def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM Step := do
-  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"
@@ -250,7 +250,7 @@ def simprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Ex
       return .continue
 
 def dsimprocCore (post : Bool) (s : SimprocTree) (erased : PHashSet Name) (e : Expr) : SimpM DStep := do
-  let candidates ← s.getMatchWithExtra e (getDtConfig (← getConfig))
+  let candidates ← withSimpIndexConfig <| s.getMatchWithExtra e
   if candidates.isEmpty then
     let tag := if post then "post" else "pre"
     trace[Debug.Meta.Tactic.simp] "no {tag}-simprocs found for {e}"

src/Lean/Meta/Tactic/Simp/Types.lean

@@ -53,7 +53,9 @@ abbrev CongrCache := ExprMap (Option CongrTheorem)
 
 structure Context where
   private mk ::
-  config           : Config := {}
+  config            : Config := {}
+  metaConfig        : ConfigWithKey := default
+  indexConfig       : ConfigWithKey := default
   /-- `maxDischargeDepth` from `config` as an `UInt32`. -/
   maxDischargeDepth : UInt32 := UInt32.ofNatTruncate config.maxDischargeDepth
   simpTheorems      : SimpTheoremsArray := {}
@@ -117,9 +119,32 @@ private def updateArith (c : Config) : CoreM Config := do
   else
     return c
 
+/--
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for indexing.
+-/
+private def mkIndexConfig (c : Config) : ConfigWithKey :=
+  { c with
+    proj         := .no
+    transparency := .reducible
+  : Meta.Config }.toConfigWithKey
+
+/--
+Converts `Simp.Config` into `Meta.ConfigWithKey` used for `isDefEq`.
+-/
+-- TODO: use `metaConfig` at `isDefEq`. It is not being used yet because it will break Mathlib.
+private def mkMetaConfig (c : Config) : ConfigWithKey :=
+  { c with
+    proj         := if c.proj then .yesWithDelta else .no
+    transparency := .reducible
+  : Meta.Config }.toConfigWithKey
+
 def mkContext (config : Config := {}) (simpTheorems : SimpTheoremsArray := {}) (congrTheorems : SimpCongrTheorems := {}) : MetaM Context := do
   let config ← updateArith config
-  return { config, simpTheorems, congrTheorems }
+  return {
+    config, simpTheorems, congrTheorems
+    metaConfig := mkMetaConfig config
+    indexConfig := mkIndexConfig config
+  }
 
 def Context.setConfig (context : Context) (config : Config) : Context :=
   { context with config }
@@ -203,6 +228,15 @@ abbrev SimpM := ReaderT MethodsRef $ ReaderT Context $ StateRefT State MetaM
 @[inline] def withInDSimp : SimpM α → SimpM α :=
   withTheReader Context (fun ctx => { ctx with inDSimp := true })
 
+/--
+Executes `x` using a `MetaM` configuration for indexing terms.
+It is inferred from `Simp.Config`.
+For example, if the user has set `simp (config := { zeta := false })`,
+`isDefEq` and `whnf` in `MetaM` should not perform `zeta` reduction.
+-/
+@[inline] def withSimpIndexConfig (x : SimpM α) : SimpM α := do
+  withConfigWithKey (← readThe Simp.Context).indexConfig x
+
 @[extern "lean_simp"]
 opaque simp (e : Expr) : SimpM Result
 
@@ -679,16 +713,6 @@ def tryAutoCongrTheorem? (e : Expr) : SimpM (Option Result) := do
     /- See comment above. This is reachable if `hasCast == true`. The `rhs` is not structurally equal to `mkAppN f argsNew` -/
     return some { expr := rhs }
 
-/--
-Return a WHNF configuration for retrieving `[simp]` from the discrimination tree.
-If user has disabled `zeta` and/or `beta` reduction in the simplifier, or enabled `zetaDelta`,
-we must also disable/enable them when retrieving lemmas from discrimination tree. See issues: #2669 and #2281
--/
-def getDtConfig (cfg : Config) : WhnfCoreConfig :=
-  match cfg.beta, cfg.zeta, cfg.zetaDelta with
-  | true, true, false => simpDtConfig
-  | _,    _,    _     => { simpDtConfig with zeta := cfg.zeta, beta := cfg.beta, zetaDelta := cfg.zetaDelta }
-
 def Result.addExtraArgs (r : Result) (extraArgs : Array Expr) : MetaM Result := do
   match r.proof? with
   | none => return { expr := mkAppN r.expr extraArgs }

src/Lean/Meta/Tactic/Symm.lean

@@ -18,9 +18,6 @@ open Lean Meta
 
 namespace Lean.Meta.Symm
 
-/-- Discrimation tree settings for the `symm` extension. -/
-def symmExt.config : WhnfCoreConfig := {}
-
 /-- Environment extensions for symm lemmas -/
 builtin_initialize symmExt :
     SimpleScopedEnvExtension (Name × Array DiscrTree.Key) (DiscrTree Name) ←
@@ -40,7 +37,7 @@ builtin_initialize registerBuiltinAttribute {
     let some _ := xs.back? | fail
     let targetTy ← reduce targetTy
     let .app (.app rel _) _ := targetTy | fail
-    let key ← withReducible <| DiscrTree.mkPath rel symmExt.config
+    let key ← withReducible <| DiscrTree.mkPath rel
     symmExt.add (decl, key) kind
 }
 
@@ -54,7 +51,7 @@ namespace Lean.Expr
 def getSymmLems (tgt : Expr) : MetaM (Array Name) := do
   let .app (.app rel _) _ := tgt
     | throwError "symmetry lemmas only apply to binary relations, not{indentExpr tgt}"
-  (symmExt.getState (← getEnv)).getMatch rel symmExt.config
+  (symmExt.getState (← getEnv)).getMatch rel
 
 /-- Given a term `e : a ~ b`, construct a term in `b ~ a` using `@[symm]` lemmas. -/
 def applySymm (e : Expr) : MetaM Expr := do

src/Lean/Meta/UnificationHint.lean

@@ -6,6 +6,7 @@ Authors: Leonardo de Moura
 prelude
 import Lean.ScopedEnvExtension
 import Lean.Util.Recognizers
+import Lean.Meta.Basic
 import Lean.Meta.DiscrTree
 import Lean.Meta.SynthInstance
 
@@ -27,7 +28,8 @@ structure UnificationHints where
 instance : ToFormat UnificationHints where
   format h := format h.discrTree
 
-def UnificationHints.config : WhnfCoreConfig := { iota := false, proj := .no }
+private def config : ConfigWithKey :=
+  { iota := false, proj := .no : Config }.toConfigWithKey
 
 def UnificationHints.add (hints : UnificationHints) (e : UnificationHintEntry) : UnificationHints :=
   { hints with discrTree := hints.discrTree.insertCore e.keys e.val }
@@ -81,7 +83,7 @@ def addUnificationHint (declName : Name) (kind : AttributeKind) : MetaM Unit :=
       match decodeUnificationHint body with
       | Except.error msg => throwError msg
       | Except.ok hint =>
-        let keys ← DiscrTree.mkPath hint.pattern.lhs UnificationHints.config
+        let keys ← withConfigWithKey config <| DiscrTree.mkPath hint.pattern.lhs
         validateHint hint
         unificationHintExtension.add { keys := keys, val := declName } kind
 
@@ -101,7 +103,7 @@ def tryUnificationHints (t s : Expr) : MetaM Bool := do
   if t.isMVar then
     return false
   let hints := unificationHintExtension.getState (← getEnv)
-  let candidates ← hints.discrTree.getMatch t UnificationHints.config
+  let candidates ← withConfigWithKey config <| hints.discrTree.getMatch t
   for candidate in candidates do
     if (← tryCandidate candidate) then
       return true

src/Lean/Meta/WHNF.lean

@@ -328,65 +328,8 @@ end
 /-! # Weak Head Normal Form auxiliary combinators -/
 -- ===========================
 
-/--
-Configuration for projection reduction. See `whnfCore`.
--/
-inductive ProjReductionKind where
-  /-- Projections `s.i` are not reduced at `whnfCore`. -/
-  | no
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfCore` is used at `s` during the process.
-  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations).
-  -/
-  | yes
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnf` is used at `s` during the process.
-  Recall that `whnfCore` does not perform `delta` reduction (i.e., it will not unfold constant declarations), but `whnf` does.
-  -/
-  | yesWithDelta
-  /--
-  Projections `s.i` are reduced at `whnfCore`, and `whnfAtMostI` is used at `s` during the process.
-  Recall that `whnfAtMostI` is like `whnf` but uses transparency at most `instances`.
-  This option is stronger than `yes`, but weaker than `yesWithDelta`.
-  We use this option to ensure we reduce projections to prevent expensive defeq checks when unifying TC operations.
-  When unifying e.g. `(@Field.toNeg α inst1).1 =?= (@Field.toNeg α inst2).1`,
-  we only want to unify negation (and not all other field operations as well).
-  Unifying the field instances slowed down unification: https://github.com/leanprover/lean4/issues/1986
-  -/
-  | yesWithDeltaI
-  deriving DecidableEq, Inhabited, Repr
-
-/--
-Configuration options for `whnfEasyCases` and `whnfCore`.
--/
-structure WhnfCoreConfig where
-  /-- If `true`, reduce recursor/matcher applications, e.g., `Nat.rec true (fun _ _ => false) Nat.zero` reduces to `true` -/
-  iota : Bool := true
-  /-- If `true`, reduce terms such as `(fun x => t[x]) a` into `t[a]` -/
-  beta : Bool := true
-  /-- Control projection reduction at `whnfCore`. -/
-  proj : ProjReductionKind := .yesWithDelta
-  /--
-  Zeta reduction: `let x := v; e[x]` reduces to `e[v]`.
-  We say a let-declaration `let x := v; e` is non dependent if it is equivalent to `(fun x => e) v`.
-  Recall that
-  ```
-  fun x : BitVec 5 => let n := 5; fun y : BitVec n => x = y
-  ```
-  is type correct, but
-  ```
-  fun x : BitVec 5 => (fun n => fun y : BitVec n => x = y) 5
-  ```
-  is not.
-  -/
-  zeta : Bool := true
-  /--
-  Zeta-delta reduction: given a local context containing entry `x : t := e`, free variable `x` reduces to `e`.
-  -/
-  zetaDelta : Bool := true
-
 /-- Auxiliary combinator for handling easy WHNF cases. It takes a function for handling the "hard" cases as an argument -/
-@[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) (config : WhnfCoreConfig := {}) : MetaM Expr := do
+@[specialize] partial def whnfEasyCases (e : Expr) (k : Expr → MetaM Expr) : MetaM Expr := do
   match e with
   | .forallE ..    => return e
   | .lam ..        => return e
@@ -397,7 +340,7 @@ structure WhnfCoreConfig where
   | .const ..      => k e
   | .app ..        => k e
   | .proj ..       => k e
-  | .mdata _ e     => whnfEasyCases e k config
+  | .mdata _ e     => whnfEasyCases e k
   | .fvar fvarId   =>
     let decl ← fvarId.getDecl
     match decl with
@@ -405,13 +348,14 @@ structure WhnfCoreConfig where
     | .ldecl (value := v) .. =>
       -- Let-declarations marked as implementation detail should always be unfolded
       -- We initially added this feature for `simp`, and added it here for consistency.
-      unless config.zetaDelta || decl.isImplementationDetail do return e
-      if (← getConfig).trackZetaDelta then
+      let cfg ← getConfig
+      unless cfg.zetaDelta || decl.isImplementationDetail do return e
+      if cfg.trackZetaDelta then
         modify fun s => { s with zetaDeltaFVarIds := s.zetaDeltaFVarIds.insert fvarId }
-      whnfEasyCases v k config
+      whnfEasyCases v k
   | .mvar mvarId   =>
     match (← getExprMVarAssignment? mvarId) with
-    | some v => whnfEasyCases v k config
+    | some v => whnfEasyCases v k
     | none   => return e
 
 @[specialize] private def deltaDefinition (c : ConstantInfo) (lvls : List Level)
@@ -611,30 +555,31 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
 Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
 expand let-expressions, expand assigned meta-variables.
 -/
-partial def whnfCore (e : Expr) (config : WhnfCoreConfig := {}): MetaM Expr :=
+partial def whnfCore (e : Expr) : MetaM Expr :=
   go e
 where
   go (e : Expr) : MetaM Expr :=
-    whnfEasyCases e (config := config) fun e => do
+    whnfEasyCases e fun e => do
       trace[Meta.whnf] e
       match e with
       | .const ..  => pure e
-      | .letE _ _ v b _ => if config.zeta then go <| b.instantiate1 v else return e
+      | .letE _ _ v b _ => if (← getConfig).zeta then go <| b.instantiate1 v else return e
       | .app f ..       =>
-        if config.zeta then
+        let cfg ← getConfig
+        if cfg.zeta then
           if let some (args, _, _, v, b) := e.letFunAppArgs? then
             -- When zeta reducing enabled, always reduce `letFun` no matter the current reducibility level
             return (← go <| mkAppN (b.instantiate1 v) args)
         let f := f.getAppFn
         let f' ← go f
-        if config.beta && f'.isLambda then
+        if cfg.beta && f'.isLambda then
           let revArgs := e.getAppRevArgs
           go <| f'.betaRev revArgs
         else if let some eNew ← whnfDelayedAssigned? f' e then
           go eNew
         else
           let e := if f == f' then e else e.updateFn f'
-          unless config.iota do return e
+          unless cfg.iota do return e
           match (← reduceMatcher? e) with
           | .reduced eNew => go eNew
           | .partialApp   => pure e
@@ -656,7 +601,7 @@ where
           match (← projectCore? c i) with
           | some e => go e
           | none => return e
-        match config.proj with
+        match (← getConfig).proj with
         | .no => return e
         | .yes => k (← go c)
         | .yesWithDelta => k (← whnf c)
@@ -967,26 +912,18 @@ def reduceNat? (e : Expr) : MetaM (Option Expr) :=
   if e.hasFVar || e.hasExprMVar || (← read).canUnfold?.isSome then
     return false
   else
-    match (← getConfig).transparency with
-    | .default => return true
-    | .all     => return true
-    | _        => return false
+    return true
 
 @[inline] private def cached? (useCache : Bool) (e : Expr) : MetaM (Option Expr) := do
   if useCache then
-    match (← getConfig).transparency with
-    | .default => return (← get).cache.whnfDefault.find? e
-    | .all     => return (← get).cache.whnfAll.find? e
-    | _        => unreachable!
+    return (← get).cache.whnf.find? (← mkExprConfigCacheKey e)
   else
     return none
 
 private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
   if useCache then
-    match (← getConfig).transparency with
-    | .default => modify fun s => { s with cache.whnfDefault := s.cache.whnfDefault.insert e r }
-    | .all     => modify fun s => { s with cache.whnfAll     := s.cache.whnfAll.insert e r }
-    | _        => unreachable!
+    let key ← mkExprConfigCacheKey e
+    modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
 @[export lean_whnf]

tests/lean/1018unknowMVarIssue.lean.expected.out

@@ -56,8 +56,8 @@ a : α
           • Fam2.any : Fam2 α α @ ⟨9, 4⟩†-⟨9, 12⟩†
             • α : Type @ ⟨9, 4⟩†-⟨9, 12⟩†
           • a (isBinder := true) : α @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.585 -> _uniq.312
-          • FVarAlias α: _uniq.584 -> _uniq.310
+          • FVarAlias a: _uniq.588 -> _uniq.315
+          • FVarAlias α: _uniq.587 -> _uniq.313
           • ?m x α a : α @ ⟨9, 18⟩-⟨9, 19⟩ @ Lean.Elab.Term.elabHole
           • [.] Fam2.nat : none @ ⟨10, 4⟩-⟨10, 12⟩
           • Fam2.nat : Nat → Fam2 Nat Nat @ ⟨10, 4⟩-⟨10, 12⟩
@@ -71,8 +71,8 @@ a : α
           • Fam2.nat n : Fam2 Nat Nat @ ⟨10, 4⟩†-⟨10, 14⟩
             • n (isBinder := true) : Nat @ ⟨10, 13⟩-⟨10, 14⟩
           • a (isBinder := true) : Nat @ ⟨8, 2⟩†-⟨10, 19⟩†
-          • FVarAlias a: _uniq.616 -> _uniq.312
-          • FVarAlias n: _uniq.615 -> _uniq.310
+          • FVarAlias a: _uniq.619 -> _uniq.315
+          • FVarAlias n: _uniq.618 -> _uniq.313
           • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩ @ Lean.Elab.Term.elabIdent
             • [.] n : some Nat @ ⟨10, 18⟩-⟨10, 19⟩
             • n : Nat @ ⟨10, 18⟩-⟨10, 19⟩

tests/lean/letFun.lean

@@ -55,10 +55,10 @@ Exercise `isDefEqQuick` for `let_fun`.
 Check that `let_fun` responds to WHNF's `zeta` option.
 -/
 
-open Lean Elab Term in
+open Lean Meta Elab Term in
 elab "#whnfCore " z?:(&"noZeta")? t:term : command => Command.runTermElabM fun _ => do
   let e ← withSynthesize <| Term.elabTerm t none
-  let e ← Meta.whnfCore e {zeta := z?.isNone}
+  let e ← withConfig (fun c => { c with zeta := z?.isNone }) <| Meta.whnfCore e
   logInfo m!"{e}"
 
 #whnfCore let_fun n := 5; n

tests/lean/run/ack.lean

@@ -5,14 +5,16 @@ def ack : Nat → Nat → Nat
 termination_by a b => (a, b)
 
 /--
-info: [reduction] unfolded declarations (max: 1725, num: 4):
-  [reduction] Nat.rec ↦ 1725
-  [reduction] Eq.rec ↦ 1114
-  [reduction] Acc.rec ↦ 1050
-  [reduction] PSigma.rec ↦ 513[reduction] unfolded reducible declarations (max: 1577, num: 3):
-  [reduction] Nat.casesOn ↦ 1577
-  [reduction] Eq.ndrec ↦ 984
-  [reduction] PSigma.casesOn ↦ 513[kernel] unfolded declarations (max: 1193, num: 5):
+info: [reduction] unfolded declarations (max: 2567, num: 5):
+  [reduction] Nat.rec ↦ 2567
+  [reduction] Eq.rec ↦ 1517
+  [reduction] Acc.rec ↦ 1158
+  [reduction] Or.rec ↦ 770
+  [reduction] PSigma.rec ↦ 514[reduction] unfolded reducible declarations (max: 2337, num: 4):
+  [reduction] Nat.casesOn ↦ 2337
+  [reduction] Eq.ndrec ↦ 1307
+  [reduction] Or.casesOn ↦ 770
+  [reduction] PSigma.casesOn ↦ 514[kernel] unfolded declarations (max: 1193, num: 5):
   [kernel] Nat.casesOn ↦ 1193
   [kernel] Nat.rec ↦ 1065
   [kernel] Eq.ndrec ↦ 973

tests/lean/run/meta3.lean

@@ -34,25 +34,25 @@ def add  := mkAppN (mkConst `Add.add [levelZero]) #[nat, mkConst `Nat.add]
 def tst1 : MetaM Unit :=
 do let d : DiscrTree Nat := {};
    let mvar ← mkFreshExprMVar nat;
-   let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1 {}
-   let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2 {}
-   let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3 {}
-   let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4 {}
-   let d ← d.insert mvar 5 {}
+   let d ← d.insert (mkAppN add #[mvar, mkNatLit 10]) 1
+   let d ← d.insert (mkAppN add #[mkNatLit 0, mkNatLit 10]) 2
+   let d ← d.insert (mkAppN (mkConst `Nat.add) #[mkNatLit 0, mkNatLit 20]) 3
+   let d ← d.insert (mkAppN add #[mvar, mkNatLit 20]) 4
+   let d ← d.insert mvar 5
    print (format d);
-   let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]) {};
+   let vs ← d.getMatch (mkAppN add #[mkNatLit 1, mkNatLit 10]);
    print (format vs);
    let t := mkAppN add #[mvar, mvar];
    print t;
-   let vs ← d.getMatch t {};
+   let vs ← d.getMatch t
    print (format vs);
-   let vs ← d.getUnify t {};
+   let vs ← d.getUnify t;
    print (format vs);
-   let vs ← d.getUnify mvar {};
+   let vs ← d.getUnify mvar;
    print (format vs);
-   let vs ← d.getUnify (mkAppN add #[mkNatLit 0, mvar]) {};
+   let vs ← d.getUnify (mkAppN add #[mkNatLit 0, mvar]);
    print (format vs);
-   let vs ← d.getUnify (mkAppN add #[mvar, mkNatLit 20]) {};
+   let vs ← d.getUnify (mkAppN add #[mvar, mkNatLit 20]);
    print (format vs);
    pure ()
 

tests/lean/run/meta5.lean

@@ -28,11 +28,11 @@ info: [Meta.debug] ?_
 [Meta.debug] fun y =>
       let x := 0;
       x.add y
-[Meta.debug] ?_uniq.3019 : Nat →
+[Meta.debug] ?_uniq.3037 : Nat
+[Meta.debug] ?_uniq.3038 : Nat →
       Nat →
         let x := 0;
         Nat
-[Meta.debug] ?_uniq.3018 : Nat
 -/
 #guard_msgs in
 #eval tst1

tests/lean/run/simp1.lean

@@ -44,7 +44,7 @@ def tst2 : MetaM Unit := do
     | some (_, lhs, _) =>
       trace[Meta.debug] "lhs: {lhs}"
       let s ← Meta.getSimpTheorems
-      let m ← s.post.getMatch lhs {}
+      let m ← s.post.getMatch lhs
       trace[Meta.debug] "result: {m}"
       assert! m.any fun s => s.origin == .decl `ex2