>
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'
(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.