why StateRefT is defined as a macro?

Stream: lean4

[Asei Inoue]

The need to define it as a macro is not understood. Why not abbrev StateRefT := StateRefT' IO.RealWorld?

import Lean

open Lean Elab Tactic

/-- info: StateRefT' IO.RealWorld State TermElabM : Type → Type -/
#guard_msgs in
  #check StateRefT State TermElabM

[Eric Wieser]

The source says

/-! Recall that `StateRefT` is a macro that infers `ω` from the `m`. -/