Conor McBride
So, taking Void to be the colour of the empty bikeshed and
avoid :: Void -> x
suppose I define
data WrapVoid = Wrap Void
may I now write
boo :: WrapVoid -> x
with no equations? Does this cover? Or does it neglect the crucial boo (Wrap _|_) case?
It would be considered ``covered''; however you may, at your option, wish to add function body to handle (Wrap x).
What about
hoo :: Void -> Bool -> x
? Does this cover, or did I forget hoo v True and hoo v False?
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. 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. I would also be willing to consider Christian Maeder's proposal where a missing function body is never an error.