<html><head><meta http-equiv="Content-Type" content="text/html; charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class=""><br class=""><div><br class=""><blockquote type="cite" class=""><div class="">On Jan 5, 2022, at 9:19 PM, Anthony Clayden <<a href="mailto:anthony.d.clayden@gmail.com" class="">anthony.d.clayden@gmail.com</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><meta charset="UTF-8" class=""><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><font face="monospace" class="">So Pattern syns seem to be giving exactly the 'stupid theta' behaviour.</font></div></div></blockquote><div><br class=""></div><div>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:</div><div><br class=""></div><div>pattern Is3 :: (Num a, Eq a) => a -- only a Required constraint</div><div>pattern Is3 = ((==) 3 -> True) -- that's a view pattern</div><div><br class=""></div><div>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).</div><br class=""><blockquote type="cite" class=""><div class=""><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><font face="monospace" class=""><br class=""></font></div><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><font face="monospace" class="">The User Guide <a href="https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms" class="">https://downloads.haskell.org/~ghc/8.10.7/docs/html/users_guide/glasgow_exts.html#typing-of-pattern-synonyms</a><span class="Apple-converted-space"> </span>says</font></div><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><font face="monospace" class=""><br class=""></font></div><ul class="gmail-simple" style="font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;"><li class=""><div style="margin: 0px;" class=""><font face="monospace" class="">⟨CProv⟩ are the constraints <em class="">made available (provided)</em> by a successful pattern match.</font></div></li></ul><div style="caret-color: rgb(0, 0, 0); font-family: Helvetica; font-size: 14px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; word-spacing: 0px; -webkit-text-stroke-width: 0px; text-decoration: none;" class=""><font face="monospace" class=""><font class=""><span style="font-size: 14px;" class="">But it doesn't mean that. It's more like "</span></font><span style="font-size: 14px;" class="">⟨CProv⟩ are the constraints made available *in addition to </span><span style="font-size: 14px;" class="">⟨CReq⟩* (provided union required) by a successful pattern match."</span></font></div></div></blockquote><br class=""></div><div>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.</div><div><br class=""></div><div>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 <a href="https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst" class="">https://github.com/ghc-proposals/ghc-proposals/blob/master/proposals/0042-bidir-constr-sigs.rst</a></div><div><br class=""></div><div>Richard</div><br class=""></body></html>