As I've promised in #513, I've looked at exhaustiveness checking for maps, and spent the past several weeks trying to figure out how the algorithms should work. This is like my third iteration of the implementation, the previous ones that I wrote were buggy, so there may be bugs even in this one (but I hope not).
I've tried to test it thoroughly and everything seems to work (except for two edge cases described in the commits). I've also tried to make booleans refinable (as in #513) and everything passes as well.
As I've promised in #513, I've looked at exhaustiveness checking for maps, and spent the past several weeks trying to figure out how the algorithms should work. This is like my third iteration of the implementation, the previous ones that I wrote were buggy, so there may be bugs even in this one (but I hope not).
I've tried to test it thoroughly and everything seems to work (except for two edge cases described in the commits). I've also tried to make booleans refinable (as in #513) and everything passes as well.
@erszcz @zuiderkwast What do you think?