RunST prevents accessing the reference of another stateful thread in a closure

Question

I have came across many explanations of RunST's Rank 2 type and how it prevents the reference from escaping RunST. But I couldn't find out why this also prevents the following code from type checking (which is correct but I still want to understand how it is doing that):

test = do v ← newSTRef True
          let a = runST $ readSTRef v
          return True

Compared to:

test = do v ← newSTRef True
          let a = runST $ newSTRef True >>= λv → readSTRef v
          return True

It seems to me that the type of newSTRef is same for both cases: Λs. Bool → ST s (STRef s Bool). And the type of v is ∃s. STRef s Bool in both cases as well if I understand it right. But then I am puzzled at what to do next to show why the first example doesn't type check, I don't see differences between both examples except that in the first example v is bound outside runST and inside in the second, which I suspect is the key here. Please help me show this and/or correct me if I am wrong somewhere along my reasoning.

Answer 1

The function runST :: (forall s . ST s a) -> a is where the magic occurs. The right question to ask is what it takes to produce a computation which has type forall s . ST s a.

Reading it as English, this is a computation which is valid for all choices of s, the phantom variable which indicates a particular "thread" of ST computation.

When you use newSTRef :: a -> ST s (STRef s a) you're producing an STRef which shares its thread variable with the ST thread which generates it. This means that the s type for the value v is fixed to be identical to the s type for the larger thread. This fixedness means that operations involving v no longer are valid "for all" choices of thread s. Thus, runST will reject operations involving v.

Conversely, a computation like newSTRef True >>= \v -> readSTRef v makes sense in any ST thread. The whole computation has a type which is valid "for all" ST threads s. This means it can be run using runST.

In general, runST must wrap around the creation of all ST threads. This means that all of the choices of s inside the argument to runST are arbitrary. If something from the context surrounding runST interacts with runST's argument then that will likely fix some of those choices of s to match the surrounding context and thus no longer be freely applicable "for all" choices of s.