6

假设我有以下（错误的）代码。

data A a b where
  APure ::  (A a b)
  AApply :: A (A b c) c

test :: (A a b) -> a -> b
test (APure) a = a
test AApply a = undefined

然后 GHC 会给我这个错误：

Couldn't match type `b' with `A b1 b'
  `b' is a rigid type variable bound by
      the type signature for test :: A a b -> a -> b
Inaccessible code in
  a pattern with constructor
    AApply :: forall c b. A (A b c) c,
  in an equation for `test'
In the pattern: AApply
In an equation for `test': test AApply a = undefined

这个错误信息不是完全错误的吗？该错误与 AApply 无关。

4

1 回答 1

4

这个错误信息不是完全错误的吗？该错误与AApply.

不完全的。可以说，您收到该错误消息是一个错误，但它并非完全偏离基础。

看片断后一起看整体。

test (APure) a = a

说我们有一个功能

test :: A a b -> r -> r

把它和签名放在一起

test :: (A a b) -> a -> b

并统一，忽略第一个方程的类型错误，类型被细化为

test :: A r r -> r -> r

然后看方程

test AApply a = undefined

看看在提炼的类型下是如何无法访问的，因为

AApply :: A (A b c) c

将需要

c ~ A b c

ifAApply是一个有效的第一个参数。

于 2013-04-21T19:57:58.700 回答