Pattern Synonyms and existentials

Learn
#1

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
#2

https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/pattern_synonyms.html

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.

2 Likes
#3

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

#4

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.

2 Likes