chore: fix bad (<- ...) occurrences

Remark: some of them were harmless since they were accessing some
read-only state.

src/Lean/Compiler/IR/EmitLLVM.lean

@@ -147,7 +147,7 @@ def callLeanRefcountFn (builder : LLVM.Builder llvmctx)
     (delta : Option (LLVM.Value llvmctx) := Option.none) : M llvmctx Unit := do
   let fnName :=  s!"lean_{kind}{if checkRef? then "" else "_ref"}{if delta.isNone then "" else "_n"}"
   let retty ← LLVM.voidType llvmctx
-  let argtys := if delta.isNone then #[← LLVM.voidPtrType llvmctx] else #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
+  let argtys ← if delta.isNone then pure #[← LLVM.voidPtrType llvmctx] else pure #[← LLVM.voidPtrType llvmctx, ← LLVM.size_tType llvmctx]
   let fn ← getOrCreateFunctionPrototype (← getLLVMModule) retty fnName argtys
   let fnty ← LLVM.functionType retty argtys
   match delta with

src/Lean/Compiler/LCNF/LambdaLifting.lean

@@ -88,7 +88,7 @@ occurring in `decl`.
 -/
 def mkAuxDecl (closure : Array Param) (decl : FunDecl) : LiftM LetDecl := do
   let nameNew ← mkAuxDeclName
-  let inlineAttr? := if (← read).inheritInlineAttrs then (← read).mainDecl.inlineAttr? else none
+  let inlineAttr? ← if (← read).inheritInlineAttrs then pure (← read).mainDecl.inlineAttr? else pure none
   let auxDecl ← go nameNew (← read).mainDecl.safe inlineAttr? |>.run' {}
   let us := auxDecl.levelParams.map mkLevelParam
   let auxDeclName ← match (← cacheAuxDecl auxDecl) with

src/Lean/Elab/BuiltinTerm.lean

@@ -232,7 +232,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 
 @[builtin_term_elab Parser.Term.withDeclName] def elabWithDeclName : TermElab := fun stx expectedType? => do
   let id := stx[2].getId
-  let id := if stx[1].isNone then id else (← getCurrNamespace) ++ id
+  let id ← if stx[1].isNone then pure id else pure <| (← getCurrNamespace) ++ id
   let e := stx[3]
   withMacroExpansion stx e <| withDeclName id <| elabTerm e expectedType?
 

src/Lean/Elab/Deriving/DecEq.lean

@@ -27,8 +27,9 @@ where
       let rhs ← if isProof then
         `(have h : @$a = @$b := rfl; by subst h; exact $(← mkSameCtorRhs todo):term)
       else
+        let sameCtor ← mkSameCtorRhs todo
         `(if h : @$a = @$b then
-           by subst h; exact $(← mkSameCtorRhs todo):term
+           by subst h; exact $sameCtor:term
           else
            isFalse (by intro n; injection n; apply h _; assumption))
       if let some auxFunName := recField then

src/Lean/Elab/Do.lean

@@ -63,8 +63,9 @@ private def letDeclHasBinders (letDecl : Syntax) : Bool :=
 /-- Return true if we should generate an error message when lifting a method over this kind of syntax. -/
 private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   let k := stx.getKind
+  -- TODO: make this extensible in the future.
   if k == ``Parser.Term.fun || k == ``Parser.Term.matchAlts ||
-     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec  then
+     k == ``Parser.Term.doLetRec || k == ``Parser.Term.letrec then
      -- It is never ok to lift over this kind of binder
     true
   -- The following kinds of `let`-expressions require extra checks to decide whether they contain binders or not
@@ -77,12 +78,15 @@ private def liftMethodForbiddenBinder (stx : Syntax) : Bool :=
   else
     false
 
+-- TODO: we must track whether we are inside a quotation or not.
 private partial def hasLiftMethod : Syntax → Bool
   | Syntax.node _ k args =>
     if liftMethodDelimiter k then false
     -- NOTE: We don't check for lifts in quotations here, which doesn't break anything but merely makes this rare case a
     -- bit slower
     else if k == ``Parser.Term.liftMethod then true
+    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
+    else if k == ``termDepIfThenElse || k == ``termIfThenElse then args.size >= 2 && hasLiftMethod args[1]!
     else args.any hasLiftMethod
   | _ => false
 
@@ -1321,6 +1325,12 @@ private partial def expandLiftMethodAux (inQuot : Bool) (inBinder : Bool) : Synt
       return .node i k (alts.map (·.1))
     else if liftMethodDelimiter k then
       return stx
+    -- For `pure` if-then-else, we only lift `(<- ...)` occurring in the condition.
+    else if args.size >= 2 && (k == ``termDepIfThenElse || k == ``termIfThenElse) then do
+      let inAntiquot := stx.isAntiquot && !stx.isEscapedAntiquot
+      let arg1 ← expandLiftMethodAux (inQuot && !inAntiquot || stx.isQuot) inBinder args[1]!
+      let args := args.set! 1 arg1
+      return Syntax.node i k args
     else if k == ``Parser.Term.liftMethod && !inQuot then withFreshMacroScope do
       if inBinder then
         throwErrorAt stx "cannot lift `(<- ...)` over a binder, this error usually happens when you are trying to lift a method nested in a `fun`, `let`, or `match`-alternative, and it can often be fixed by adding a missing `do`"

src/Lean/Elab/Structure.lean

@@ -704,6 +704,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
       if info.kind == StructFieldKind.fromParent then
         return none
       else
+        let env ← getEnv
         return some {
           fieldName  := info.name
           projFn     := info.declName
@@ -711,7 +712,7 @@ private def registerStructure (structName : Name) (infos : Array StructFieldInfo
           autoParam? := (← inferType info.fvar).getAutoParamTactic?
           subobject? :=
             if info.kind == StructFieldKind.subobject then
-              match (← getEnv).find? info.declName with
+              match env.find? info.declName with
               | some (ConstantInfo.defnInfo val) =>
                 match val.type.getForallBody.getAppFn with
                 | Expr.const parentName .. => some parentName

src/Lean/Elab/Tactic/Ext.lean

@@ -131,10 +131,10 @@ def withExtHyps (struct : Name) (flat : Term)
   withLocalDeclD `x (mkAppN structC params) fun x => do
   withLocalDeclD `y (mkAppN structC params) fun y => do
     let mut hyps := #[]
-    let fields := if flat then
-      getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
+    let fields ← if flat then
+      pure <| getStructureFieldsFlattened (← getEnv) struct (includeSubobjectFields := false)
     else
-      getStructureFields (← getEnv) struct
+      pure <| getStructureFields (← getEnv) struct
     for field in fields do
       let x_f ← mkProjection x field
       let y_f ← mkProjection y field

src/Lean/Meta/AbstractMVars.lean

@@ -101,7 +101,10 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
             let type   ← abstractExprMVars decl.type
             let fvarId ← mkFreshFVarId
             let fvar := mkFVar fvarId;
-            let userName := if decl.userName.isAnonymous then (`x).appendIndexAfter (← get).fvars.size else decl.userName
+            let userName ← if decl.userName.isAnonymous then
+              pure <| (`x).appendIndexAfter (← get).fvars.size
+            else
+              pure decl.userName
             modify fun s => {
               s with
               emap  := s.emap.insert mvarId fvar,

src/Lean/Meta/Match/MatcherApp/Transform.lean

@@ -24,8 +24,10 @@ private partial def updateAlts (unrefinedArgType : Expr) (typeNew : Expr) (altNu
         let alt ← try instantiateLambda alt xs catch _ => throwError "unexpected matcher application, insufficient number of parameters in alternative"
         forallBoundedTelescope d (some 1) fun x _ => do
           let alt ← mkLambdaFVars x alt -- x is the new argument we are adding to the alternative
-          let refined := if refined then refined else
-            !(← isDefEq unrefinedArgType (← inferType x[0]!))
+          let refined ← if refined then
+            pure refined
+          else
+            pure <| !(← isDefEq unrefinedArgType (← inferType x[0]!))
           return (← mkLambdaFVars xs alt, refined)
       updateAlts unrefinedArgType (b.instantiate1 alt) (altNumParams.set! i (numParams+1)) (alts.set ⟨i, h⟩ alt) refined (i+1)
     | _ => throwError "unexpected type at MatcherApp.addArg"

src/Lean/Meta/Tactic/Rewrites.lean

@@ -329,11 +329,11 @@ def findRewrites (hyps : Array (Expr × Bool × Nat))
     (leavePercentHeartbeats : Nat := 10) : MetaM (List RewriteResult) := do
   let mctx ← getMCtx
   let candidates ← rewriteCandidates hyps moduleRef target forbidden
-  let minHeartbeats : Nat :=
+  let minHeartbeats : Nat ←
         if (← getMaxHeartbeats) = 0 then
-          0
+          pure 0
         else
-          leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
+          pure <| leavePercentHeartbeats * (← getRemainingHeartbeats) / 100
   let cfg : RewriteResultConfig :=
         { stopAtRfl, minHeartbeats, max, mctx, goal, target, side }
   return (← takeListAux cfg {} (Array.mkEmpty max) candidates.toList).toList

tests/lean/run/3713.lean

@@ -0,0 +1,35 @@
+import Lean
+open Lean  Elab Meta
+
+def somethingBad : MetaM Nat := do
+  IO.println "oh no"
+  return 1
+
+/--
+error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
+---
+info:
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  let t := if false then ← somethingBad else 9
+
+def foo : MetaM Bool :=
+  return false
+
+/--
+error: invalid use of `(<- ...)`, must be nested inside a 'do' expression
+---
+info:
+-/
+#guard_msgs in
+#eval show MetaM Unit from do
+  let t := if (← foo) then ← somethingBad else 9
+
+/--
+info: 1
+-/
+#guard_msgs in
+#eval show MetaM Nat from do
+  let t := if (← foo) then 0 else 1
+  return t