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).
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.