On Tue, Jan 16, 2024 at 04:16:26PM +0100, Olaf Klinke wrote:
I don't think the number of constructors/patterns is the issue. Likely the problem lies in the fact that while ordinary constructors make up disjoint subsets of the type, with patterns you can define overlapping sets, which makes completeness checks much more complicated. Hence I believe that completeness checks in presence of patterns is equivalent to determine whether a disjunction of logic formulae, which are possibly self-referential, is a tautology. That may well be semi- decidable at best.
That seems plausible, but I think that interface stability is a more serious concern. It isn't enough to know that *as-implemented* at a given time some particular set of patterns is complete. The implementation of a set of patterns (or the underlying type) can change in a manner that changes complete <-> incomplete in either direction. Such changes are non-breaking, provided there was no "contract" (COMPLETE pragma) that the patterns are *intended* to be complete. Initially: data Foo = A | B pattern Good :: Foo; pattern Good = Foo A pattern Bad :: Foo; pattern Bad = Foo B Later: data Foo = A | B | C pattern Good :: Foo; pattern Good = Foo A pattern Bad :: Foo; pattern Bad = Foo B Later still: pattern Ugly :: Foo; pattern Ugly = Foo C All fine, if there was no expectation that "Good, Bad" is a COMPLETE set. Such completeness is a matter of interface contract (design intent), and cannot be derived. -- Viktor.