> Do you really want exhaustiveness, or is what you actually want safety?
I want both. Exhaustiveness checking now and forever, because it's a modular property. Safety when somebody gets around to implementing whole-program analysis in the compiler I use, when I feel like waiting around for a whole-program analysis to complete, and when I'm not making local modifications to somebody else's enormous, unsafe Haskell program.
Exhaustiveness is handy if every function is exhaustive, then it's a local property contributing to global safety. If you have functions like head floating around, then local exhaustiveness does not equal global safety. I can see why some people want it, but I'm not one of them (which in my mind makes it perfect for a flag).
Needless to say, safety analysis should identify 'assert False' and confirm at compile time that there are no assertion failures.
Catch already does assertion checking (1). Its runtime on moderate to small programs (HsColour in particular) is far less than the time GHC takes to compile them, and I still have no idea what its runtime is on enormous programs (2). An analysis can be whole program and can be slow, one does not imply the other. Thanks Neil 1) To the extent that it can.... It certainly tries to prove the assertions can't fail, and reports each one it fails to prove. 2) I think HsColour was fairly near to the largest program Yhc ever compiled...