奇怪的ghc错误信息,"我的大脑爆炸了"？

Question

当我尝试使用proc语法(使用Netwire和Vinyl)对GADT 进行模式匹配时:

sceneRoot = proc inputs -> do
            let (Identity camera :& Identity children) = inputs 
            returnA -< (<*>) (map (rGet draw) children) . pure

我从ghc-7.6.3得到(相当奇怪的)编译器错误

  My brain just exploded
    I can't handle pattern bindings for existential or GADT data constructors.
    Instead, use a case-expression, or do-notation, to unpack the constructor.
    In the pattern: Identity cam :& Identity childs

当我将模式放在模式中时,我得到了类似的错误proc (...).为什么是这样？它不健全,还是只是未实现？

Answer 1

考虑GADT

data S a where
  S :: Show a => S a

和代码的执行

foo :: S a -> a -> String
foo s x = case s of
            S -> show x

在基于字典的Haskell实现中,可以预期该值s携带类字典,并且从所述字典中case提取show函数以便show x可以执行.

如果我们执行

foo undefined (\x::Int -> 4::Int)

我们得到一个例外.在操作上,这是预期的,因为我们无法访问字典.更一般地说,case (undefined :: T) of K -> ...会产生错误,因为它会强制进行评估undefined(假设T不是a newtype).

现在考虑代码(让我们假装这个编译)

bar :: S a -> a -> String
bar s x = let S = s in show x

和执行

bar undefined (\x::Int -> 4::Int)

这应该怎么办？有人可能认为它应该产生与之相同的例外foo.如果是这种情况,参考透明度就意味着这一点

let S = undefined :: S (Int->Int) in show (\x::Int -> 4::Int)

同样的例外也失败了.这意味着let正在评估undefined表达式,非常不同于例如

let [] = undefined :: [Int] in 5

评估为5.

实际上,a let中的模式是懒惰的:它们并不强制表达式的评估,不像case.这就是为什么例如

let (x,y) = undefined :: (Int,Char) in 5

成功评估为5.

人们可能想要let S = e in e'评估e是否show需要e',但感觉相当奇怪.另外,评估时let S = e1 ; S = e2 in show ...它会不清楚是否要评估e1,e2或两者兼而有之.

GHC目前选择用一个简单的规则来禁止所有这些案例:消除GADT时没有懒惰的模式.