Pattern synonym existential variable confusion

Ponder this:

magic :: Int -> a
magic = undefined

pattern Silly :: a -> Int
pattern Silly a <- (magic -> a)

According to the rules for implicit quantification in pattern signatures, the a in Silly's type is labeled as existential. That's sensible enough. But what surprised me is that the code is accepted, even though the pattern (magic -> a) doesn't bring any existentials into scope.

Apparently, GHC is clever enough not to produce a core-lint error, and it actually treats the variable as existential, as witnessed by

foo (Silly x) = x

which fails to compile because of skolem-escape.

If you change the pattern signature to

pattern Silly :: forall a. a -> Int

that changes a to be universal, and then foo is accepted.

I think the original program, with a inferred to be existential, should be rejected.

(The inference around universal/existential is not at issue. With a signature pattern Silly :: () => forall a. a -> Int, the program is still accepted when it shouldn't be.)

Trac metadata

Trac field	Value
Version	8.0.1
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture