On Mon, Jan 15, 2024 at 08:56:33PM +0100, Olaf Klinke wrote:
On Mon, Jan 15, 2024 at 12:00:16PM +0100, Olaf Klinke wrote:
How can I teach GHC 9 that the pattern is indeed exhaustive?
Have you tried COMPLETE pragmas?
https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/pragmas.html#complet...
Huh, of course that works. Thanks.
You're welcome.
It never occurred to me to even consider the existence of manual completeness annotation, since completeness checks work so reliably for ordinary constructors. But maybe my types weren't esoteric enough so far. Are there pattern-free cases where the GHC completeness checker is wrong? Of what computational class is the problem? Can I simulate a Turing machine by checking completeness in the presence of patterns?
I think the completeness checker works fine in all pattern-synonym-free cases, i.e. when you're using only real constructors. I don't actually understand why completeness annotations are needed for pattern synonyms. Tom