7

当我尝试在 GHC 7.4.1 下加载以下代码时：

{-# LANGUAGE RankNTypes #-}

import Control.Monad.ST

newtype M s a = M { unM :: ST s a }

runM :: (forall s. M s a) -> a
runM (M m) = runST m

它失败并显示以下消息：

test.hs:9:14:
    Couldn't match type `s0' with `s'
      because type variable `s' would escape its scope
    This (rigid, skolem) type variable is bound by
      a type expected by the context: ST s a
    The following variables have types that mention s0
      m :: ST s0 a (bound at test.hs:9:9)
    In the first argument of `runST', namely `m'
    In the expression: runST m
    In an equation for `runM': runM (M m) = runST m

为什么这会失败，什么时候M只是一个包装器ST？

（我的实际程序在顶部堆叠了一些变压器——这只是一个最小的例子。）

编辑：似乎添加let解决了这个问题：

runM m = let M m' = m in runST m

但是，如果TypeFamilies启用（就像在我的真实代码中一样），它会再次失败。

4

1 回答 1

11

这是模式匹配 + rankntypes 的问题。

GHC 推断m有类型ST ??? awhere???是一个类型变量，它可以与任何东西统一并且必须与某物统一*。所以我们然后将它传递给runST并runST想要一个ST s asom与它统一并与???统一s。但是等等，现在我们正在与定义范围如此灾难s的范围之外统一。s

一个更简单的例子是

test (M m) = (m :: forall t . ST t a) `seq` ()

我们再次得到同样的错误，因为我们试图与musing的类型统一t，但t范围太小。

最简单的解决方案就是不使用

 test m = runST (unM m)

这里unM返回一个好的和真正的多态ST，它runST是满意的。您可以使用let它，因为它默认是多态的，但是因为-XTypeFamilies它会使 let 单态它会像您发现的模式匹配一​​样爆炸。

** 看起来m是单态的。let是多态的，没有类型族，所以我怀疑这是怎么回事。它的行为就像它

test :: forall a. (forall t. M t a) -> ()
test (M m) = (m :: ST Bool a) `seq` (m :: ST Int a) `seq` ()

尝试统一的错误Bool以及Int您对单态类型变量的期望。为什么我发现的每一个奇怪的类型错误似乎都隐藏了某种形式的单态类型变量..

于 2013-09-12T03:51:28.820 回答