Why does this equivalent program not compile?

Question

This program:

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

import qualified Data.Vector.Mutable as MV
import qualified Data.Vector as V
import Control.Monad.ST
import Control.Monad.Primitive

unsafeModify :: [(forall s . MV.MVector s Int -> ST s ())] -> V.Vector Int -> V.Vector Int
unsafeModify mods vec = runST $ do
    mvec <- V.unsafeThaw vec
    (mods !! 0) mvec
    V.unsafeFreeze mvec

Compiles. This program:

{-# LANGUAGE RankNTypes, ImpredicativeTypes #-}

import qualified Data.Vector.Mutable as MV
import qualified Data.Vector as V
import Control.Monad.ST
import Control.Monad.Primitive

unsafeModify :: [(forall s . MV.MVector s Int -> ST s ())] -> V.Vector Int -> V.Vector Int
unsafeModify mods vec = runST $ do
    mvec <- V.unsafeThaw vec
    ($ mvec) (mods !! 0)
    V.unsafeFreeze mvec

Does not compile with the following error:

Muts.hs:10:15:
    Couldn't match type ‘forall s1. UV.MVector s1 Int -> ST s1 ()’
                  with ‘UV.MVector s Int -> ST s a0’
    Expected type: [UV.MVector s Int -> ST s a0]
      Actual type: [forall s. UV.MVector s Int -> ST s ()]
    Relevant bindings include
      mvec :: UV.MVector s Int (bound at Muts.hs:9:5)
    In the first argument of ‘(!!)’, namely ‘mods’
    In the first argument of ‘$ mvec’, namely ‘(mods !! 0)’

Why?

Answer 1

_{Note: This post is written in literate Haskell. You can save it as Unsafe.lhs and try it in your GHCi.}

---

Let's compare the types of the different lines:

 mods                ::     [(forall s . MV.MVector s Int -> ST s ())]
(mods !! 0)          ::      (forall s . MV.MVector s Int -> ST s ())
(mods !! 0)  mvec    ::       forall s. ST s ()


($ mvec)             ::     (MV.Vector s Int -> b) -> b
         (mods !! 0) ::     (forall s . MV.MVector s Int -> ST s ())
($ mvec) (mods !! 0) ::     ????????????????????????

They aren't equivalent due to $'s type:

($) :: forall a b. (a -> b) -> a -> b

Whereas you would need something along

($)  :: (a ~ (forall s . MV.MVector s Int -> ST s ())) =>
      (a -> b) -> a -> b

which isn't legal.

However, let's have a look at what you actually want to do.

> {-# LANGUAGE RankNTypes #-}

> import qualified Data.Vector.Mutable as MV
> import qualified Data.Vector as V
> import Control.Monad.ST
> import Control.Monad.Primitive

  unsafeModify :: ??? -> V.Vector Int -> V.Vector Int

> unsafeModify mods vec = runST $ do
>   mvec <- V.unsafeThaw vec
>   mapM_ ($ mvec) (mods !! 0)
>   V.unsafeFreeze mvec

Things got messy due to unsafeModify's polymorphic first argument mods. Your original type

[(forall s . MV.MVector s Int -> ST s ())]

tells us it is a list of functions, where every function is polymorphic the parameter s, so every function could use another s. However, that's too much. It's fine if the s gets shared throuhgout the whole list:

(forall s. [MV.MVector s Int -> ST s ()])

After all, we want to use all functions in the same ST computation, therefore the type of the stream state token s can be the same. We end up with

> unsafeModify :: (forall s. [MV.MVector s Int -> ST s ()]) -> V.Vector Int -> V.Vector Int

And now your code happily compiles, regardless of whether you use ($ mvec) (mods !! 0), (mods !! 0) mvec or mapM_, because s is now correctly fixed by runST throughout the whole list.