In my particular use case this is a real option, see below.
That is indeed a detail inherent to the implementation and not to the concept of sets, which is discussed in another thread. In a way, what we are trying to do is similar: Hide implementation-level detail from the user.
The basis for my question is an XSD specification of XML structure, which can be translated mechanistically to a Haskell record type, say X. The spec for the business logic does not stop there, though. It uses schematron assertions to describe additional properties inexpressible in the XSD. Our goal is to provide smart constructors for X that have the assertions (or at least most of them) baked in.
Some of these properties mention only XML tags and their occurrence, which translates to predicates on X that mention only constructor patterns, as in Example 1. At least for this part of the spec I expect the sub-typing described above to be feasible. Some other assertions are “solvable” as in Example 2, and therefore can lead to the removal of redundant constructors.
There are, however, hundreds of assertions. This warrants a code-generator instead of manually processing them. Hence my question for theory on the subject.