Collect occurences of incomplete patterns to make them available to Haddock

I feel like this is a relatively "easy" win that we can take from Idris (without having to solve the halting problem). From the Idris documentation:

By default, functions in Idris must be covering. That is, there must be patterns which cover all possible values of the inputs types. For example, the following definition will give an error:

fromMaybe : Maybe a -> a
fromMaybe (Just x) = x

This gives an error because fromMaybe Nothing is not defined. Idris reports:

frommaybe.idr:1:1--2:1:fromMaybe is not covering. Missing cases:
        fromMaybe Nothing

You can override this with a partial annotation:

partial fromMaybe : Maybe a -> a
fromMaybe (Just x) = x

However, this is not advisable, and in general you should only do this during the initial development of a function, or during debugging. If you try to evaluate fromMaybe Nothing at run time you will get a run time error.

-- https://idris2.readthedocs.io/en/latest/tutorial/typesfuns.html#totality-and-covering

Beyond the usual benefits, it powers the documentation generation tool:

We can't yet carry proof for pre-conditions that would guarantee totality in a function that is partial, but we can certainly start by exposing this meta-data about a function: Has the function triggered a -Wincomplete-patterns warning?