ST周围的newtype会导致类型错误

Question

当我尝试在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启用(因为它在我的真实代码中),它会再次失败.

Answer 1

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

GHC推断m有型ST ??? a,其中???是一个类型变量,可以与任何统一,并与一些统一*.因此,我们再通过它一起runST并runST希望有一个ST s a这样m与它相结合,并???与统一s.但是等等,现在我们正在与s范围之外的范围内进行统一,因为范围s是如此灾难.

一个更简单的例子是

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

我们再次得到了同样的错误,因为我们试图用的类型,统一m使用t,但t在过小的范围.

最简单的解决方案就是不要用它来创建这个类型的变量

 test m = runST (unM m)

这里unM返回一个很好的,真正的多态ST,runST很满意.你可以使用let它,因为它默认是多态的,但是因为-XTypeFamilies它会让它变形,就像你发现的模式匹配一​​样.

**似乎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正如您对单形类型变量所期望的那样.为什么我发现的每个奇怪的类型错误似乎都隐藏了某种形式的单态变量..