perf: mark ReaderT context argument as borrow

src/Init/Prelude.lean

@@ -4082,7 +4082,7 @@ Actions in the resulting monad are functions that take the local value as a para
 ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type (max u v) :=
-  ρ → m α
+  (a : @&ρ) → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.

src/Lean/Compiler/IR/AddExtern.lean

@@ -21,6 +21,7 @@ public section
 
 namespace Lean.IR
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_add_extern]
 def addExtern (declName : Name) (externAttrData : ExternAttrData) : CoreM Unit := do
   if !isPrivateName declName then

src/Lean/Elab/PreDefinition/Structural/Eqns.lean

@@ -184,6 +184,7 @@ def getUnfoldFor? (declName : Name) : MetaM (Option Name) := do
   else
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_structural_rec_arg_pos]
 def getStructuralRecArgPosImp? (declName : Name) : CoreM (Option Nat) := do
   let some info := eqnInfoExt.find? (← getEnv) declName | return none

src/Lean/Elab/Tactic/Try.lean

@@ -787,6 +787,7 @@ where
           throw ex
 
 -- `evalSuggest` implementation
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_eval_suggest_tactic]
 private partial def evalSuggestImpl : TryTactic := fun tac => do
   trace[try.debug] "{tac}"

src/Lean/Meta/ExprDefEq.lean

@@ -1126,6 +1126,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
       return none
     return some v
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Implementation for `_root_.Lean.MVarId.checkedAssign`
 @[export lean_checked_assign]
 def checkedAssignImpl (mvarId : MVarId) (val : Expr) : MetaM Bool := do
@@ -2233,6 +2234,7 @@ private def whnfCoreAtDefEq (e : Expr) : MetaM Expr := do
   else
     whnfCore e
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_is_expr_def_eq]
 partial def isExprDefEqAuxImpl (t : Expr) (s : Expr) : MetaM Bool := withIncRecDepth do
   withTraceNodeBefore `Meta.isDefEq (fun _ => return m!"{t} =?= {s}") do

src/Lean/Meta/InferType.lean

@@ -206,6 +206,7 @@ because it overrides unrelated configurations.
     else
       withConfig (fun cfg => { cfg with beta := true, iota := true, zeta := true, zetaHave := true, zetaDelta := true, proj := .yesWithDelta, etaStruct := .all }) x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_infer_type]
 def inferTypeImp (e : Expr) : MetaM Expr :=
   let rec infer (e : Expr) :  MetaM Expr := do

src/Lean/Meta/LevelDefEq.lean

@@ -85,6 +85,7 @@ private def isMVarWithGreaterDepth (v : Level) (mvarId : LMVarId) : MetaM Bool :
   | Level.mvar mvarId' => return (← mvarId'.getLevel) > (← mvarId.getLevel)
   | _ => return false
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
 
   private partial def solve (u v : Level) : MetaM LBool := do

src/Lean/Meta/Match/MatchEqs.lean

@@ -138,6 +138,7 @@ Creates conditional equations and splitter for the given match auxiliary declara
 
 See also `getEquationsFor`.
 -/
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_get_match_equations_for]
 def getEquationsForImpl (matchDeclName : Name) : MetaM MatchEqns := do
   /-
@@ -246,6 +247,7 @@ where go baseName splitterName := withConfig (fun c => { c with etaStruct := .no
     let result := { eqnNames, splitterName, splitterMatchInfo }
     registerMatchEqns matchDeclName result
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Generate the congruence equations for the given match auxiliary declaration.
 The congruence equations have a completely unrestricted left-hand side (arbitrary discriminants),

src/Lean/Meta/Sym/Pattern.lean

@@ -785,6 +785,7 @@ def isDefEqApp (tFn : Expr) (t : Expr) (s : Expr) (_ : tFn = t.getAppFn) : DefEq
   let numArgs := t.getAppNumArgs
   isDefEqAppWithInfo t s (numArgs - 1) info
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 `isDefEqMain` implementation.
 -/

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

@@ -40,6 +40,7 @@ abbrev cacheResult (e : Expr) (r : Result) : SimpM Result := do
     modify fun s => { s with persistentCache := s.persistentCache.insert { expr := e } r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_sym_simp]
 def simpImpl (e₁ : Expr) : SimpM Result := withIncRecDepth do
   let numSteps := (← get).numSteps

src/Lean/Meta/SynthInstance.lean

@@ -944,6 +944,7 @@ def synthInstance (type : Expr) (maxResultSize? : Option Nat := none) : MetaM Ex
       | none        => throwFailedToSynthesize type)
     (fun _ => throwFailedToSynthesize type)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_synth_pending]
 private def synthPendingImp (mvarId : MVarId) : MetaM Bool := withIncRecDepth <| mvarId.withContext do
   let mvarDecl ← mvarId.getDecl

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean

@@ -276,6 +276,7 @@ private def propagateNonlinearPow (x : Var) : GoalM Bool := do
   c'.assert
   return true
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_cutsat_propagate_nonlinear]
 def propagateNonlinearTermImpl (y : Var) (x : Var) : GoalM Bool := do
   unless (← isVarEqConst? y).isSome do return false
@@ -338,6 +339,7 @@ partial def _root_.Int.Linear.Poly.updateOccsForElimEq (p : Poly) (x : Var) : Go
     go p
   go p
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_eq]
 def EqCnstr.assertImpl (c : EqCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean

@@ -99,6 +99,7 @@ where
         return some { p := c.p.addConst 1, h := .ofLeDiseq c c' }
     return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_assert_le]
 def LeCnstr.assertImpl (c : LeCnstr) : GoalM Unit := do
   if (← inconsistent) then return ()

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -325,7 +325,9 @@ private def mkPowEqProof (ka : Int) (ca? : Option EqCnstr) (kb : Nat) (cb? : Opt
   let h := mkApp8 (mkConst ``Int.Linear.pow_eq) a b (toExpr ka) (toExpr kbInt) (toExpr k) h₁ h₂ eagerReflBoolTrue
   return mkApp6 (mkConst ``Int.Linear.of_var_eq) (← getContext) (← mkVarDecl x) (toExpr k) (← mkPolyDecl c'.p) eagerReflBoolTrue h
 
+set_option compiler.ignoreBorrowAnnotation true in
 mutual
+
 @[export lean_cutsat_eq_cnstr_to_proof]
 private partial def EqCnstr.toExprProofImpl (c' : EqCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.lia.proof] "{← c'.pp}"

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Var.lean

@@ -64,6 +64,7 @@ where
         registerNonlinearOcc e x
     | _ => registerNonlinearOcc e x
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_cutsat_mk_var]
 def mkVarImpl (expr : Expr) : GoalM Var := do
   if let some var := (← get').varMap.find? { expr } then

src/Lean/Meta/Tactic/Grind/Canon.lean

@@ -239,6 +239,7 @@ private def normOfNatArgs? (args : Array Expr) : MetaM (Option (Array Expr)) :=
       return some args.toArray
   return none
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_canon]
 partial def canonImpl (e : Expr) : GoalM Expr := do profileitM Exception "grind canon" (← getOptions) do
   trace_goal[grind.debug.canon] "{e}"

src/Lean/Meta/Tactic/Grind/Core.lean

@@ -348,6 +348,7 @@ where
       internalize rhs generation p
       addEqCore lhs rhs proof isHEq
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_process_new_facts]
 private def processNewFactsImpl : GoalM Unit := do
   repeat

src/Lean/Meta/Tactic/Grind/Internalize.lean

@@ -535,6 +535,7 @@ private def internalizeOfNatFinBitVecLiteral (e : Expr) (generation : Nat) (pare
   updateIndicesFound (.const ``OfNat.ofNat)
   activateTheorems ``OfNat.ofNat generation
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_internalize]
 private partial def internalizeImpl (e : Expr) (generation : Nat) (parent? : Option Expr := none) : GoalM Unit := withIncRecDepth do
   if (← alreadyInternalized e) then

src/Lean/Meta/Tactic/Grind/Proof.lean

@@ -328,6 +328,7 @@ mutual
 
 end
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Returns a proof that `a = b`.
 It assumes `a` and `b` are in the same equivalence class.
@@ -338,6 +339,7 @@ def mkEqProofImpl (a b : Expr) : GoalM Expr := do
     throwError "internal `grind` error, `mkEqProof` invoked with terms of different types{indentExpr a}\nhas type{indentExpr (← inferType a)}\nbut{indentExpr b}\nhas type{indentExpr (← inferType b)}"
   mkEqProofCore a b (heq := false)
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_mk_heq_proof]
 def mkHEqProofImpl (a b : Expr) : GoalM Expr :=
   mkEqProofCore a b (heq := true)

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

@@ -42,6 +42,7 @@ def dsimpCore (e : Expr) : GrindM Expr := do profileitM Exception "grind dsimp"
   modify fun s => { s with simp }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 /--
 Preprocesses `e` using `grind` normalization theorems and simprocs,
 and then applies several other preprocessing steps.

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

@@ -202,6 +202,7 @@ protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
     (simpTheorems := #[thms])
     (congrTheorems := (← getSimpCongrTheorems))
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_grind_normalize]
 def normalizeImp (e : Expr) (config : Grind.Config) : MetaM Expr := do
   let (r, _) ← Meta.simp e (← Grind.getSimpContext config) (← Grind.getSimprocs)

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

@@ -512,6 +512,7 @@ Auxiliary `dsimproc` for not visiting `Char` literal subterms.
 -/
 private def doNotVisitCharLit : DSimproc := doNotVisit isCharLit ``Char.ofNat
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_dsimp]
 private partial def dsimpImpl (e : Expr) : SimpM Expr := do
   let cfg ← getConfig
@@ -710,6 +711,7 @@ where
       r ← r.mkEqTrans (← simpLoop r.expr)
     cacheResult e cfg r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_simp]
 def simpImpl (e : Expr) : SimpM Result := withIncRecDepth do
   checkSystem "simp"

src/Lean/Meta/WHNF.lean

@@ -1100,6 +1100,7 @@ private def cache (useCache : Bool) (e r : Expr) : MetaM Expr := do
     modify fun s => { s with cache.whnf := s.cache.whnf.insert key r }
   return r
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_whnf]
 partial def whnfImp (e : Expr) : MetaM Expr :=
   withIncRecDepth <| whnfEasyCases e fun e => do

src/Lean/Parser.lean

@@ -65,6 +65,7 @@ end Parser
 namespace PrettyPrinter
 namespace Parenthesizer
 
+set_option compiler.ignoreBorrowAnnotation true in
 -- Close the mutual recursion loop; see corresponding `[extern]` in the parenthesizer.
 @[export lean_mk_antiquot_parenthesizer]
 def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Parenthesizer :=
@@ -80,6 +81,7 @@ def mkAntiquot.parenthesizer (name : String) (kind : SyntaxNodeKind) (anonymous
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_parenthesizer_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Parenthesizer
   | ParserDescr.const n                             => getConstAlias parenthesizerAliasesRef n
@@ -101,6 +103,7 @@ end Parenthesizer
 
 namespace Formatter
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_mk_antiquot_formatter]
 def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := true) (isPseudoKind := true) : Formatter :=
   Parser.mkAntiquot.formatter name kind anonymous isPseudoKind
@@ -113,6 +116,7 @@ def mkAntiquot.formatter (name : String) (kind : SyntaxNodeKind) (anonymous := t
 
 open Lean.Parser
 
+set_option compiler.ignoreBorrowAnnotation true in
 @[export lean_pretty_printer_formatter_interpret_parser_descr]
 unsafe def interpretParserDescr : ParserDescr → CoreM Formatter
   | ParserDescr.const n                             => getConstAlias formatterAliasesRef n

stage0/src/stdlib_flags.h

@@ -11,7 +11,7 @@ options get_default_options() {
     opts = opts.update({"debug", "terminalTacticsAsSorry"}, false);
     // switch to `true` for ABI-breaking changes affecting meta code;
     // see also next option!
-    opts = opts.update({"interpreter", "prefer_native"}, false);
+    opts = opts.update({"interpreter", "prefer_native"}, true);
     // switch to `false` when enabling `prefer_native` should also affect use
     // of built-in parsers in quotations; this is usually the case, but setting
     // both to `true` may be necessary for handling non-builtin parsers with

tests/elab/Reparen.lean.out.expected

@@ -4028,7 +4028,7 @@ Actions in the resulting monad are functions that take the local value as a para
 ordinary actions in `m`.
 -/
 def ReaderT (ρ : Type u) (m : Type u → Type v) (α : Type u) : Type max u v :=
-  ρ → m α
+  (a : @&ρ) → m α
 
 /--
 Interpret `ρ → m α` as an element of `ReaderT ρ m α`.