chore: make sure we don't lift methods over binders

src/Lean/CoreM.lean

@@ -74,7 +74,8 @@ instance : MonadResolveName CoreM where
   getOpenDecls := return (← read).openDecls
 
 @[inline] def liftIOCore (x : IO α) : CoreM α := do
-  IO.toEIO (fun (err : IO.Error) => Exception.error (← getRef) (toString err)) x
+  let ref ← getRef
+  IO.toEIO (fun (err : IO.Error) => Exception.error ref (toString err)) x
 
 instance : MonadLift IO CoreM where
   monadLift := liftIOCore

src/Lean/Elab/Command.lean

@@ -131,7 +131,8 @@ private def ioErrorToMessage (ctx : Context) (ref : Syntax) (err : IO.Error) : M
 @[inline] def liftEIO {α} (x : EIO Exception α) : CommandElabM α := liftM x
 
 @[inline] def liftIO {α} (x : IO α) : CommandElabM α := do
-  IO.toEIO (fun (ex : IO.Error) => Exception.error (← read).ref ex.toString) x
+  let ctx ← read
+  IO.toEIO (fun (ex : IO.Error) => Exception.error ctx.ref ex.toString) x
 
 instance : MonadLiftT IO CommandElabM where
   monadLift := liftIO

src/Lean/Elab/InfoTree.lean

@@ -255,10 +255,12 @@ def mkInfoNode (info : Info) : m Unit := do
     Prod.fst <$> MonadFinally.tryFinally' x fun a? => do
       match a? with
       | none   => modifyInfoTrees fun _ => treesSaved
-      | some a => modifyInfoTrees fun trees =>
-        match (← mkInfo a) with
-        | Sum.inl info  => treesSaved.push <| InfoTree.node info trees
-        | Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId
+      | some a =>
+        let info ← mkInfo a
+        modifyInfoTrees fun trees =>
+          match info with
+          | Sum.inl info  => treesSaved.push <| InfoTree.node info trees
+          | Sum.inr mvaId => treesSaved.push <| InfoTree.hole mvaId
   else
     x
 

src/Lean/Elab/Quotation.lean

@@ -114,7 +114,8 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
                 | none                 => Array.empty)
             | _ =>
               let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
-              `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
+              let tuple ← mkTuple ids
+              `(Array.map (fun $tuple => $(inner[0])) $arr)
           let arr ←
             if k == `sepBy then
               `(mkSepArray $arr (mkAtom $(getSepFromSplice arg)))

src/Lean/Elab/SetOption.lean

@@ -26,8 +26,9 @@ def elabSetOption (id : Syntax) (val : Syntax) : m Options := do
     throwError "unexpected set_option value {val}"
 where
   setOption (optionName : Name) (val : DataValue) : m Options := do
-    let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error (← getRef) ex.toString) (getOptionDecl optionName)
+    let ref ← getRef
+    let decl ← IO.toEIO (fun (ex : IO.Error) => Exception.error ref ex.toString) (getOptionDecl optionName)
     unless decl.defValue.sameCtor val do throwError "type mismatch at set_option"
     return (← getOptions).insert optionName val
 
-end Lean.Elab
+end Lean.Elab

src/Lean/Elab/Syntax.lean

@@ -113,8 +113,9 @@ where
       let candidates ← resolveGlobalConstWithInfos (← getRef) parserName
       /- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name,
          and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/
+      let env ← getEnv
       candidates.filterMap fun c =>
-         match (← getEnv).find? c with
+         match env.find? c with
          | none      => none
          | some info =>
            match info.type with

src/Lean/Elab/Tactic/Induction.lean

@@ -128,7 +128,8 @@ partial def mkElimApp (elimName : Name) (elimInfo : ElimInfo) (targets : Array E
           addNewArg arg
         | _ =>
           let arg ← mkFreshExprSyntheticOpaqueMVar (← getArgExpectedType) (tag := appendTag tag binderName)
-          modify fun s => { s with alts := s.alts.push (← getBindingName, arg.mvarId!) }
+          let x   ← getBindingName
+          modify fun s => { s with alts := s.alts.push (x, arg.mvarId!) }
           addNewArg arg
       loop
     | _ =>

src/Lean/Elab/Term.lean

@@ -1392,7 +1392,8 @@ def resolveName (stx : Syntax) (n : Name) (preresolved : List (Name × List Stri
         throwError "invalid use of explicit universe parameters, '{e}' is a local"
       return [(e, projs)]
     -- check for section variable capture by a quotation
-    if let some (e, projs) := preresolved.findSome? fun (n, projs) => (← read).sectionFVars.find? n |>.map (·, projs) then
+    let ctx ← read
+    if let some (e, projs) := preresolved.findSome? fun (n, projs) => ctx.sectionFVars.find? n |>.map (·, projs) then
       return [(e, projs)]  -- section variables should shadow global decls
     if preresolved.isEmpty then
       process (← resolveGlobalName n)

src/Lean/Meta/LevelDefEq.lean

@@ -82,7 +82,9 @@ private def solveSelfMax (mvarId : MVarId) (v : Level) : MetaM Unit := do
   assignLevelMVar mvarId <| mkMaxArgsDiff mvarId v n
 
 private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
-  modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := (← getRef), ctx? := (← read).defEqCtx? }
+  let ref ← getRef
+  let ctx ← read
+  modifyPostponed fun postponed => postponed.push { lhs := lhs, rhs := rhs, ref := ref, ctx? := ctx.defEqCtx? }
 
 mutual
 

src/Lean/Meta/SizeOf.lean

@@ -79,7 +79,7 @@ private partial def mkSizeOfMinors {α} (motiveFVars : Array Expr) (minorFVars :
 where
   loop (i : Nat) (minors : Array Expr) : MetaM α := do
     if i < minorFVars.size then
-      forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ =>
+      forallTelescopeReducing (← inferType minorFVars[i]) fun xs _ => do
       forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do
         let mut minor ← mkNumeral (mkConst ``Nat) 1
         for x in xs, x' in xs' do