[Haskell-cafe] Pattern synonyms and explicit forall.

[Kai-Oliver Prott]

Some comments in-line :)
Best,
Kai Prott

>
> > pattern Any2 :: forall . forall a. a -> Some
> We're friends here. I think I can share that my reaction was a rather 
> loud WTF??!!??
Yep, that is quite weird.
> And there's not a mention in the docos that this is even a thing. I 
> feel like dragging whoever's responsible to the headmaster's office.
> Ok that seems to work -- in the sense that pattern-matching on it 
> yields an `x` that's unusable on RHS just as much as the `Any` decl 
> with implicit `forall`, or with no type signature at all.
> What would be useful is to be able to introduce a constraint into the 
> sig, so I can do something like
> > foo (Any2 x) y = x == y
> After playing with it, all I'm getting is weird rejections.
> > pattern Any2 :: forall . forall a. () => (Eq a) => a -> Some

Your first error message seems like a case of bad error messages.
Just out of curiosity, I've tried writing the following:

pattern Refl :: forall a. forall . () => (Eq a) => Bool -> a
pattern Refl a <- (refl -> a)

refl :: Eq a => a -> Bool
refl a = a == a

This should not be accepted. Indeed I get the error message with "fewer 
arrows", although it seems like the given type signature has exactly the 
number of arrows it needs. The problem here is the misplaced constraint.
GHC checks the arity of `Eq a => Bool -> a`, which it argues has zero 
arrows (->) at the top of the type.
Note that the correct type signature would be

pattern Refl :: forall a. (Eq a) => forall . () =>  Bool -> a

> > * Pattern synonym `Any2' has one argument >    but its type 
> signature has 1 fewer arrows
> I need to put the constraints inside the scope of the `forall a.`. A 
> single `(Show a) => a -> Some` complains no instance provided.

The problem here is, that `Some` does not carry around any information 
that its argument has an `Eq` instance. It was not declared with such a 
constraint. Thus, pattern matching on `Some` cannot bring any `Eq` 
instance into scope. This is what the second error is trying to tell 
you. `Some` does not carry around enough information for `Any` to 
provide an `Eq` constraint when pattern matched.

And as a quick note: Even if we do define `Some :: Eq a => a -> Some` 
your example still does not work, since x  and y are not guaranteed to 
be of the same type. But we could write:

data Some where
   Some :: Eq a => a -> Some

pattern Any2 :: forall . forall a. (Eq a) => a -> Some
pattern Any2 a = Some a

foo :: Some -> Bool
foo (Any2 x) = x == x

>
>
>
> _______________________________________________
> Haskell-Cafe mailing list
> To (un)subscribe, modify options or view archives go to:
> http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe
> Only members subscribed via the mailman list are allowed to post.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/haskell-cafe/attachments/20210919/1804ad42/attachment.html>