diff --git a/src/Lean/Data/RArray.lean b/src/Lean/Data/RArray.lean
index dee14797ca..adddb7b32e 100644
--- a/src/Lean/Data/RArray.lean
+++ b/src/Lean/Data/RArray.lean
@@ -6,6 +6,8 @@ Authors: Joachim Breitner
 
 prelude
 import Init.Data.RArray
+import Lean.Meta.InferType
+import Lean.Meta.DecLevel
 import Lean.ToExpr
 
 /-!
@@ -57,19 +59,22 @@ where
     case case1 => simp [ofFn.go, size]
     case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
-section Meta
-open Lean
-
-def RArray.toExpr (ty : Expr) (f : α → Expr) : RArray α → Expr
-  | .leaf x  =>
-    mkApp2 (mkConst ``RArray.leaf) ty (f x)
-  | .branch p l r =>
-    mkApp4 (mkConst ``RArray.branch) ty (mkRawNatLit p) (l.toExpr ty f) (r.toExpr ty f)
-
-instance [ToExpr α] : ToExpr (RArray α) where
-  toTypeExpr := mkApp (mkConst ``RArray) (toTypeExpr α)
-  toExpr a := a.toExpr (toTypeExpr α) toExpr
-
-end Meta
+open Meta
+def RArray.toExpr (ty : Expr) (f : α → Expr) (a : RArray α) : MetaM Expr := do
+  let k (leaf branch : Expr) : MetaM Expr :=
+    let rec go (a : RArray α) : MetaM Expr := do
+      match a with
+      | .leaf x  =>
+        return mkApp2 leaf ty (f x)
+      | .branch p l r =>
+        return mkApp4 branch ty (mkRawNatLit p) (← go l) (← go r)
+    go a
+  let info ← getConstInfo ``RArray
+  -- TODO: remove after bootstrapping hell
+  if info.levelParams.isEmpty then
+    k (mkConst ``RArray.leaf) (mkConst ``RArray.branch)
+  else
+    let u ← getDecLevel ty
+    k (mkConst ``RArray.leaf [u]) (mkConst ``RArray.branch [u])
 
 end Lean
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
index f221c90f9c..71e2ba8186 100644
--- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
+++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean
@@ -288,7 +288,7 @@ where
       let ras := Lean.RArray.ofArray as h
       let packedType := mkConst ``BVExpr.PackedBitVec
       let pack := fun (width, expr) => mkApp2 (mkConst ``BVExpr.PackedBitVec.mk) (toExpr width) expr
-      let newAtomsAssignment := ras.toExpr packedType pack
+      let newAtomsAssignment ← ras.toExpr packedType pack
       modify fun s => { s with atomsAssignmentCache := some newAtomsAssignment }
       return newAtomsAssignment
     else
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index b014d7b712..dcddcd5ff6 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -82,14 +82,14 @@ private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr)
       i := i - 1
     return e
 
-private def toContextExprCore (vars : PArray Expr) (type : Expr) : Expr :=
+private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
   if h : 0 < vars.size then
     RArray.toExpr type id (RArray.ofFn (vars[·]) h)
   else
     RArray.toExpr type id (RArray.leaf (mkIntLit 0))
 
 private def toContextExpr : GoalM Expr := do
-  return toContextExprCore (← getVars) (mkConst ``Int)
+  toContextExprCore (← getVars) (mkConst ``Int)
 
 private def withForeignContexts (k : Std.HashMap ForeignType Expr → GoalM α) : GoalM α := do
   go 1 (← get').foreignVars.toList {}
@@ -99,7 +99,7 @@ where
     | [] => k r
     | (type, ctx) :: ctxs =>
       let typeExpr := type.denoteType
-      let ctxExpr := toContextExprCore ctx typeExpr
+      let ctxExpr ← toContextExprCore ctx typeExpr
       withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray) typeExpr) ctxExpr fun ctx => do
         go (i+1) ctxs (r.insert type ctx)
 
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
index fa30307cec..08757c27a7 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Basic.lean
@@ -245,7 +245,7 @@ def dvdCnstr? (e : Expr) : MetaM (Option (Int × Int.Linear.Expr × Array Expr))
     let e := e.applyPerm perm
     return some (d, e, atoms)
 
-def toContextExpr (ctx : Array Expr) : Expr :=
+def toContextExpr (ctx : Array Expr) : MetaM Expr :=
   if h : 0 < ctx.size then
     RArray.toExpr (mkConst ``Int) id (RArray.ofArray ctx h)
   else
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
index 72bcd23eb2..255bf73086 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Int/Simp.lean
@@ -36,37 +36,37 @@ def simpEq? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let p := a.sub b |>.norm
     if p.isUnsatEq then
       let r := mkConst ``False
-      let h := mkApp4 (mkConst ``Int.Linear.eq_eq_false) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
+      let h := mkApp4 (mkConst ``Int.Linear.eq_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq e r))
     else if p.isValidEq then
       let r := mkConst ``True
-      let h := mkApp4 (mkConst ``Int.Linear.eq_eq_true) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
+      let h := mkApp4 (mkConst ``Int.Linear.eq_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq e r))
     else if p.toExpr == a && b == .num 0 then
       return none
     else match p with
       | .add 1 x (.add (-1) y (.num 0)) =>
         let r := mkIntEq atoms[x]! atoms[y]!
-        let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr y) reflBoolTrue
+        let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr y) reflBoolTrue
         return some (r, ← mkExpectedTypeHint h (← mkEq e r))
       | .add 1 x (.num k) =>
         let r := mkIntEq atoms[x]! (toExpr (-k))
-        let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var_const) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr (-k)) reflBoolTrue
+        let h := mkApp6 (mkConst ``Int.Linear.norm_eq_var_const) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr x) (toExpr (-k)) reflBoolTrue
         return some (r, ← mkExpectedTypeHint h (← mkEq e r))
       | _ =>
         let k := p.gcdCoeffs'
         if k == 1 then
           let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
-          let h := mkApp5 (mkConst ``Int.Linear.norm_eq) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
+          let h := mkApp5 (mkConst ``Int.Linear.norm_eq) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
           return some (r, ← mkExpectedTypeHint h (← mkEq e r))
         else if p.getConst % k == 0 then
           let p := p.div k
           let r := mkIntEq (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
-          let h := mkApp6 (mkConst ``Int.Linear.norm_eq_coeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
+          let h := mkApp6 (mkConst ``Int.Linear.norm_eq_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
           return some (r, ← mkExpectedTypeHint h (← mkEq e r))
         else
           let r := mkConst ``False
-          let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
+          let h := mkApp5 (mkConst ``Int.Linear.eq_eq_false_of_divCoeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr (Int.ofNat k)) reflBoolTrue
           return some (r, ← mkExpectedTypeHint h (← mkEq e r))
 
 
@@ -79,11 +79,11 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
     let p := a.sub b |>.norm
     if p.isUnsatLe then
       let r := mkConst ``False
-      let h := mkApp4 (mkConst ``Int.Linear.le_eq_false) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
+      let h := mkApp4 (mkConst ``Int.Linear.le_eq_false) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq e r))
     else if p.isValidLe then
       let r := mkConst ``True
-      let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
+      let h := mkApp4 (mkConst ``Int.Linear.le_eq_true) (← toContextExpr atoms) (toExpr a) (toExpr b) reflBoolTrue
       return some (r, ← mkExpectedTypeHint h (← mkEq e r))
     else if checkIfModified && p.toExpr == a && b == .num 0 then
       return none
@@ -91,16 +91,16 @@ def simpLe? (e : Expr) (checkIfModified : Bool) : MetaM (Option (Expr × Expr))
       let k := p.gcdCoeffs'
       if k == 1 then
         let r := mkIntLE (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
-        let h := mkApp5 (mkConst ``Int.Linear.norm_le) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
+        let h := mkApp5 (mkConst ``Int.Linear.norm_le) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) reflBoolTrue
         return some (r, ← mkExpectedTypeHint h (← mkEq e r))
       else
         let tight := p.getConst % k != 0
         let p := p.div k
         let r := mkIntLE (← p.denoteExpr (atoms[·]!)) (mkIntLit 0)
-        let h := if tight then
-          mkApp6 (mkConst ``Int.Linear.norm_le_coeff_tight) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
+        let h ← if tight then
+          pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff_tight) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
         else
-          mkApp6 (mkConst ``Int.Linear.norm_le_coeff) (toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
+          pure <| mkApp6 (mkConst ``Int.Linear.norm_le_coeff) (← toContextExpr atoms) (toExpr a) (toExpr b) (toExpr p) (toExpr (Int.ofNat k)) reflBoolTrue
         return some (r, ← mkExpectedTypeHint h (← mkEq e r))
 
 def simpRel? (e : Expr) : MetaM (Option (Expr × Expr)) := do
@@ -151,14 +151,14 @@ def simpDvd? (e : Expr) : MetaM (Option (Expr × Expr)) := do
       if e == p.toExpr then
         return none
       let rhs := mkIntDvd (toExpr d') (← p.denoteExpr (atoms[·]!))
-      let h := if g == 1 then
-        mkApp5 (mkConst ``Int.Linear.norm_dvd) (toContextExpr atoms) (toExpr d) (toExpr e) (toExpr p) reflBoolTrue
+      let h ← if g == 1 then
+        pure <| mkApp5 (mkConst ``Int.Linear.norm_dvd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr p) reflBoolTrue
       else
-        mkApp7 (mkConst ``Int.Linear.norm_dvd_gcd) (toContextExpr atoms) (toExpr d) (toExpr e) (toExpr d') (toExpr p) (toExpr g) reflBoolTrue
+        pure <| mkApp7 (mkConst ``Int.Linear.norm_dvd_gcd) (← toContextExpr atoms) (toExpr d) (toExpr e) (toExpr d') (toExpr p) (toExpr g) reflBoolTrue
       return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
     else
       let rhs := mkConst ``False
-      let h := mkApp4 (mkConst ``Int.Linear.dvd_eq_false) (toContextExpr atoms) (toExpr d) (toExpr e) reflBoolTrue
+      let h := mkApp4 (mkConst ``Int.Linear.dvd_eq_false) (← toContextExpr atoms) (toExpr d) (toExpr e) reflBoolTrue
       return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
 
 def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
@@ -167,7 +167,7 @@ def simpExpr? (lhs : Expr) : MetaM (Option (Expr × Expr)) := do
   let e' := p.toExpr
   if e != e' then
     -- We only return some if monomials were fused
-    let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
+    let h := mkApp4 (mkConst ``Int.Linear.Expr.eq_of_norm_eq) (← toContextExpr atoms) (toExpr e) (toExpr p) reflBoolTrue
     let rhs ← p.denoteExpr (atoms[·]!)
     return some (rhs, ← mkExpectedTypeHint h (← mkEq lhs rhs))
   else
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean
index a5f8b68664..7565229c22 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Basic.lean
@@ -179,7 +179,7 @@ def toLinearCnstr? (e : Expr) : MetaM (Option (LinearCnstr × Array Expr)) := do
     let c := c.applyPerm perm
     return some (c, atoms)
 
-def toContextExpr (ctx : Array Expr) : Expr :=
+def toContextExpr (ctx : Array Expr) : MetaM Expr := do
   if h : 0 < ctx.size then
     RArray.toExpr (mkConst ``Nat) id (RArray.ofArray ctx h)
   else
diff --git a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
index 3f3ccad32e..e987c86e7c 100644
--- a/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
+++ b/src/Lean/Meta/Tactic/Simp/Arith/Nat/Simp.lean
@@ -18,17 +18,17 @@ def simpCnstrPos? (e : Expr) : MetaM (Option (Expr × Expr)) := do
     let c₂ := c₁.norm
     if c₂.isUnsat then
       let r := mkConst ``False
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (toContextExpr atoms) (toExpr c) reflBoolTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_false_of_isUnsat) (← toContextExpr atoms) (toExpr c) reflBoolTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else if c₂.isValid then
       let r := mkConst ``True
-      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (toContextExpr atoms) (toExpr c) reflBoolTrue
+      let p := mkApp3 (mkConst ``Nat.Linear.ExprCnstr.eq_true_of_isValid) (← toContextExpr atoms) (toExpr c) reflBoolTrue
       return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
     else
       let c₂ : LinearCnstr := c₂.toExpr
       let r ← c₂.toArith atoms
       if r != lhs then
-        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (toContextExpr atoms) (toExpr c) (toExpr c₂) reflBoolTrue
+        let p := mkApp4 (mkConst ``Nat.Linear.ExprCnstr.eq_of_toNormPoly_eq) (← toContextExpr atoms) (toExpr c) (toExpr c₂) reflBoolTrue
         return some (r, ← mkExpectedTypeHint p (← mkEq lhs r))
       else
         return none
@@ -74,7 +74,7 @@ def simpExpr? (input : Expr) : MetaM (Option (Expr × Expr)) := do
   let e' : LinearExpr := p'.toExpr
   if e' == e then
     return none
-  let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
+  let p := mkApp4 (mkConst ``Nat.Linear.Expr.eq_of_toNormPoly_eq) (← toContextExpr ctx) (toExpr e) (toExpr e') reflBoolTrue
   let r ← e'.toArith ctx
   return some (r, ← mkExpectedTypeHint p (← mkEq input r))
 
diff --git a/tests/lean/run/liaByRefl.lean b/tests/lean/run/liaByRefl.lean
index 422110632e..d8ebac28b2 100644
--- a/tests/lean/run/liaByRefl.lean
+++ b/tests/lean/run/liaByRefl.lean
@@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
   let ts : Array Lean.Syntax := ts
   let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
   if h : 0 < es.size then
-    return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
+    Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
   else
     throwErrorAt tk "RArray cannot be empty"
 
diff --git a/tests/lean/run/linearByRefl.lean b/tests/lean/run/linearByRefl.lean
index 14fed4bea7..e19e6d7bbb 100644
--- a/tests/lean/run/linearByRefl.lean
+++ b/tests/lean/run/linearByRefl.lean
@@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
   let ts : Array Lean.Syntax := ts
   let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
   if h : 0 < es.size then
-    return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
+    Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
   else
     throwErrorAt tk "RArray cannot be empty"
 
diff --git a/tests/lean/run/som1.lean b/tests/lean/run/som1.lean
index fb1b9d5fd7..a73304c136 100644
--- a/tests/lean/run/som1.lean
+++ b/tests/lean/run/som1.lean
@@ -7,7 +7,7 @@ elab tk:"#R[" ts:term,* "]" : term => do
   let ts : Array Lean.Syntax := ts
   let es ← ts.mapM fun stx => Lean.Elab.Term.elabTerm stx none
   if h : 0 < es.size then
-    return (Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h))
+    Lean.RArray.toExpr (← Lean.Meta.inferType es[0]!) id (Lean.RArray.ofArray es h)
   else
     throwErrorAt tk "RArray cannot be empty"