
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.