Am 23.02.21 um 20:07 schrieb Richard Eisenberg:
> You might be interested in my recent paper on exactly this problem:
> how to make DatatypeContexts actually work the way you want:
> https://richarde.dev/papers/2020/partialdata/partialdata.pdf
> <https://richarde.dev/papers/2020/partialdata/partialdata.pdf>.

I think that paper is _not_ how DatatypeContexts should work -- at least for the example in that thread of `fmap` over a data structure wanting to preserve some invariant, such as unique elements.

For the matching/Provided constraints the paper at least does no harm by magically unveiling constraints via a Well-Formed-Type mechanism. It would equally do no harm by just not Providing any constraints at all.
For the building/Required constraints: it would do harm to magically unveil (for example) a computation to squish out duplicates or re-order elements by their `fmap`ed result.

The Laws for `Functor.fmap` include "preserving the structure of " the Functor. Squishing out duplicates/reordering/rebalancing breaks that.

Instead of `fmap` you should use `Foldable.foldMap :: Monoid m => (a -> m) -> t a -> m`; with `m` instance of the form `Ord b => Monoid (t b)` -- `Ord` induced from the Datatype context of `t`. Then there is a mechanism to pass in the `Ord` dictionary from outside/no need for WFT magic.

I get it that Required `Ord b` is a poor stand-in for the invariant: no duplicates; elements in ascending sequence; BST balanced. So the Monoid instance still couldn't expose the underlying data constructors.

Forcing to use `foldMap` at least puts it in the programmer's face that trying to use `fmap` is a type error standing in for law-breaking.

AntC