Pattern synonym existential variable confusion
|Reported by:||goldfire||Owned by:|
|Type of failure:||None/Unknown||Test Case:|
|Related Tickets:||Differential Rev(s):|
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
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
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.)