<div dir="ltr"><div dir="ltr" class="gmail_attr">> On Sun, 28 Apr 2024 at 07:03, Olaf Klinke <<a href="mailto:olf@aatal-apotheke.de">olf@aatal-apotheke.de</a>> wrote:<br></div><br class="gmail-Apple-interchange-newline"><div dir="ltr">> 

I think what we see here is an instance of the fact that all checks<br>> must break down in presence of view patterns.<div><br></div><div>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.</div><div>To contrast with other pattern-related styles:</div><div><br></div><div>* with guards, GHC can see the coverage, doesn't complain, works fine.</div><div><br></div><div>* with Pattern Synonyms (at least simple bidir ones) GHC complains about non-exhaustiveness, but in fact works fine.</div><div><br></div><div>* with PattSyns defined explicitly bidir using a View Pattern, again checks break down.</div><div><br></div><div><br></div><div>As well as the 'Boolean blindness' mentioned on that thread, there's 'Maybe blindness'</div><div>or even 'algebraic blindness' <a href="https://github.com/quchen/articles/blob/master/algebraic-blindness.md">https://github.com/quchen/articles/blob/master/algebraic-blindness.md</a></div><div>(and more articles/threads via Google).</div><div>Walk a data structure (could be a JSON), come back with a bunch of Maybes, now too easy to confuse which means what.</div><div>The 'audit trail' has gone cold.</div><div><br></div><div><br></div><div> </div></div></div>