Haskell Inaccessible code bug?

问题:

Say I have the following (erroneous) code.

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 will then give me this error:

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

Isn't this error message completely wrong? The error has nothing to do with AApply.

回答1:

Isn't this error message completely wrong? The error has nothing to do with AApply.

Not completely. It's arguably a bug that you get that error message, but it's not completely off base.

Look at the whole thing together after looking at the pieces.

test (APure) a = a

says we have a function

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

Put that together with the signature

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

and unify, ignoring the type error from the first equation, the type is refined to

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

Then look at the equation

test AApply a = undefined

and see how that is inaccessible under the refined type, since

AApply :: A (A b c) c

would entail

c ~ A b c

if AApply were a valid first argument.