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 |