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.
You are right: It is possible that the types of the bidirectional patterns do not change, but the completeness changes. In your example given I would argue the contract is broken, because the new patterns are for a different type Foo. Instead -- before: Good, Bad are complete data Foo = A | B pattern Good :: Foo pattern Good = A pattern Bad :: Foo pattern Bad = B -- after: Good, Bad are incomplete -- Foo, Good as before pattern Bad = A Here neither the definition of Foo nor the types of Good or Bad have changed, but completeness has. Here is why I think that completeness checks even with pattern synonyms should work and we would not need COMPLETE pragmas. The algorithm for a set of patterns of type T is: 1. Construct a Stone [1] space X from the given type T. (Often X = T) 2. Translate each pattern to a clopen of that Stone space 3. Use Stone duality to translate coverage into a Zeroth-order logic problem, which is decidable. Let us define an equivalence relation on the elements of a type. Say x~y whenever there is no pattern that can distinguish x and y by pattern match. Notice that any pattern partitions the set of equivalence classes into two disjoint subsets, think of isJust or isNothing. In general, given a pattern Pat for type T, write isPat :: T -> Bool isPat x = case x of Pat -> True _ -> False For functions types, there is only one equivalence class, because there is only one way to pattern-match a function. Observe that two elements can be distinguished by a set of patterns if and only if there is one element in the pattern set that already distinguishes them. Do pattern synonyms refine the equivalence relation induced by ordinary constructors? No. Consider type Clopen x = x -> Bool data C = L C | R C cl :: Clopen C cl = isL . shift where isL :: Clopen C -- a pattern isL (L c) = True isL (R c) = False shift :: C -> C shift (L c) = c shift (R c) = c Can one define a single pattern synonym pattern CL :: C -> C such that CL matches c if any only if cl c == True? Note that cl is the disjunction of two ordinary patterns, namely L (L _) R (L _) CL morally should be the pattern (_(L _)) but that is not valid pattern syntax. Indeed with synonyms we can define the CL pattern: {-# LANGUAGE PatternSynonyms, ViewPatterns #-} swap :: C -> C swap (L (R c)) = R (L c) swap (R (L c)) = L (R c) swap c = c pattern CL c <- (swap -> L c) isCL :: Clopen C isCL c = case c of CL _ -> True _ -> False Now, at least as long as a type X has only a finite number of constructors (integers with numeric literals being an exception), the type Clopen X defines a Stone space, a compact zero-dimensional Hausdorff space. By Stone duality these are dually equivalent to Boolean algebras. The duality translates the problem of coverage by clopens to the problem of proving that the disjunction of some elements in the algebra is the top element 'True'. Since Zeroth-order logic is decidable, completness checks even in the presence of pattern synonyms should be, too. For the countably infinite type C above, one can use the Select monad [2] to decide whether any number of clopens covers the space, pattern or not. For numeric literal patterns we can safely say that any set of patterns is not covering unless a wildcard pattern is among them. Olaf [1] https://en.wikipedia.org/wiki/Stone_space [2] https://hackage.haskell.org/package/transformers-0.6.1.1/docs/Control-Monad-... see also https://hackage.haskell.org/package/infinite-search