I would say common explanation is that existential s prohibits you from using one STRef in multiple instances of runST - so you could try to run those ST actions in separate runSTs, but you wouldn't have any STRef to pass to them

It may be trying avoid unifying some external variable (I guess it infers k :: p1from lambda) with type that contains existential, because it's not sure whether it could be used outside of proper scope (runST) that way, thus "escaping"? But when you use freeze, it's type is filled in inside of runST call, so it should be fine?

But at that stage I guess you already know the structure of the types for your function and it's not as useful for getting to that point as λ> :type \mv k -> runST $ mv >>= k would have been if that could have told you some information about the types of mv and k.

λ> :t runST $ _mv >>= _k
<interactive>:1:9: error:
• Found hole: _mv :: ST s a0
Where: ‘a0’ is an ambiguous type variable
‘s’ is a rigid type variable bound by
a type expected by the context:
forall s. ST s a
at <interactive>:1:9-18
Or perhaps ‘_mv’ is mis-spelled, or not in scope
• In the first argument of ‘(>>=)’, namely ‘_mv’
In the second argument of ‘($)’, namely ‘_mv >>= _k’
In the expression: runST $ _mv >>= _k
<interactive>:1:17: error:
• Found hole: _k :: a0 -> ST s a
Where: ‘a0’ is an ambiguous type variable
‘s’ is a rigid type variable bound by
a type expected by the context:
forall s. ST s a
at <interactive>:1:9-18
‘a’ is a rigid type variable bound by
the inferred type of it :: a
at <interactive>:1:1
Or perhaps ‘_k’ is mis-spelled, or not in scope
• In the second argument of ‘(>>=)’, namely ‘_k’
In the second argument of ‘($)’, namely ‘_mv >>= _k’
In the expression: runST $ _mv >>= _k
• Valid hole fits include
fixST :: forall a s. (a -> ST s a) -> ST s a
with fixST @a @s
(imported from ‘Control.Monad.ST’
(and originally defined in ‘base-4.14.0.0:Control.Monad.ST.Imp’))
return :: forall (m :: * -> *) a. Monad m => a -> m a
with return @(ST s) @a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
fail :: forall (m :: * -> *) a. MonadFail m => String -> m a
with fail @(ST s) @a
(imported from ‘Prelude’
(and originally defined in ‘Control.Monad.Fail’))
pure :: forall (f :: * -> *) a. Applicative f => a -> f a
with pure @(ST s) @a
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
id :: forall a. a -> a
with id @(ST s a)
(imported from ‘Prelude’ (and originally defined in ‘GHC.Base’))
head :: forall a. [a] -> a
with head @(ST s a)
(imported from ‘Prelude’ (and originally defined in ‘GHC.List’))
(Some hole fits suppressed; use -fmax-valid-hole-fits=N or -fno-max-valid-hole-fits)

It seems to me that the

`forall s`

existential quantifier in`runST`

is the linchpin that enforces sequential reads/writes in the`ST`

monad, but I'd like to hear other people's take on it. I wrote a blog post about it https://chrismwendt.github.io/blog/2018/03/02/what-if-run-st-did-not-use-existential-quantification.html Is this a useful way to view it? Are there any glaring problems with looking at it this way?I would say common explanation is that existential

`s`

prohibits you from using one`STRef`

in multiple instances of`runST`

- so you could try to run those`ST`

actions in separate`runST`

s, but you wouldn't have any`STRef`

to pass to themI've been confused by how

`runST`

works this week actually. It throws an error when I try this in the repl:And if I feed it a function (say

`initMV`

) for that`m`

that returns`ST s (MV.MVector s SomeUnboxType)`

, it still complains:but if I replace the

`k`

with something a simple as`V.freeze`

there are no problems at all:what's GHC struggling with exactly?

It may be trying avoid unifying some external variable (I guess it infers

`k :: p1`

from lambda) with type that contains existential, because it's not sure whether it could be used outside of proper scope (`runST`

) that way, thus "escaping"? But when you use`freeze`

, it's type is filled in inside of`runST`

call, so it should be fine?`p1`

"lives longer" than`s`

, so unifying with it would be bad - try giving`k`

binding as concrete annotation as possible (or use type signature)(That is, something like

`forall s. something -> ST s somethingElse`

)Yeah that works with

`RankNTypes`

on.But at that stage I guess you already know the structure of the types for your function and it's not as useful for getting to that point as

`λ> :type \mv k -> runST $ mv >>= k`

would have been if that could have told you some information about the types of`mv`

and`k`

.You could use typed holes instead of bindings:

It even tells you what "fits" there

This seems close, but still isn't well-typed "Couldn't match type ‘s’ with ‘s0’":

If that were well-typed, I think you could replace

`a`

with`f s`

to support passing`STRef`

s from`m`

to`k`

:@Peter Kjeld Andersen I think I solved it with the help of @TheMatten

Instead of

`F (STRef s a)`

, you'd probably use something like`Flip p a b`

, but it seems like this would be extremely cumbersome to use :oh_no: