[Haskell-cafe] Spurious [-Woverlapping-patterns] -- [cont] ghc should be able to deduce correct use of partial functions

[Olaf Klinke]

On Sun, 2024-04-28 at 22:29 +1200, Anthony Clayden wrote:
> > On Sun, 28 Apr 2024 at 07:03, Olaf Klinke <olf at aatal-apotheke.de>
> > 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.