为什么这个等价的程序不编译？

Question

这个项目：

{-# 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

编译。这个项目：

{-# 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

不使用下列错误进行编译：

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)’

为什么？

Answer 1

(这可能是一个评论，但我需要更多的空间。)

遗憾的是，正如@dfeuer所指出的那样，非谓词类型在GHC中不太有效。考虑一下这个例子：

{-# LANGUAGE ImpredicativeTypes, PartialTypeSignatures #-}
import qualified Data.Vector.Mutable as MV
import Control.Monad.ST

-- myIndex :: [forall s. MV.MVector s Int -> ST s ()] 
--         -> Int
--         -> (forall s. MV.MVector s Int -> ST s ())
myIndex = (!!) :: [forall s. MV.MVector s Int -> ST s ()] -> Int -> _

它编译成功，但由于类型漏洞而发出警告：

VectorTest.hs:9:69: Warning:
    Found hole ‘_’ with type: forall s. MV.MVector s Int -> ST s ()
    Relevant bindings include
      myIndex :: [forall s. MV.MVector s Int -> ST s ()]
                 -> Int -> forall s. MV.MVector s Int -> ST s ()
        (bound at VectorTest.hs:9:1)

我们可以尝试删除PartialTypeSignatures扩展并用它的类型forall s. MV.MVector s Int -> ST s ()填充这个洞。但这是可怕的失败：

VectorTest.hs:9:11:
    Couldn't match type ‘forall s2. MV.MVector s2 Int -> ST s2 ()’
                   with ‘MV.MVector s1 Int -> ST s1 ()’
    Expected type: [forall s. MV.MVector s Int -> ST s ()]
                   -> Int -> MV.MVector s1 Int -> ST s1 ()
      Actual type: [MV.MVector s1 Int -> ST s1 ()]
                   -> Int -> MV.MVector s1 Int -> ST s1 ()

最后一个forall被提升到顶层，现在GHC推断(!!)的第一个参数必须是一个单形元素[MV.MVector s1 Int -> ST s1 ()]的列表，尽管我们进行了注释！基本上，GHC有两个选择：

-- Note the hoisted forall s1
myIndex = (!!) :: forall s1. [forall s. MV.MVector s Int -> ST s ()] -> Int 
               -- ^ first choice for instantiating the type of (!!)
               -> MV.MVector s1 Int -> ST s1 ()
               -- ^ second choice

GHC选择第二个，并失败。只有部分类型签名，我才能删除第二选择，以便GHC被迫做正确的事情。

如果我们有像GHC那样的显式类型应用程序，我们就可以编写(!!) @ (forall s. ...)，但是遗憾的是，我们没有。