
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