fix: regression from ST redefinition (#10940)

This PR fixes a regression introduced by the `ST` redefinition by making
the definition of `ST` as
reducible as previously. The key issue here is that in the previous
state it would reduce to a
function at which point the monad lifting mechanisms don't kick in in
the same fashion anymore.

Author: hargoniX

src/Init/System/ST.lean

@@ -31,7 +31,7 @@ A restricted version of `IO` in which mutable state is the only side effect.
 
 It is possible to run `ST` computations in a non-monadic context using `runST`.
 -/
-abbrev ST (σ : Type) (α : Type) := Void σ → ST.Out σ α
+@[expose] def ST (σ : Type) (α : Type) := Void σ → ST.Out σ α
 
 namespace ST
 

tests/lean/run/aesop_run_metam.lean

@@ -0,0 +1,6 @@
+import Lean.Meta.Basic
+
+open Lean
+
+instance [Monad m] [MonadLiftT MetaM m] : MonadLiftT (ST IO.RealWorld) m where
+  monadLift x := (x : MetaM _)