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. ...
I don't think that's the only (or even the chief) reason. Wadler's response on that 1999 thread is telling
"Often, a type will make no sense without the constraints; e.g., an association list type Alist a b makes no sense unless Eq a holds. The class constraints on data declarations were a simple way for the user to ask the compiler to enforce this invariant. They have compile-time effect only, no effect whatsoever on run-time (in particular, no dictionaries should be passed). "
And yet he's somehow forgotten his own design for constraints: the _only_ way to enforce a constraint is by providing evidence in the form of a dictionary. (This is especially impossible for a constructor class where it's the (invisible) argument type to the constructor that wants the constraint.) That's why I agree with SPJ 1999 here: on a pattern match there's no mechanism to pass in a constraint (dictionary-as-evidence); and you're not doing computation in merely matching -- it doesn't even need `Eq`.
In a pattern
> baz (MkT 3 3) = "Three" -- desugars to
> baz (MkT x y) | x == fromInteger #3#, y == fromInteger #3# = "Three"
It's the appearance of the `==` and `fromInteger` that Require `(Eq a, Num a)`; I don't expect them Provided by `T`'s nor `MkT`'s Datatype context. And in general, guards can induce arbitrary computation; it's not the responsibility of the datatype declarer to anticipate that. (A Separation of Concerns argument.)
So I want constraints 'Required' for building -- that is constraints 'sighted' whether or not any computation involved; but not 'Provided' by matching -- because they're already sighted by the very fact of having built the pattern (to paraphrase SPJ1999). Thanks for pointing out that proposal. I guess it'll achieve what I want for a BST or Wadler's assoc list; would be nice to see an explicit example.
I don't want to use a GADT here, because it's the same constraint on every data constructor; and a BST recurses with the same constraint; holding identical dictionaries inside each node is just clutter. Something accessing the BST (probably) needs to bring its `Ord` dictionary with it (`elem` for example); but not necessarily (`count`, `toList` or `show`).
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,
I disagree. To "be available" requires a dictionary. A pattern synonym gets desugarred, it doesn't hold a dictionary itself. The dictionary *was* "already available" at the time of building; but it's no longer available unless the PatSyn got desugarred to a GADT with that dictionary inside. I want these PatSyns desugarred to ordinary H98 data constructors.
And I want an empty Provided `:: (Ord a) => () => a -> a -> T a` to mean nothing is Provided, not even what was Required.
AntC