chore: remove workaround

src/Init/Data/RArray.lean

@@ -26,11 +26,11 @@ See `RArray.ofFn` and `RArray.ofArray` in module `Lean.Data.RArray` for function
 It is not universe-polymorphic. ; smaller proof objects and no complication with the `ToExpr` type
 class.
 -/
-inductive RArray (α : Type) : Type where
+inductive RArray (α : Type u) : Type u where
   | leaf : α → RArray α
   | branch : Nat → RArray α → RArray α → RArray α
 
-variable {α : Type}
+variable {α : Type u}
 
 /-- The crucial operation, written with very little abstractional overhead -/
 noncomputable def RArray.get (a : RArray α) (n : Nat) : α :=

src/Lean/Data/RArray.lean

@@ -59,22 +59,17 @@ where
     case case1 => simp [ofFn.go, size]
     case case2 ih1 ih2 hiu => rw [ofFn.go]; simp +zetaDelta [size, *]; omega
 
-open Meta
+open Meta in
 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])
+  let u ← getDecLevel ty
+  let leaf := mkConst ``RArray.leaf [u]
+  let branch := mkConst ``RArray.branch [u]
+  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
 
 end Lean

src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean

@@ -100,7 +100,7 @@ where
     | (type, ctx) :: ctxs =>
       let typeExpr := type.denoteType
       let ctxExpr ← toContextExprCore ctx typeExpr
-      withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray) typeExpr) ctxExpr fun ctx => do
+      withLetDecl ((`ctx).appendIndexAfter i) (mkApp (mkConst ``RArray [levelZero]) typeExpr) ctxExpr fun ctx => do
         go (i+1) ctxs (r.insert type ctx)
 
 private def getLetCtxVars : ProofM (Array Expr) := do
@@ -110,7 +110,7 @@ private def getLetCtxVars : ProofM (Array Expr) := do
   return r
 
 private abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
-  withLetDecl `ctx (mkApp (mkConst ``RArray) (mkConst ``Int)) (← toContextExpr) fun ctx =>
+  withLetDecl `ctx (mkApp (mkConst ``RArray [levelZero]) (mkConst ``Int)) (← toContextExpr) fun ctx =>
   withForeignContexts fun foreignCtxs =>
     go { ctx, foreignCtxs } |>.run' {}
 where