Re: Typing of Pattern Synonyms: Required vs Provided constraints

On Jan 5, 2022, at 9:19 PM, Anthony Clayden wrote:

So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.

In your example, yes: the Required context is "stupid" in the way that "stupid theta" is. The reason to have a Required context is if your pattern synonym does computation that requires a constraint. For example: pattern Is3 :: (Num a, Eq a) => a -- only a Required constraint pattern Is3 = ((==) 3 -> True) -- that's a view pattern In your case, there is no computation (your pattern synonym just stands for a constructor), so the Required context is unhelpful (and does indeed act just like a datatype context).

The User Guide https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts... https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts... says

⟨CProv⟩ are the constraints made available (provided) by a successful pattern match. But it doesn't mean that. It's more like "⟨CProv⟩ are the constraints made available *in addition to ⟨CReq⟩* (provided union required) by a successful pattern match."

I agree with the user guide here: the Provided constraints are made available. The Required constraint must *already* be available before the pattern match, so they are not made available *by* the match. It is true, though, that in the context of the match, both the Provided and the Required constraints must be satisfiable. To get the pre-1999 behavior, you would need a different type for a pattern synonym used as a pattern than for one used as an expression. This is the subject of the accepted-but-not-implemented https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bi... Richard