Pattern synonym constraints :: Ord a => () => ...

[Anthony Clayden]

On Wed, 6 Oct 2021 at 21:24, Simon Peyton Jones <simonpj at microsoft.com>
wrote:

>
>
> I suggest the User Guide needs an example where a constraint needed for
> matching (presumably via a View pattern) is not amongst the
> constraints carried inside the data constructor, nor amongst those needed
> for building. Then the limitations in the current design would be more
> apparent for users.
>
>
>
> The user manual
> <https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pattern_synonyms.html?highlight=pattern%20syn#typing-of-pattern-synonyms>
> does already speak about the type of a builder, here:
>
...
   How could we make that clearer?


This point in that section of the Guide is wrong/misleading:




   - ⟨CReq⟩ are the constraints *required* to match the pattern.

<CReq> must be the union of the constraints required to match the pattern,
_plus_ required to build with the pattern -- if it is bidirectional.


Then thank you Simon, but it's the type of the _matcher_ that's
problematic. The only mechanism for getting the constraints needed for
building is by polluting the constraints needed for matching. Here's a
(crude, daft) example, using guards to 'raise' a
required-for-failing-to-build that isn't required-for-successful-building
nor for-matching

>    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).
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20211006/f272b35d/attachment-0001.html>