Couldn't match type `a' with `STRef s Integer'

Question

When I compile runST (newSTRef 1) I got a message:

Couldn't match type `a' with `STRef s Integer'
Expected: ST s a
Actual: ST s (STRef s Integer)

But when I use some other type as a (for example, Integer), it works: runST ((newSTRef 1) >>= readSTRef). Looks like STRef is a special type, it doesn't match when other types do. I'm novice in Haskell, it looks like I don't understand something fundamental, sorry. Thanks in advance.

Answer 1

Look at the type of runST:

runST :: forall a. (forall s. ST s a) → a

In order to compute a value of type a using ST, you must supply a computation of type forall s. ST s a; note that a cannot possibly depend on s since s is chosen by the callee (runST). This is the crucial restriction that ensures that extracting data from ST computations is safe even though ST computations have side effects: those side effects are constrained to the state thread s and thus cannot escape into the return type a.

In your case, you are trying to return an STRef s Integer, which depends on s, so there is no way to make it work (and this is very much a feature).

Note that earlier versions of GHC gave a slightly different error message:

    • Couldn't match type ‘a’ with ‘STRef s Integer’
        because type variable ‘s’ would escape its scope
      This (rigid, skolem) type variable is bound by
        a type expected by the context:
          forall s. ST s a

Answer 2

I reproduced the problem without ST monad. Now the problem is more visible. Function f5 cannot return type with s if s is marked as forall inside an implementation of the function.

data T1 s a = T1 a
data T2 s a = T2 a

f1 :: (forall s. T1 s a) -> a
f1 (T1 a) = a

f2 :: T1 s Integer
f2 = T1 1

f3 :: T1 s (T2 s Integer)
f3 = T1 (T2 1)

f4 :: Integer
f4 = f1 f2 -- OK, returns 1

f5 :: T2 s Integer
f5 = f1 f3 -- Error
--Couldn't match type `s1' with `s'
--Expected: T1 s1 (T2 s Integer)
--  Actual: T1 s1 (T2 s1 Integer)