[Haskell-cafe] Wincomplete-uni-patterns and bidirectional patterns

[Viktor Dukhovni]

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.