Why there is no ST monad transformer

WhytheresnoSTT.hs

{-# LANGUAGE RankNTypes #-}

import Control.Monad
import Data.Void
import GHC.Exts (Any)
import Unsafe.Coerce

-- Candidate for "ST monad transformer"

newtype STT s m a = STT ([Any] -> m (a, [Any]))

-- References are pointers into the heap ([Any])
newtype Ref s a = Ref Int

-- Just a state monad...
instance Monad m => Functor (STT s m) where
  fmap = liftM

instance Monad m => Applicative (STT s m) where
  (<*>) = ap
  pure x = STT (\s -> pure (x, s))

instance Monad m => Monad (STT s m) where
  STT u >>= k = STT (\s -> do
    (a, s') <- u s
    let STT v = k a
    v s')

runSTT :: Monad m => (forall s. STT s m a) -> m a
runSTT (STT r) = fmap fst (r [])

liftSTT :: Monad m => m a -> STT s m a
liftSTT y = STT (\s -> fmap (\a -> (a, s)) y)

-- unsafeCoerce below

-- Create and initialize reference
newRef :: Monad m => a -> STT s m (Ref s a)
newRef a = STT (\s -> pure (Ref (length s), s ++ [unsafeCoerce a :: Any]))
--                                                ^^^^^^^^^^^^

readRef :: Monad m => Ref s a -> STT s m a
readRef (Ref n) = STT (\s -> pure (unsafeCoerce (s !! n), s))
--                                 ^^^^^^^^^^^^


-- Demonstration that STT is unsafe

-- The continuation monad
newtype K r a = K ((a -> r) -> r)

instance Functor (K r) where
  fmap = liftM

instance Applicative (K r) where
  (<*>) = ap
  pure x = K (\k -> k x)

instance Monad (K r) where
  K u >>= h = K (\k -> u (\ x -> h' x k)) where
    h' x = let K y = h x in y

runSTTK :: (forall s. STT s (K r) r) -> r
runSTTK y =
  let K u = runSTT y in u id

-- Sanity check that STT and K "work" in simple cases
okST :: STT s (K r) (Int, Bool)
okST = do
  x <- newRef (0 :: Int)
  y <- newRef True
  liftM2 (,) (readRef x) (readRef y)
  -- (0, True)
  
-- !!FUN!! EXPERIMENT BELOW

-- Use a time machine (e -> K r Void) in one timeline to send an e to
-- the other timeline.
--
-- How this works: first return a Right (starting the first timeline),
-- with a certain function (e -> _), which, if it is ever called
-- (with some argument e), backtracks to return the argument
-- as a Left (ending the first and starting the second timeline).
--
-- This is also known as a proof of the double negation of the
-- Law of Excluded Middle (LEM) in intuitionistic logic.
lem :: K r (Either e (e -> K r r'))
lem = K (\k -> k (Right (\e -> K (\_ -> k (Left e)))))

-- Breaking the type system with STT
badST :: a -> STT s (K r) b
badST a = do
  x <- liftSTT lem  -- x :: Either (Ref s b) (Ref s b -> K r b)
  case x of
    Right k -> do
      -- In the first timeline, we are given a time machine k which can carry a (Ref s b)
      r <- newRef undefined   -- We allocate a (Ref s b)
      liftSTT (k r)           -- We send it back in time
    Left r -> do
      -- In the second timeline, we get a reference out of nowhere (actually, from the previous timeline).
      _ <- newRef a     -- Allocate a reference of type a for **no reason** (actually, to populate the place the previous reference is pointing to with something of a different type)
      readRef r         -- Read the old reference

unsafeCoerce_ :: a -> b
unsafeCoerce_ a = runSTTK (badST a)

main :: IO ()
main = do
  print (runSTTK okST)   -- Sanity check (0, True)
  print (unsafeCoerce_ True :: Int)  -- segfault or a very bad looking number