diff --git a/src/Init/Control/Applicative.lean b/src/Init/Control/Applicative.lean
index 2de9cd3cdf..8e80b9c5c9 100644
--- a/src/Init/Control/Applicative.lean
+++ b/src/Init/Control/Applicative.lean
@@ -19,19 +19,19 @@ class HasSeq (f : Type u → Type v) : Type (max (u+1) v) :=
 infixl <*> := HasSeq.seq
 
 class HasSeqLeft (f : Type u → Type v) : Type (max (u+1) v) :=
-(seqLeft : ∀ {α β : Type u}, f α → f β → f α)
+(seqLeft : ∀ {α : Type u}, f α → f PUnit → f α)
 
 infixl <* := HasSeqLeft.seqLeft
 
 class HasSeqRight (f : Type u → Type v) : Type (max (u+1) v) :=
-(seqRight : ∀ {α β : Type u}, f α → f β → f β)
+(seqRight : ∀ {β : Type u}, f PUnit → f β → f β)
 
 infixr *> := HasSeqRight.seqRight
 
 class Applicative (f : Type u → Type v) extends Functor f, HasPure f, HasSeq f, HasSeqLeft f, HasSeqRight f :=
 (map      := fun _ _ x y => pure x <*> y)
-(seqLeft  := fun α β a b => const β <$> a <*> b)
-(seqRight := fun α β a b => const α id <$> a <*> b)
+(seqLeft  := fun α a b => const _ <$> a <*> b)
+(seqRight := fun β a b => const _ id <$> a <*> b)
 
 @[macroInline]
 def when {m : Type → Type u} [Applicative m] (c : Prop) [h : Decidable c] (t : m Unit) : m Unit :=
diff --git a/src/Init/Control/EState.lean b/src/Init/Control/EState.lean
index a732269f38..bab6287d07 100644
--- a/src/Init/Control/EState.lean
+++ b/src/Init/Control/EState.lean
@@ -102,7 +102,7 @@ fun s => match x s with
   | Result.ok a s    => Result.ok (f a) s
   | Result.error e s => Result.error e s
 
-@[inline] protected def seqRight (x : EStateM ε σ α) (y : EStateM ε σ β) : EStateM ε σ β :=
+@[inline] protected def seqRight (x : EStateM ε σ PUnit) (y : EStateM ε σ β) : EStateM ε σ β :=
 fun s => match x s with
   | Result.ok _ s    => y s
   | Result.error e s => Result.error e s
diff --git a/src/Init/Control/Except.lean b/src/Init/Control/Except.lean
index 2432a60c61..8cd89a207e 100644
--- a/src/Init/Control/Except.lean
+++ b/src/Init/Control/Except.lean
@@ -181,7 +181,7 @@ instance (ε m out) [MonadRun out m] : MonadRun (fun α => out (Except ε α)) (
 ⟨fun α => run⟩
 
 /-- Execute `x` and then execute `finalizer` even if `x` threw an exception -/
-@[inline] def finally {ε α β : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m β) : m α :=
+@[inline] def finally {ε α : Type u} {m : Type u → Type v} [Monad m] [MonadExcept ε m] (x : m α) (finalizer : m PUnit) : m α :=
 catch
   (do a ← x; finalizer; pure a)
   (fun e => do finalizer; throw e)
diff --git a/src/Init/Control/Functor.lean b/src/Init/Control/Functor.lean
index 46235c3bcf..af4a5259bc 100644
--- a/src/Init/Control/Functor.lean
+++ b/src/Init/Control/Functor.lean
@@ -22,3 +22,8 @@ infixr `$>`  := Functor.mapConstRev
 @[reducible] def Functor.mapRev {f : Type u → Type v} [Functor f] {α β : Type u} : f α → (α → β) → f β :=
 fun a f => f <$> a
 infixl `<&>` := Functor.mapRev
+
+def Functor.discard {f : Type u → Type v} {α : Type u} [Functor f] (x : f α) : f PUnit :=
+PUnit.unit <$ x
+
+export Functor (discard)
diff --git a/src/Init/Control/Monad.lean b/src/Init/Control/Monad.lean
index c67566b965..d62b3f9163 100644
--- a/src/Init/Control/Monad.lean
+++ b/src/Init/Control/Monad.lean
@@ -25,8 +25,8 @@ infixr `>=>` := mcomp
 class Monad (m : Type u → Type v) extends Applicative m, HasBind m : Type (max (u+1) v) :=
 (map      := fun α β f x => x >>= pure ∘ f)
 (seq      := fun α β f x => f >>= (fun y => y <$> x))
-(seqLeft  := fun α β x y => x >>= fun a => y >>= fun _ => pure a)
-(seqRight := fun α β x y => x >>= fun _ => y)
+(seqLeft  := fun α x y => x >>= fun a => y >>= fun _ => pure a)
+(seqRight := fun β x y => x >>= fun _ => y)
 
 instance monadInhabited' {α : Type u} {m : Type u → Type v} [Monad m] : Inhabited (α → m α) :=
 ⟨pure⟩
diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 875106bbdc..9cae7da327 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -504,7 +504,7 @@ variables {m : Type v → Type w} [Monad m]
 variable {β : Type v}
 
 @[specialize]
-partial def forMAux (f : α → m β) (a : Array α) : Nat → m PUnit
+partial def forMAux (f : α → m PUnit) (a : Array α) : Nat → m PUnit
 | i =>
   if h : i < a.size then
      let idx : Fin a.size := ⟨i, h⟩;
@@ -513,11 +513,11 @@ partial def forMAux (f : α → m β) (a : Array α) : Nat → m PUnit
   else
      pure ⟨⟩
 
-@[inline] def forM (f : α → m β) (a : Array α) : m PUnit :=
+@[inline] def forM (f : α → m PUnit) (a : Array α) : m PUnit :=
 a.forMAux f 0
 
 @[specialize]
-partial def forRevMAux (f : α → m β) (a : Array α) : forall (i : Nat), i ≤ a.size → m PUnit
+partial def forRevMAux (f : α → m PUnit) (a : Array α) : forall (i : Nat), i ≤ a.size → m PUnit
 | i, h =>
   if hLt : 0 < i then
     have i - 1 < i from Nat.subLt hLt (Nat.zeroLtSucc 0);
@@ -528,7 +528,7 @@ partial def forRevMAux (f : α → m β) (a : Array α) : forall (i : Nat), i 
   else
      pure ⟨⟩
 
-@[inline] def forRevM (f : α → m β) (a : Array α) : m PUnit :=
+@[inline] def forRevM (f : α → m PUnit) (a : Array α) : m PUnit :=
 a.forRevMAux f a.size (Nat.leRefl _)
 
 end
diff --git a/src/Init/Data/List/Control.lean b/src/Init/Data/List/Control.lean
index 78a499d9b7..f8d5937686 100644
--- a/src/Init/Data/List/Control.lean
+++ b/src/Init/Data/List/Control.lean
@@ -62,22 +62,22 @@ def mapA₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type
 | _,     _     => pure []
 
 @[specialize]
-def forM {m : Type u → Type v} [Monad m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+def forM {m : Type u → Type v} [Monad m] {α : Type w} (f : α → m PUnit) : List α → m PUnit
 | []     => pure ⟨⟩
 | h :: t => do f h; forM t
 
 @[specialize]
-def forM₂ {m : Type u → Type v} [Monad m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
+def forM₂ {m : Type u → Type v} [Monad m] {α : Type u₁} {β : Type u₂} (f : α → β → m PUnit) : List α → List β → m PUnit
 | a::as, b::bs => do f a b; forM₂ as bs
 | _,     _     => pure ⟨⟩
 
 @[specialize]
-def forA {m : Type u → Type v} [Applicative m] {α : Type w} {β : Type u} (f : α → m β) : List α → m PUnit
+def forA {m : Type u → Type v} [Applicative m] {α : Type w} (f : α → m PUnit) : List α → m PUnit
 | []     => pure ⟨⟩
 | h :: t => f h *> forA t
 
 @[specialize]
-def forA₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} {γ : Type u} (f : α → β → m γ) : List α → List β → m PUnit
+def forA₂ {m : Type u → Type v} [Applicative m] {α : Type u₁} {β : Type u₂} (f : α → β → m PUnit) : List α → List β → m PUnit
 | a::as, b::bs => f a b *> forA₂ as bs
 | _,     _     => pure ⟨⟩
 
diff --git a/src/Init/Data/PersistentArray/Basic.lean b/src/Init/Data/PersistentArray/Basic.lean
index 6f0f3e0297..0b42406758 100644
--- a/src/Init/Data/PersistentArray/Basic.lean
+++ b/src/Init/Data/PersistentArray/Basic.lean
@@ -231,11 +231,11 @@ else do
   b ← foldlFromMAux f t.root (USize.ofNat ini) t.shift b;
   t.tail.foldlM f b
 
-@[specialize] partial def forMAux (f : α → m β) : PersistentArrayNode α → m PUnit
+@[specialize] partial def forMAux (f : α → m PUnit) : PersistentArrayNode α → m PUnit
 | node cs => cs.forM (fun c => forMAux c)
 | leaf vs => vs.forM f
 
-@[specialize] def forM (t : PersistentArray α) (f : α → m β) : m PUnit :=
+@[specialize] def forM (t : PersistentArray α) (f : α → m PUnit) : m PUnit :=
 forMAux f t.root *> t.tail.forM f
 
 end
diff --git a/src/Init/Data/RBMap/Basic.lean b/src/Init/Data/RBMap/Basic.lean
index 1acdfa1aab..ac3d99dda8 100644
--- a/src/Init/Data/RBMap/Basic.lean
+++ b/src/Init/Data/RBMap/Basic.lean
@@ -236,8 +236,8 @@ t.val.depth f
 @[inline] def mfold {m : Type w → Type w'} [Monad m] (f : σ → α → β → m σ) : σ → RBMap α β lt → m σ
 | b, ⟨t, _⟩ => t.mfold f b
 
-@[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m σ) (t : RBMap α β lt) : m PUnit :=
-t.mfold (fun _ k v =>  f k v *> pure ⟨⟩) ⟨⟩
+@[inline] def mfor {m : Type w → Type w'} [Monad m] (f : α → β → m PUnit) (t : RBMap α β lt) : m PUnit :=
+t.mfold (fun _ k v => f k v) ⟨⟩
 
 @[inline] def isEmpty : RBMap α β lt → Bool
 | ⟨leaf, _⟩ => true
diff --git a/src/Init/Data/RBTree/Basic.lean b/src/Init/Data/RBTree/Basic.lean
index 2a0513c97c..153ea1b4c4 100644
--- a/src/Init/Data/RBTree/Basic.lean
+++ b/src/Init/Data/RBTree/Basic.lean
@@ -34,8 +34,8 @@ RBMap.revFold (fun r a _ => f r a) b t
 @[inline] def mfold {m : Type v → Type w} [Monad m] (f : β → α → m β) (b : β) (t : RBTree α lt) : m β :=
 RBMap.mfold (fun r a _ => f r a) b t
 
-@[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m β) (t : RBTree α lt) : m PUnit :=
-t.mfold (fun _ a => f a *> pure ⟨⟩) ⟨⟩
+@[inline] def mfor {m : Type v → Type w} [Monad m] (f : α → m PUnit) (t : RBTree α lt) : m PUnit :=
+t.mfold (fun _ a => f a) ⟨⟩
 
 @[inline] def isEmpty (t : RBTree α lt) : Bool :=
 RBMap.isEmpty t
diff --git a/src/Init/Lean/Compiler/IR/EmitC.lean b/src/Init/Lean/Compiler/IR/EmitC.lean
index 1523dd3012..f0219f9120 100644
--- a/src/Init/Lean/Compiler/IR/EmitC.lean
+++ b/src/Init/Lean/Compiler/IR/EmitC.lean
@@ -400,7 +400,7 @@ ys.toList.map argToCString
 def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M Unit := do
 emit f; emit "(";
 -- We must remove irrelevant arguments to extern calls.
-ys.size.foldM
+_ ← ys.size.foldM
   (fun i (first : Bool) =>
     if (ps.get! i).ty.isIrrelevant then
       pure first
diff --git a/src/Init/Lean/Delaborator.lean b/src/Init/Lean/Delaborator.lean
index 28ca37e83b..4b02a91874 100644
--- a/src/Init/Lean/Delaborator.lean
+++ b/src/Init/Lean/Delaborator.lean
@@ -435,14 +435,14 @@ Expr.const c@(Name.str _ f _) _ _ ← pure fn.getAppFn | failure;
 env ← liftM getEnv;
 some info ← pure $ env.getProjectionFnInfo c | failure;
 -- can't use with classes since the instance parameter is implicit
-assert (!info.fromClass);
+guard $ !info.fromClass;
 -- projection function should be fully applied (#struct params + 1 instance parameter)
 -- TODO: support over-application
-assert $ e.getAppNumArgs == info.nparams + 1;
+guard $ e.getAppNumArgs == info.nparams + 1;
 -- If pp.explicit is true, and the structure has parameters, we should not
 -- use field notation because we will not be able to see the parameters.
 expl ← getPPOption getPPExplicit;
-assert $ !expl || info.nparams == 0;
+guard $ !expl || info.nparams == 0;
 appStx ← withAppArg delab;
 `($(appStx).$(mkIdent f):ident)
 
@@ -450,7 +450,7 @@ appStx ← withAppArg delab;
 @[builtinDelab app.coe]
 def delabCoe : Delab := whenPPOption getPPCoercions $ do
 e ← getExpr;
-assert $ e.getAppNumArgs >= 4;
+guard $ e.getAppNumArgs >= 4;
 -- delab as application, then discard function
 stx ← delabAppImplicit;
 match_syntax stx with
diff --git a/src/Init/Lean/Elab/App.lean b/src/Init/Lean/Elab/App.lean
index 4d744ff684..c224837449 100644
--- a/src/Init/Lean/Elab/App.lean
+++ b/src/Init/Lean/Elab/App.lean
@@ -180,7 +180,7 @@ unless (ctx.explicit || ctx.foundExplicit || ctx.typeMVars.isEmpty)  $ do
     | some eTypeBody =>
       unless eTypeBody.hasLooseBVars $
       when (hasTypeMVar ctx eTypeBody && hasOnlyTypeMVar ctx eTypeBody) $ do
-        isDefEq ctx.ref expectedType eTypeBody;
+        _ ← isDefEq ctx.ref expectedType eTypeBody;
         pure ()
 
 private def nextArgIsHole (ctx : ElabAppArgsCtx) : Bool :=
@@ -201,7 +201,7 @@ private partial def elabAppArgsAux : ElabAppArgsCtx → Expr → Expr → TermEl
     | none              => pure ()
     | some expectedType => do {
       -- Try to propagate expected type. Ignore if types are not definitionally equal, caller must handle it.
-      isDefEq ctx.ref expectedType eType;
+      _ ← isDefEq ctx.ref expectedType eType;
       pure ()
     };
     synthesizeAppInstMVars ctx.ref ctx.instMVars;
diff --git a/src/Init/Lean/Elab/Binders.lean b/src/Init/Lean/Elab/Binders.lean
index dbc4cf528f..8231a0b21d 100644
--- a/src/Init/Lean/Elab/Binders.lean
+++ b/src/Init/Lean/Elab/Binders.lean
@@ -305,7 +305,7 @@ match s.expectedType? with
   expectedType ← whnfForall ref expectedType;
   match expectedType with
   | Expr.forallE _ d b _ => do
-    isDefEq ref fvarType d;
+    _ ← isDefEq ref fvarType d;
     checkNoOptAutoParam ref fvarType;
     let b := b.instantiate1 fvar;
     pure { expectedType? := some b, .. s }
diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index baccd8be40..2f784b319e 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -509,7 +509,7 @@ fun stx => do
 def hasNoErrorMessages : CommandElabM Bool := do
 s ← get; pure $ !s.messages.hasErrors
 
-def failIfSucceeds {α} (ref : Syntax) (x : CommandElabM α) : CommandElabM Unit := do
+def failIfSucceeds (ref : Syntax) (x : CommandElabM Unit) : CommandElabM Unit := do
 let resetMessages : CommandElabM MessageLog := do {
   s ← get;
   let messages := s.messages;
diff --git a/src/Init/Lean/Elab/StructInst.lean b/src/Init/Lean/Elab/StructInst.lean
index 0240c5f6cd..2aed9e89a7 100644
--- a/src/Init/Lean/Elab/StructInst.lean
+++ b/src/Init/Lean/Elab/StructInst.lean
@@ -521,7 +521,7 @@ match expectedType? with
     | none           => pure ()
     | some typeBody =>
       unless typeBody.hasLooseBVars $ do
-        isDefEq ref expectedType typeBody;
+        _ ← isDefEq ref expectedType typeBody;
         pure ()
 
 private def mkCtorHeader (ref : Syntax) (ctorVal : ConstructorVal) (expectedType? : Option Expr) : TermElabM CtorHeaderResult := do
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 921896caab..5473ea7767 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -1166,7 +1166,7 @@ fun stx expectedType? => do
   typeMVar ← mkFreshTypeMVar ref MetavarKind.synthetic;
   registerSyntheticMVar ref typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat));
   match expectedType? with
-  | some expectedType => do isDefEq ref expectedType typeMVar; pure ()
+  | some expectedType => do _ ← isDefEq ref expectedType typeMVar; pure ()
   | _                 => pure ();
   u ← getLevel ref typeMVar;
   u ← decLevel ref u;
diff --git a/src/Init/Lean/LocalContext.lean b/src/Init/Lean/LocalContext.lean
index 07010d2687..288d4bab32 100644
--- a/src/Init/Lean/LocalContext.lean
+++ b/src/Init/Lean/LocalContext.lean
@@ -222,10 +222,10 @@ lctx.decls.foldlM (fun b decl => match decl with
   | some decl => f b decl)
   b
 
-@[specialize] def forM (lctx : LocalContext) (f : LocalDecl → m β) : m PUnit :=
+@[specialize] def forM (lctx : LocalContext) (f : LocalDecl → m PUnit) : m PUnit :=
 lctx.decls.forM $ fun decl => match decl with
   | none      => pure PUnit.unit
-  | some decl => f decl *> pure PUnit.unit
+  | some decl => f decl
 
 @[specialize] def findDeclM? (lctx : LocalContext) (f : LocalDecl → m (Option β)) : m (Option β) :=
 lctx.decls.findSomeM? $ fun decl => match decl with
diff --git a/src/Init/Lean/Meta/Basic.lean b/src/Init/Lean/Meta/Basic.lean
index 96fa45cb92..61883e19f1 100644
--- a/src/Init/Lean/Meta/Basic.lean
+++ b/src/Init/Lean/Meta/Basic.lean
@@ -254,9 +254,9 @@ def throwBug {α} (b : Bug) : MetaM α :=
 throwEx $ Exception.bug b
 
 /-- Execute `x` only in debugging mode. -/
-@[inline] private def whenDebugging {α} (x : MetaM α) : MetaM Unit := do
+@[inline] private def whenDebugging (x : MetaM Unit) : MetaM Unit := do
 ctx ← read;
-when ctx.config.debug (do x; pure ())
+when ctx.config.debug x
 
 @[inline] def shouldReduceAll : MetaM Bool := do
 ctx ← read; pure $ ctx.config.transparency == TransparencyMode.all
diff --git a/src/Init/Lean/Meta/Check.lean b/src/Init/Lean/Meta/Check.lean
index be302c797b..b289c85e6a 100644
--- a/src/Init/Lean/Meta/Check.lean
+++ b/src/Init/Lean/Meta/Check.lean
@@ -15,7 +15,7 @@ namespace Lean
 namespace Meta
 
 private def ensureType (e : Expr) : MetaM Unit := do
-getLevel e; pure ()
+_ ← getLevel e; pure ()
 
 @[specialize] private def checkLambdaLet
     (check   : Expr → MetaM Unit)
diff --git a/src/Init/Lean/Meta/ExprDefEq.lean b/src/Init/Lean/Meta/ExprDefEq.lean
index 722717e067..3b150ea26c 100644
--- a/src/Init/Lean/Meta/ExprDefEq.lean
+++ b/src/Init/Lean/Meta/ExprDefEq.lean
@@ -165,8 +165,8 @@ if h : args₁.size = args₂.size then do
     let a₂   := args₂.get! i;
     let info := finfo.paramInfo.get! i;
     when info.instImplicit $ do {
-      trySynthPending a₁;
-      trySynthPending a₂;
+      _ ← trySynthPending a₁;
+      _ ← trySynthPending a₂;
       pure ()
     };
     withAtLeastTransparency TransparencyMode.default $ isExprDefEqAux a₁ a₂)
diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index c8d57d0e05..995cb7d194 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1842,7 +1842,7 @@ categoryParserFnRef.set categoryParserFnImpl
 def addToken (env : Environment) (tk : TokenConfig) : Except String Environment := do
 -- Recall that `ParserExtension.addEntry` is pure, and assumes `addTokenConfig` does not fail.
 -- So, we must run it here to handle exception.
-addTokenConfig (parserExtension.getState env).tokens tk;
+_ ← addTokenConfig (parserExtension.getState env).tokens tk;
 pure $ parserExtension.addEntry env $ ParserExtensionEntry.token tk
 
 def addSyntaxNodeKind (env : Environment) (k : SyntaxNodeKind) : Environment :=
diff --git a/src/Init/Lean/Util/Trace.lean b/src/Init/Lean/Util/Trace.lean
index 055d087fb6..79e4837011 100644
--- a/src/Init/Lean/Util/Trace.lean
+++ b/src/Init/Lean/Util/Trace.lean
@@ -58,7 +58,7 @@ whenM (isTracingEnabledFor cls) (do msg ← mkMsg; addTrace cls msg)
 
 @[inline] def traceCtx (cls : Name) (ctx : m α) : m α := do
 b ← isTracingEnabledFor cls;
-if !b then do old ← enableTracing false; a ← ctx; enableTracing old; pure a
+if !b then do old ← enableTracing false; a ← ctx; _ ← enableTracing old; pure a
 else do
   oldCurrTraces ← getResetTraces;
   a ← ctx;
@@ -78,8 +78,8 @@ b ← isTracingEnabledFor cls;
 if !b then do
   old ← enableTracing false;
   catch
-    (do a ← ctx; enableTracing old; pure a)
-    (fun e => do enableTracing old; throw e)
+    (do a ← ctx; _ ← enableTracing old; pure a)
+    (fun e => do _ ← enableTracing old; throw e)
 else do
   oldCurrTraces ← getResetTraces;
   catch
diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index c445ce6b70..2276557203 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -346,10 +346,7 @@ static expr parse_do(parser & p, bool has_braces) {
                                    pos);
             }
         } else {
-            r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(p), ps[i]),
-                                      es[i],
-                                      p.save_pos(mk_lambda("_x", mk_expr_placeholder(), r), p.pos_of(r))),
-                               ps[i]);
+            r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
         }
     }
     return r;
diff --git a/stage0/src/frontends/lean/builtin_exprs.cpp b/stage0/src/frontends/lean/builtin_exprs.cpp
index c445ce6b70..2276557203 100644
--- a/stage0/src/frontends/lean/builtin_exprs.cpp
+++ b/stage0/src/frontends/lean/builtin_exprs.cpp
@@ -346,10 +346,7 @@ static expr parse_do(parser & p, bool has_braces) {
                                    pos);
             }
         } else {
-            r = p.rec_save_pos(mk_app(p.save_pos(mk_bind_fn(p), ps[i]),
-                                      es[i],
-                                      p.save_pos(mk_lambda("_x", mk_expr_placeholder(), r), p.pos_of(r))),
-                               ps[i]);
+            r = p.rec_save_pos(mk_app(p.save_pos(mk_const({"HasSeqRight", "seqRight"}), ps[i]), es[i], r), ps[i]);
         }
     }
     return r;
diff --git a/tests/bench/binarytrees.lean b/tests/bench/binarytrees.lean
index a2a57c5c62..3f2c3a2d10 100644
--- a/tests/bench/binarytrees.lean
+++ b/tests/bench/binarytrees.lean
@@ -53,7 +53,7 @@ def main : List String → IO UInt32
 
   -- allocate, walk, and deallocate many bottom-up binary trees
   let vs := (depth minN maxN); -- `using` (parList $ evalTuple3 r0 r0 rseq)
-  vs.mapM (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
+  vs.forM (fun ⟨m,d,i⟩ => out (toString m ++ "\t trees") d i.get);
 
   -- confirm the the long-lived binary tree still exists
   out "long lived tree" maxN (check long);
diff --git a/tests/bench/deriv.lean b/tests/bench/deriv.lean
index b00c0d674f..50c00effe5 100644
--- a/tests/bench/deriv.lean
+++ b/tests/bench/deriv.lean
@@ -94,6 +94,6 @@ unsafe def main : List String → IO UInt32
   let n := s.toNat!;
   let x := Var "x";
   let f := pow x x;
-  nest deriv n f;
+  _ ← nest deriv n f;
   pure 0
 | _ => pure 1
diff --git a/tests/bench/parser.lean b/tests/bench/parser.lean
index 7770d57ddd..4438f31822 100644
--- a/tests/bench/parser.lean
+++ b/tests/bench/parser.lean
@@ -4,6 +4,6 @@ def main : List String → IO Unit
 | [fname, n] => do
   env ← Lean.mkEmptyEnvironment;
   n.toNat!.forM $ fun _ =>
-    Lean.Parser.parseFile env fname *> pure ();
+    discard $ Lean.Parser.parseFile env fname;
   pure ()
 | _    => throw $ IO.userError "give file"
diff --git a/tests/bench/unionfind.lean b/tests/bench/unionfind.lean
index 53edda5945..892e0090d6 100644
--- a/tests/bench/unionfind.lean
+++ b/tests/bench/unionfind.lean
@@ -80,7 +80,7 @@ do r₁ ← findEntry n₁;
 
 def mkNodes : Nat → M Unit
 | 0   => pure ()
-| n+1 => mk *> mkNodes n
+| n+1 => do _ ← mk; mkNodes n
 
 def checkEq (n₁ n₂ : Node) : M Unit :=
 do r₁ ← find n₁; r₂ ← find n₂;
diff --git a/tests/compiler/t2.lean b/tests/compiler/t2.lean
index d829922406..f40523bb45 100644
--- a/tests/compiler/t2.lean
+++ b/tests/compiler/t2.lean
@@ -92,7 +92,7 @@ do
 def main (xs : List String) : IO UInt32 :=
 do let x := Var "x";
    let f := pow x x;
-   nest deriv 7 f;
+   _ ← nest deriv 7 f;
    pure 0
 
 -- setOption profiler True
diff --git a/tests/compiler/t4.lean b/tests/compiler/t4.lean
index ef27a59492..1931e935ae 100644
--- a/tests/compiler/t4.lean
+++ b/tests/compiler/t4.lean
@@ -107,7 +107,7 @@ def main (xs : List String) : IO UInt32 :=
 do let x := Var "x";
    let f := add x (mul x (mul x (add x x)));
    IO.println f;
-   nest deriv 3 f;
+   _ ← nest deriv 3 f;
    pure 0
 
 -- setOption profiler True
diff --git a/tests/lean/file_not_found.lean b/tests/lean/file_not_found.lean
index 0ec53f2fe0..8002cc2ce2 100644
--- a/tests/lean/file_not_found.lean
+++ b/tests/lean/file_not_found.lean
@@ -3,13 +3,13 @@ import Init.System.IO
 
 open IO.FS
 
-#eval (IO.FS.Handle.mk "non-existent-file.txt" Mode.read *> pure () : IO Unit)
+#eval (discard $ IO.FS.Handle.mk "non-existent-file.txt" Mode.read : IO Unit)
 #eval do condM (IO.fileExists "readonly.txt")
                (pure ())
                (IO.FS.withFile "readonly.txt" Mode.write $ fun _ => pure ());
          IO.setAccessRights "readonly.txt" { user := { read := true } };
          (pure () : IO Unit)
-#eval (IO.FS.Handle.mk "readonly.txt" Mode.write *> pure () : IO Unit)
+#eval (discard $ IO.FS.Handle.mk "readonly.txt" Mode.write : IO Unit)
 #eval do h ← IO.FS.Handle.mk "readonly.txt" Mode.read;
          h.putStr "foo";
          IO.println "foo";
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index 4ea83e08b2..5110a54100 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -10,7 +10,7 @@ n.forM $ fun i => do
 def showArrayRef (r : IO.Ref (Array Nat)) : IO Unit :=
 do a ← r.swap ∅;
    a.size.forM (fun i => IO.println ("[" ++ toString i ++ "]: " ++ toString (a.get! i)));
-   r.swap a;
+   _ ← r.swap a;
    pure ()
 
 def tst (n : Nat) : IO Unit :=
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index f08cf55770..9e05a71a0d 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -92,5 +92,5 @@ do
 unsafe def main : IO Unit :=
 do let x := Var "x";
    let f := pow x x;
-   nest deriv 9 f;
+   _ ← nest deriv 9 f;
    pure ()
diff --git a/tests/lean/run/parseCore.lean b/tests/lean/run/parseCore.lean
index a2ce66ec30..a6953f6b2c 100644
--- a/tests/lean/run/parseCore.lean
+++ b/tests/lean/run/parseCore.lean
@@ -5,7 +5,7 @@ if System.Platform.isWindows then
   pure () -- TODO investigate why the following doesn't work on Windows
 else do
   env ← Lean.mkEmptyEnvironment;
-  Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
+  _ ← Lean.Parser.parseFile env (System.mkFilePath ["..", "..", "..", "src", "Init", "Core.lean"]);
   IO.println "done"
 
 #eval test