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

AApply有効な最初の引数である場合。

于 2013-04-21T19:57:58.700 に答える