RunST prevents accessing the reference of another stateful thread in a closure
haskell, monads, types
Solution
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`.
Problem
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.