Hi again [editing slightly] Russell O'Connor wrote:
Conor McBride
writes: may I now write
boo :: WrapVoid -> x hoo :: Void -> Bool -> x
with no equations? It would be considered ``covered''; however you may, at your option, wish to add function body to handle (Wrap x).
This is considered covered, but again you may, at your option, wish to add a function body to handle the hoo v True and hoo v False cases.
Hmmm. For GADTs, I fear that this coverage checking problem may be undecidable. To see why, check page 179 of my PhD thesis, although the result (due to Gerard Huet, I believe) was certainly known to Thierry Coquand in 1992. But...
Basically we considered all the cases covered if they are covered for all non-bottom values. This is (I understand) what the warning in GHC does.
...isn't (Wrap _|_) a non-bottom value? Doesn't moo (Wrap v) = True distinguish (Wrap _|_) from _|_ ? If you're willing to tolerate the need to cover these cases, coverage checking becomes decidable! Of course, it leaves you wondering what to write on the right-hand side...
I would also be willing to consider Christian Maeder's proposal where a missing function body is never an error.
I'd be more comfortable with a more explicit way to leave a stub, but I agree that there should be a way to indicate 'unfinished' which is distinct from 'defined to be _|_'. Moreover, I should very much like to have a token I can write in the place of an expression, such that on compilation, I receive a diagnostic giving me as much type information as possible about what must replace the token. When you try the old trick of making a deliberate type error to achive this effect, you often get less back than you might hope. Fine for genuine errors, but not enough to satisfy the ulterior motive. Cheers Conor