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.
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.