# Pattern Synonyms and existentials

So, I’ve been playing a bit with the ideas from the `trees that grow` paper, and I’ve stumbled into something I don’t quite get.

Consider the following silly existential:

``````type family SomeX (tag :: Type ) (x :: Type) :: Type
data Some tag x where
Some :: SomeX tag x -> x -> Some tag ()
``````

If we let:

``````-- Proof carries a prof for `psi a`
data Proof (psi :: k -> Constraint) (a :: k) where
P :: psi a => Proof psi a
``````

Then we can “inject” constraints by:

``````data Foo
type instance SomeX Foo x = (Proof Show x)
``````

But, if I try to make a pattern, it throws a compilation error:

``````-- Doesn't work 'x' does not unify with 'x1'
pattern SomeFoo :: (Show x) => x -> Some Foo ()
pattern SomeFoo x = Some P x
``````

I thought that this unidirectional pattern is supposed to work as an ordinary (possibly smart) constructor. If i “downgrade” it to an ordinary function, it compiles as expected:

``````someFoo :: (Show x) => x -> Some Foo ()
someFoo x = Some P x``````

Constructors don’t just require constraints like regular functions, they can also provide them. Due to this fact, the precise signature of a pattern synonym actually has two constraint arguments. Your signature is being interpreted as `Show x => () => ...`, when `() => Show x => ...` would be accepted. See above for detail.
Ohh, I thought that `() => Show x ...`, `Show x => () ...`, `(Show x, ())` were all different ways of writing the same constraint. Notational-ly (viewed as system F big lambdas), it makes sense that they aren’t. Thanks! now that section makes sense
You thought right—though `(A, B) => C` and `A => B => C` can in practice be distinguished by the compiler, they’re morally equivalent.
Unfortunately, `PatternSynonyms` is an extension, not part of Haskell’s initial design—and it shows. It makes the choice to be conservative about introducing new syntax by instead abusing what’s already available.