fix: bug at runST and runEST

src/Init/System/ST.lean

@@ -22,12 +22,14 @@ class STWorld (σ : outParam Type) (m : Type → Type)
 instance {σ m n} [STWorld σ m] [MonadLift m n] : STWorld σ n := ⟨⟩
 instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
 
-@[inline] def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α :=
+@[noinline nospecialize]
+def runEST {ε α : Type} (x : forall (σ : Type), EST ε σ α) : Except ε α :=
   match x Unit () with
   | EStateM.Result.ok a _     => Except.ok a
   | EStateM.Result.error ex _ => Except.error ex
 
-@[inline] def runST {α : Type} (x : forall (σ : Type), ST σ α) : α :=
+@[noinline nospecialize]
+def runST {α : Type} (x : forall (σ : Type), ST σ α) : α :=
   match x Unit () with
   | EStateM.Result.ok a _     => a
   | EStateM.Result.error ex _ => nomatch ex

tests/lean/runSTBug.lean

@@ -0,0 +1,19 @@
+import Lean
+
+open Lean
+
+def f (xs : List Nat) (delta : Nat) : List Nat :=
+  runST (fun ω => visit xs |>.run)
+where
+  visit {ω} : List Nat → MonadCacheT Nat Nat (ST ω) (List Nat)
+    | []    => []
+    | a::as => do
+      let b ← checkCache a fun _ => return a + delta
+      return b :: (← visit as)
+
+def tst (xs : List Nat) : IO Unit := do
+  IO.println (f xs 10)
+  IO.println (f xs 20)
+  IO.println (f xs 30)
+
+#eval tst [1, 2, 3, 1, 2]

tests/lean/runSTBug.lean.expected.out

@@ -0,0 +1,3 @@
+[11, 12, 13, 11, 12]
+[21, 22, 23, 21, 22]
+[31, 32, 33, 31, 32]