[ clean ] Removed some old, commented out code.
[ optim ] Use raiseS in construction of substitution.
[ clarify ] Some rewriting of the code for with display form generation.
[ refactor ] Express patToTerms via numberPatVars.
[ Issue 1377 ] If instance argument cannot be filled in immediately, add constraint to do it later.
[ clean ] Removed some old, commented out code.
[ big refactor ] Added reason to NotBlocked and NeutralLevel.

We now distinguish not only reduction stuck on a meta, but also on
neutral terms, by virtue of underapplication, and missing or absurd
clauses.  See Syntax.Internal.NotBlocked.
[ refactor ] Use ifBlockedType in Agda.TypeChecking.Empty.
[ refactor ] Overloaded empty for Doc and TCM Doc.
[ comment ] Remark on future use of DefaultSignatures.
[ new ] Null instance for Simplification.
[ removed ] Monoid instance for Agda.TypeChecking.Patterns.Match.Match.
[ clean ] Removed commented out and unused code.
[ NotBlocked ] new reason MissingClauses.
[ NotBlocked ] Use stuckOn to propagate NotBlocked info.
[ clean ] Removed old, commented-out code.
[ comment ] Fixed typo.
[ haddockify ] module comment of MetaVars.Occurs.
[ clarify ] overly long expression with a where definition.
[ Issue 1382 ] Improved neutrality check allows more (sound) pruning.

This solves the performance problem experienced at Issue 1382, caused
by excessive failing retries of constraint solving.
TODO: keep track of when we can actually make progress on a constraint
to speed up type checking with open metas (probably significantly).