Re: Typing of Pattern Synonyms: Required vs Provided constraints

> On Jan 5, 2022, at 9:19 PM, Anthony Clayden <[email protected]> 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.html#typing-of-pattern-synonyms <https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms> 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-bidir-constr-sigs.rst

Richard

_______________________________________________
Glasgow-haskell-users mailing list
[email protected]
http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users