ST-like encapsulation

Question

I am trying to use the type system to ensure that X can never be taken out from the monad M. I'm expecting it to work similar to runST, where it is impossible to mix environments from different threads.

data X s = X Int
type M s = State Int

newX :: M s (X s)
newX = X <$> get

eval :: (forall s. M s a) -> a
eval x = evalState x 0

However the following code does not cause a type error:

ghci> x = eval newX
ghci> :t x
x :: X s

Why does similar code in the ST monad throw an error and mine does not? To my understanding the s in the M s a should become bound, making the s in X s a free type variable and thereby causing an error in the type checker.

Answer 1

To enforce type abstraction, you must use data or newtype, not type.

An unused parameter in a type synonym has no effect at all:

type M s = State Int

So these are equivalent:

newX :: M s (X s)
newX :: State Int (X s)

eval :: (forall s. M s a) -> a
eval :: State Int a -> a

eval is not actually higher-rank.