Make totality a warning until compiling

Now, totality errors will not prevent loading a file. This means that
features such as :missing and :addmissing can be used to fix the
problem.

However, the compiler will fail if there are totality errors, just as it
does with metavariables.
Show more errors

The totality warnings mean that elaboration doesn't stop when it sees a
totality issue. Allow both issues to be reported in this test.
Update for totality warnings

Now, totality discrepancies prevent compilation. Add partial annotations
to totality005 to make it compile.
Don't try to compile a test that doesn't have `main`

Instead, just --check it.
Update test for totality warnings

Now, all totality problems are shown. Update test accordingly.
Add totality warnings to CHANGELOG
Merge pull request #1204 from david-christiansen/totality-warning

Make totality a warning until compiling