Моделирование монады ST в Агда

Этот недавний SO вопрос побудил меня написать небезопасную и чистую эмуляцию монады ST в Haskell, слегка модифицированную версию которой вы можете увидеть ниже:

{-# LANGUAGE DeriveFunctor, GeneralizedNewtypeDeriving, RankNTypes #-}

import Control.Monad.Trans.State
import GHC.Prim (Any)
import Unsafe.Coerce (unsafeCoerce)
import Data.List

newtype ST s a = ST (State ([Any], Int) a) deriving (Functor, Applicative, Monad)
newtype STRef s a = STRef Int deriving Show

newSTRef :: a -> ST s (STRef s a)
newSTRef a = ST $ do
  (env, i) <- get
  put (unsafeCoerce a : env, i + 1)
  pure (STRef i)

update :: [a] -> (a -> a) -> Int -> [a]
update as f i = case splitAt i as of
  (as, b:bs) -> as ++ f b : bs
  _          -> as

readSTRef :: STRef s a -> ST s a
readSTRef (STRef i) = ST $ do
  (m, i') <- get
  pure (unsafeCoerce (m !! (i' - i - 1)))

modifySTRef :: STRef s a -> (a -> a) -> ST s ()
modifySTRef (STRef i) f = ST $
  modify $ \(env, i') -> (update env (unsafeCoerce f) (i' - i - 1), i')

runST :: (forall s. ST s a) -> a
runST (ST s) = evalState s ([], 0)

Было бы хорошо, если бы мы могли представить обычный ST-код монады ST без unsafeCoerce. В частности, я хотел бы формализовать причины, по которым работает обычная монашка GHC ST и вышеупомянутая эмуляция. Мне кажется, что они работают, потому что:

Любое STRef s a с правильным тегом s должно быть создано в текущем вычислении ST, так как runST гарантирует, что разные состояния не могут быть перемешаны.
Предыдущая точка вместе с тем фактом, что вычисления ST могут только расширять среду ссылок, подразумевает, что любой STRef s a с правильным тегом s ссылается на допустимое a -типированное местоположение в среде (после, возможно, ослабление ссылки во время выполнения).

Вышеприведенные моменты обеспечивают замечательный опыт программирования без обязательств. Ничто действительно не приближается к безопасному и чистому Haskell, о котором я могу думать; мы можем сделать довольно плохую имитацию с помощью индексированных состояний монадов и гетерогенных списков, но это не выражает каких-либо из вышеперечисленных пунктов и, следовательно, требует доказательств на каждом сайте использования STRef -s.

Я не понимаю, как мы могли бы официально оформить это в Агда. Во-первых, "выделенные в этом вычислении" достаточно сложны. Я думал о представлении STRef -s в качестве доказательств того, что конкретное распределение содержится в конкретном вычислении ST, но это, как представляется, приводит к бесконечной рекурсии индексации типов.

Ответ 1