Haskell 无法访问的代码错误？

Question

假设我有以下(错误的)代码。

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 无关。

Answer 1

Isn't this error message completely wrong? The error has nothing to do with 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

如果 AApply是一个有效的第一个论点。