# Mixing IO w / ST Monad - "variable of type s2" would disappear due to its volume "

I decided to simplify my code to find out what conditions caused the error. I start with a simple nested "s" like `ST s (STArray s x y)`

this:

```
{-# LANGUAGE RankNTypes #-}
import Control.Monad.ST
import Control.Applicative
data Foo s = Foo { foo::Bool }
newFoo :: ST s (Foo s)
newFoo = return $ Foo False
```

To check the status code, I run the following transformation:

```
changeFoo :: (forall s. ST s (Foo s)) -> ST s (Foo s)
changeFoo sf = do
f <- sf
let f' = Foo (not $ foo f)
return f'
```

I would like to extract the value from the state while saving the state, so the next step would be to extract the Bool value:

```
splitChangeFoo :: (forall s. ST s (Foo s)) -> ST s (Bool,(Foo s))
splitChangeFoo sf = do
f <- changeFoo sf
let b = foo f
return (b,f)
```

To extract this Bool, I have to use `runST`

. I understand that this will create additional state, which I will provide by providing `forall s.`

in the return type:

```
extractFoo :: (forall s. ST s (Bool,(Foo s))) -> (forall s. (Bool,ST s ((Foo s))))
extractFoo sbf = (runST $ fst <$> sbf,snd <$> sbf)
```

The example above compiles without final `forall`

, however in the circumstance I am trying to debug this is not possible. Regardless, in this case, it compiles anyway.

I can use the above code to combine multiple uses of state together:

```
testFoo :: (Bool, ST s (Foo s))
testFoo = (b && b',sf')
where
(b,sf) = extractFoo $ splitChangeFoo newFoo
(b',sf') = extractFoo $ splitChangeFoo sf
```

Now I am trying to throw IO into the mix and so I am using applicative fmap `<$>`

. This won't compile: (NB. Same problem if I use `fmap`

or `>>= return`

rather than `<$>`

)

```
testBar :: IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
where
testBar' :: IO (Bool, ST s (Foo s))
testBar' = return $ extractFoo $ splitChangeFoo newFoo
```

With the following error:

```
Couldn't match type `s0' with `s2'
because type variable `s2' would escape its scope
This (rigid, skolem) type variable is bound by
a type expected by the context: ST s2 (Foo s2)
The following variables have types that mention s0
sf :: ST s0 (Foo s0) (bound at src\Tests.hs:132:16)
Expected type: ST s2 (Foo s2)
Actual type: ST s0 (Foo s0)
In the first argument of `splitChangeFoo', namely `sf'
In the second argument of `($)', namely `splitChangeFoo sf'
In the expression: extractFoo $ splitChangeFoo sf
```

I know from this SO question about the structure of ST functions that not all possible uses of ST are taken into account by the compiler. To test this assumption, I modified the above function to not use IO and just pass the return value to the lambda:

```
testFooBar :: (Bool, ST s (Foo s))
testFooBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) testFooBar'
where
testFooBar' :: (Bool, ST s (Foo s))
testFooBar' = extractFoo $ splitChangeFoo newFoo
```

Predictably this also fails to compile with an identical error message.

It's a challenge. I have a reasonable amount of I / O that needs to interact with a set of deeply nested ST operations. It works fine for one iteration, however I cannot use the return value anymore.

source to share

I'm not sure how this all works in your real code and it seems to me that you are doing something more convoluted than strictly necessary, but since I cannot say much definitively about this, I will only refer to the nearest problems in your question.

### Why `testBar`

doesn't it work

In `(\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'`

we have `<$>`

, which has a type `forall a b. (a -> b) -> IO a -> IO b`

. However, it `testBar`

has a type `forall s. IO (Bool, ST s (Foo s))`

. We can only apply `fmap`

to `testBar`

after `s`

.

In your case `s`

, a new variable is instantiated `s0`

, so inside the lambda `sf`

there is this parameter as well. Unfortunately, it `s0`

differs from the topmost parameter `s`

(which we would like to see in the return type), so it `sf`

is currently practically not used.

In case the `testFooBar`

problem is that the lambda arguments are monomorphic by default (otherwise type inference would become undecidable), so we just need to annotate the type:

```
testFooBar :: (Bool, ST s (Foo s))
testFooBar =
(\(x :: forall s. (Bool, (ST s (Foo s)))) -> extractFoo $ splitChangeFoo $ snd x) testFooBar'
where
testFooBar' :: (Bool, ST s (Foo s))
testFooBar' = extractFoo $ splitChangeFoo newFoo
```

All we have done here is introduce a cumbersome alternative for expressions `let`

and `where`

. But that doesn't matter as `testFoo`

`fmap`

it requires the lambda argument to be fully instance type, so we can't annotate our troubles.

We can try the following:

```
{-# LANGUAGE ScopedTypeVariables #-}
testBar :: forall s. IO (Bool, ST s (Foo s))
testBar = (\(b,sf) -> extractFoo $ splitChangeFoo sf) <$> testBar'
where
testBar' :: IO (Bool, ST s (Foo s))
testBar' = return $ extractFoo $ splitChangeFoo newFoo
```

Now `testBar`

has the correct `s`

parameter; since it is no longer generalized, we can immediately apply to it `fmap`

. Internally, the lambda `sf`

has a type `ST s (Foo s)`

. But this also won't work, since a `extractFoo`

expects a `forall`

quantitative argument, but `sf`

is monomorphic. Now - if you try this version in GHCi - the error message we get is no longer related to skolems speedup, but good old fashioned one `can't match type s with s2`

.

### How to help

Obviously `extract`

must return `forall s.`

-ed in some way `ST s (Foo s)`

. Your original type doesn't fit because GHC doesn't have polymorphic return types, so

`(forall s. ST s (Bool, Foo s)) -> (forall s. (Bool, ST s (Foo s)))`

actually means

```
forall s. (forall s. ST s (Bool, Foo s)) -> (Bool, ST s (Foo s))
```

since GHC pops up all `forall`

-s at the top of the area. This simplifies type inference and allows the use of typecheck terms. Indeed, you can type `:t extract`

in GHCi and represent it as a float.

A possible solution would include `ImprediactiveTypes`

and have

```
extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, forall s. ST s (Foo s))
```

But there is a reason why it is `ImpredicativeTypes`

rarely used: it is poorly integrated with the rest of the type checking machine and tends to fail for all but the simplest purposes. As an example, assuming `extract`

with a changed type, the following example does not check the type:

```
testBar :: IO (Bool, forall s. ST s (Foo s))
testBar = (\(b, sf) -> (b, sf)) <$> testBar'
where
testBar' :: IO (Bool, forall s. ST s (Foo s))
testBar' = return $ extractFoo $ splitChangeFoo newFoo
```

But it changes the typecheck when we change `(\(b, sf) -> (b, sf))`

to `(\x -> x)`

! So let's forget about the troubled types.

The usual solution is to just wrap quantitative types in newtype. It's much less flexible than the non-specific type, but at least it works.

```
{-# LANGUAGE RankNTypes #-}
import Control.Monad.ST
import Control.Applicative
import Control.Arrow
data Foo s = Foo { foo::Bool }
newtype ST' f = ST' {unST' :: forall s. ST s (f s)}
newFoo :: ST s (Foo s)
newFoo = return $ Foo False
splitChangeFoo :: ST s (Foo s) -> ST s (Bool, Foo s)
splitChangeFoo = fmap (\(Foo b) -> (b, Foo (not b)))
extract :: (forall s. ST s (Bool, Foo s)) -> (Bool, ST' Foo)
extract s = (runST $ fst <$> s, ST' $ snd <$> s)
testBar :: IO (Bool, ST s (Foo s))
testBar = (\(_, ST' s) -> second unST' $ extract $ splitChangeFoo s) <$>
(return $ extract $ splitChangeFoo newFoo)
```

So, whenever you need to return quantitative types, wrap it in a new type and then expand as needed. You might want to stick with the normal type argument scheme for your custom types (for example, always make the parameter `s`

last, so you can use the same type `ST'`

for multiple types to be wrapped).

source to share