> On Jan 5, 2022, at 9:19 PM, Anthony Clayden <anthony.d.clay...@gmail.com> > 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 Glasgow-haskell-users@haskell.org http://mail.haskell.org/cgi-bin/mailman/listinfo/glasgow-haskell-users