diff --git a/src/Lean/Compiler/IR/Checker.lean b/src/Lean/Compiler/IR/Checker.lean
index 8b81030f95..684890d19a 100644
--- a/src/Lean/Compiler/IR/Checker.lean
+++ b/src/Lean/Compiler/IR/Checker.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,10 +7,7 @@ Authors: Leonardo de Moura
 import Lean.Compiler.IR.CompilerM
 import Lean.Compiler.IR.Format
 
-namespace Lean
-namespace IR
-
-namespace Checker
+namespace Lean.IR.Checker
 
 structure CheckerContext :=
 (env : Environment) (localCtx : LocalContext := {}) (decls : Array Decl)
@@ -20,9 +18,10 @@ structure CheckerState :=
 abbrev M := ReaderT CheckerContext (ExceptT String (StateT CheckerState Id))
 
 def markIndex (i : Index) : M Unit := do
-s ← get;
-when (s.foundVars.contains i) $ throw ("variable / joinpoint index " ++ toString i ++ " has already been used");
-modify $ fun s => { s with foundVars := s.foundVars.insert i }
+let s ← get
+if s.foundVars.contains i then
+  throw s!"variable / joinpoint index {i} has already been used"
+modify fun s => { s with foundVars := s.foundVars.insert i }
 
 def markVar (x : VarId) : M Unit :=
 markIndex x.idx
@@ -31,18 +30,20 @@ def markJP (j : JoinPointId) : M Unit :=
 markIndex j.idx
 
 def getDecl (c : Name) : M Decl := do
-ctx ← read;
+let ctx ← read
 match findEnvDecl' ctx.env c ctx.decls with
-| none   => throw ("unknown declaration '" ++ toString c ++ "'")
+| none   => throw s!"unknown declaration '{c}'"
 | some d => pure d
 
 def checkVar (x : VarId) : M Unit := do
-ctx ← read;
-unless (ctx.localCtx.isLocalVar x.idx || ctx.localCtx.isParam x.idx) $ throw ("unknown variable '" ++ toString x ++ "'")
+let ctx ← read
+unless ctx.localCtx.isLocalVar x.idx || ctx.localCtx.isParam x.idx do
+ throw s!"unknown variable '{x}'"
 
 def checkJP (j : JoinPointId) : M Unit := do
-ctx ← read;
-unless (ctx.localCtx.isJP j.idx) $ throw ("unknown join point '" ++ toString j ++ "'")
+let ctx ← read
+unless ctx.localCtx.isJP j.idx do
+ throw s!"unknown join point '{j}'"
 
 def checkArg (a : Arg) : M Unit :=
 match a with
@@ -52,24 +53,26 @@ match a with
 def checkArgs (as : Array Arg) : M Unit :=
 as.forM checkArg
 
-@[inline] def checkEqTypes (ty₁ ty₂ : IRType) : M Unit :=
-unless (ty₁ == ty₂) $ throw ("unexpected type")
+@[inline] def checkEqTypes (ty₁ ty₂ : IRType) : M Unit := do
+unless ty₁ == ty₂ do
+  throw "unexpected type"
 
-@[inline] def checkType (ty : IRType) (p : IRType → Bool) : M Unit :=
-unless (p ty) $ throw ("unexpected type '" ++ toString ty ++ "'")
+@[inline] def checkType (ty : IRType) (p : IRType → Bool) : M Unit := do
+unless p ty do
+ throw s!"unexpected type '{ty}'"
 
 def checkObjType (ty : IRType) : M Unit := checkType ty IRType.isObj
 
 def checkScalarType (ty : IRType) : M Unit := checkType ty IRType.isScalar
 
 def getType (x : VarId) : M IRType := do
-ctx ← read;
+let ctx ← read
 match ctx.localCtx.getType x with
 | some ty => pure ty
-| none    => throw ("unknown variable '" ++ toString x ++ "'")
+| none    => throw s!"unknown variable '{x}'"
 
 @[inline] def checkVarType (x : VarId) (p : IRType → Bool) : M Unit := do
-ty ← getType x; checkType ty p
+let ty ← getType x; checkType ty p
 
 def checkObjVar (x : VarId) : M Unit :=
 checkVarType x IRType.isObj
@@ -78,17 +81,17 @@ def checkScalarVar (x : VarId) : M Unit :=
 checkVarType x IRType.isScalar
 
 def checkFullApp (c : FunId) (ys : Array Arg) : M Unit := do
-when (c == `hugeFuel) $
-  throw ("the auxiliary constant `hugeFuel` cannot be used in code, it is used internally for compiling `partial` definitions");
-decl ← getDecl c;
-unless (ys.size == decl.params.size) $
-  throw ("incorrect number of arguments to '" ++ toString c ++ "', " ++ toString ys.size ++ " provided, " ++ toString decl.params.size ++ " expected");
+if c == `hugeFuel then
+  throw "the auxiliary constant `hugeFuel` cannot be used in code, it is used internally for compiling `partial` definitions"
+let decl ← getDecl c
+unless ys.size == decl.params.size do
+  throw s!"incorrect number of arguments to '{c}', {ys.size} provided, {decl.params.size} expected"
 checkArgs ys
 
 def checkPartialApp (c : FunId) (ys : Array Arg) : M Unit := do
-decl ← getDecl c;
-unless (ys.size < decl.params.size) $
-  throw ("too many arguments too partial application '" ++ toString c ++ "', num. args: " ++ toString ys.size ++ ", arity: " ++ toString decl.params.size);
+let decl ← getDecl c
+unless ys.size < decl.params.size do
+  throw s!"too many arguments too partial application '{c}', num. args: {ys.size}, arity: {decl.params.size}"
 checkArgs ys
 
 def checkExpr (ty : IRType) : Expr → M Unit
@@ -100,13 +103,14 @@ def checkExpr (ty : IRType) : Expr → M Unit
 | Expr.reuse x i u ys     => checkObjVar x *> checkArgs ys *> checkObjType ty
 | Expr.box xty x          => checkObjType ty *> checkScalarVar x *> checkVarType x (fun t => t == xty)
 | Expr.unbox x            => checkScalarType ty *> checkObjVar x
-| Expr.proj i x           => do xType ← getType x;
+| Expr.proj i x           => do
+  let xType ← getType x;
   match xType with
   | IRType.object       => checkObjType ty
   | IRType.tobject      => checkObjType ty
   | IRType.struct _ tys => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
   | IRType.union _ tys  => if h : i < tys.size then checkEqTypes (tys.get ⟨i,h⟩) ty else throw "invalid proj index"
-  | other               => throw ("unexpected IR type '" ++ toString xType ++ "'")
+  | other               => throw s!"unexpected IR type '{xType}'"
 | Expr.uproj _ x          => checkObjVar x *> checkType ty (fun t => t == IRType.usize)
 | Expr.sproj _ _ x        => checkObjVar x *> checkScalarType ty
 | Expr.isShared x         => checkObjVar x *> checkType ty (fun t => t == IRType.uint8)
@@ -115,22 +119,22 @@ def checkExpr (ty : IRType) : Expr → M Unit
 | Expr.lit _              => pure ()
 
 @[inline] def withParams (ps : Array Param) (k : M Unit) : M Unit := do
-ctx ← read;
-localCtx ← ps.foldlM (fun (ctx : LocalContext) p => do
-   markVar p.x;
-   pure $ ctx.addParam p) ctx.localCtx;
+let ctx ← read
+let localCtx ← ps.foldlM (init := ctx.localCtx) fun (ctx : LocalContext) p => do
+   markVar p.x
+   pure $ ctx.addParam p
 withReader (fun _ => { ctx with localCtx := localCtx }) k
 
 partial def checkFnBody : FnBody → M Unit
 | FnBody.vdecl x t v b    => do
   checkExpr t v;
   markVar x;
-  ctx ← read;
+  let ctx ← read
   withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addLocal x t v }) (checkFnBody b)
 | FnBody.jdecl j ys v b => do
   markJP j;
   withParams ys (checkFnBody v);
-  ctx ← read;
+  let ctx ← read
   withReader (fun ctx => { ctx with localCtx := ctx.localCtx.addJP j ys v }) (checkFnBody b)
 | FnBody.set x _ y b      => checkVar x *> checkArg y *> checkFnBody b
 | FnBody.uset x _ y b     => checkVar x *> checkVar y *> checkFnBody b
@@ -152,9 +156,9 @@ def checkDecl : Decl → M Unit
 end Checker
 
 def checkDecl (decls : Array Decl) (decl : Decl) : CompilerM Unit := do
-env ← getEnv;
+let env ← getEnv
 match (Checker.checkDecl decl { env := env, decls := decls }).run' {} with
-| Except.error msg => throw ("IR check failed at '" ++ toString decl.name ++ "', error: " ++ msg)
+| Except.error msg => throw s!"IR check failed at '{decl.name}', error: {msg}"
 | other            => pure ()
 
 def checkDecls (decls : Array Decl) : CompilerM Unit :=