Should exhaustiveness testing be on by default?

[Don Stewart]

ndmitchell:
> >> 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.
> >
> > But the primary problem with Catch is that its analysis not well
> > defined. I have no guarantee regarding the existence or not of false
> > positives or false negatives, as Catch has no underlying formal logic to
> > guide such reasoning.
> 
> If Catch says your program will not crash, then it will not crash. I
> even gave an argument for correctness in the final appendix of my
> thesis http://community.haskell.org/~ndm/thesis/ (pages 175-207). Of
> course, there are engineering concerns (perhaps your Haskell compiler
> will mis-translate the program to Core, perhaps the libraries will be
> wrong, perhaps a bit in RAM will flip due to electrical interference),
> but Catch has a formal basis.

Oh, very good! I wasn't aware you'd tried this. I imagine you do
something like:

    * identify all partial functions
    * bubble that information outwards, crossing off partial functions
      that are actually total due to tests in callers that effectively
      reduce the possible inhabitants of the types passed to the partial
      function
    * and you have some argument for why your travesal doesn't miss, or
      mislabel constraints.

Is it possible for Catch to print out its reasoning for why some
function 'f' is total, such that I could check it (with another tool)?

-- Don