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??!!??

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.