Excellent bikeshedding opportunity! Frontend syntax for pattern synonym types

[Tsuyoshi Ito]

> pattern (Num a, Eq b) => P a b :: (Show a) => T a

Is “P a b” a typo for “P b”?  Otherwise I cannot see how we can read
from this signature that pattern synonym P should be used with one
argument, which is a pattern of type b.

Is there a reason why the leftmost context is the provided one and the
context after :: is the required one, rather than the other way
around?  I am asking this not because I think the other way is better,
but because to me both look equally good (or equally confusing) and I
can imagine that I will have trouble remembering which context means
which, no matter which way is chosen.

One thing I like about the above notation better than

>    pattern P ::
>      b -> T t
>      requires (Show t)
>      provides (Num t, Eq b)

or

> pattern P :: (Show t) => b -> T t => (Num t, Eq b)

is that it avoids the use of type constructor (->) because P is
neither an expression nor a pattern of type “b -> T t”.  At best, P is
a “pattern function” from a pattern of type b to a pattern of type T
t, and it has little to do with the function type “b -> T t” if I am
not mistaken.

By the way, do you allow higher-order pattern functions such as

  pattern Q p <- p "Hello"

with which Q P evaluates to

  MkT (f -> True) "Hello"

?  I guess they are not allowed, but if they are allowed, I do not
know how their types can be expressed in the syntax you proposed.

Best regards,
Tsuyoshi