<CReq> must be the union of the constraints required to match the pattern, _plus_ required to build with the pattern -- if it is bidirectional.
I think that is confusing too! How about this:
* ⟨CReq⟩ are the constraints required to match the pattern, in a pattern match.
* ⟨CProv⟩ are the constraints made available (provided) by a successful pattern match.
* <CReq> and <CProv> are both required when P is used as a constructor in an expression.
That makes the constructor form explicit.
The only mechanism for getting the constraints needed for building is by polluting the constraints needed for matching.
Yes I agree that’s bad. It is acknowledge as such in the paper, and is the subject of accepted proposal #42.
Simon
PS: I am leaving Microsoft at the end of November 2021, at which point simonpj@microsoft.commailto:simonpj@microsoft.com will cease to work. Use simon.peytonjones@gmail.commailto:simon.peytonjones@gmail.com instead. (For now, it just forwards to simonpj@microsoft.com.)
From: Anthony Clayden
pattern TwoNode :: (Show a, Ord a) => () => a -> a -> Tree a -- GHC insists on both constraints as Req'd
pattern TwoNode x y <- Node Empty x (Leaf y) where TwoNode x y | x > y = Node Empty x (Leaf y) | otherwise = error (show x ++ " not greater " ++ show y) To quote you from May 1999
But when you take a constructor *apart*, the invariant must hold
by construction: you couldn't have built the thing you are taking
apart unless invariant held. So enforcing the invariant again is
redundant; and in addition it pollutes the type of selectors.
`Show a` must have "held by construction" of the `Node`. But the PatSyn's constraints are requiring more than that was true in some distant line of code: it wants evidence in the form of a dictionary at the point of deconstructing; since the build was successful, I ipso facto don't want to `show` anything in consuming it. An `instance Foldable Tree` has no mechanism to pass in any such dictionaries (which'll anyway be redundant, as you say).