My point is that which patterns are expected to be complete is an API design choice, subject to API stability decisions, and not just a matter of deductive reasoning.

Now I understand: Even though completeness is (provably) provable, the COMPLETE pragma can signal the library user which sets of patterns the library author intended to cover the (opaque) type, much like the MINIMAL pragma for type classes. Otherwise the library user could only know this by compiling a code snippet with -Wincomplete-uni-patterns. To further draw the parallel between MINIMAL and COMPLETE, is COMPLETE picked up by Haddock? Seems not: The Data.Sequence.Internal module contains {-# COMPLETE (:<|), Empty #-} {-# COMPLETE (:|>), Empty #-} yet the "bundled patterns" section in https://hackage.haskell.org/package/containers-0.7/docs/Data-Sequence.html#t... does not show it. If COMPLETE is indeed never picked up by Haddock, I'd say this pragma is currently fairly useless for conveying contracts. Should we open a feature request at Haddock? Olaf