On Sun, 2024-04-28 at 22:29 +1200, Anthony Clayden wrote:

...

On Sun, 28 Apr 2024 at 07:03, Olaf Klinke wrote:

...

 I think what we see here is an instance of the fact that all checks must break down in presence of view patterns.

Sadly, yes. I'd originally tried that example with a view pattern `fromJust`, to keep closer to last week's o.p. Switching to explicit constructor didn't help. To contrast with other pattern-related styles:

* with guards, GHC can see the coverage, doesn't complain, works fine.

* with Pattern Synonyms (at least simple bidir ones) GHC complains about non-exhaustiveness, but in fact works fine.

* with PattSyns defined explicitly bidir using a View Pattern, again checks break down.

As well as the 'Boolean blindness' mentioned on that thread, there's 'Maybe blindness' or even 'algebraic blindness' https://github.com/quchen/articles/blob/master/algebraic-blindness.md (and more articles/threads via Google). Walk a data structure (could be a JSON), come back with a bunch of Maybes, now too easy to confuse which means what. The 'audit trail' has gone cold.

I believe that completeness can be decidable, if we only could restrict the functions that are allowed in view patterns to so-called perfect maps. See https://mail.haskell.org/pipermail/haskell-cafe/2024-January/136556.html The key insights are: 1. Every data type (except Integer) has only a finite number of constructors and thereby a finite number of primary patterns to match on. 2. Every pattern corresponds to a Boolean predicate on the type. Ordinary pattern matching makes this predicate decidable. 3. In every Boolean algebra, it is decidable whether the disjunction of formulas (the cases of the pattern match) is true (the match is complete). If we could restrict the functions allowed in view patterns to those functions that preserve preimages of decidable subsets [*], then the entirety of Haskell patterns could be decidable. Olaf [*] More precisely: Let f :: a -> b and let P be a pattern on b that is decidable, that is, the corresponding predicate isP :: b -> Bool is decidable. There is the predicate isP.f :: a -> Bool but it need not be deciable. If it is for every P, the function f is called perfect.