There have been big improvements in the exhaustiveness checker. I know that it's not fully decideable with GADTs, so it will always have some holes, but it can handle this case now.