[issue 938] implement recursive instance search (without termination check)
solve constraints with inert right-hand sides

Given a constraint
  _X us == D vs
where D is an inert definition (data/record/var/con) we can solve
  _X := \ xs -> D (_Ys xs)
provided that
  - us are all neutral, to ensure that _X cannot reduce to D
  - none of us have D as head
This is important for instance search where knowing the head D can
enable progress.
updated instance argument examples for recursive search
don't treat constructors as inert

not needed for instance search and it can lead to unsolved metas
(see test/succeed/InertFailure.agda)
fixed bugs in inert improvement
moved documentation from CHANGELOG to release-notes/2-4-2
Relax the no-meta constraint on recursive instance search

Instead of disallowing metas in the goal, freeze any metas in the goal.
This allows us to solve constraints like Monad (State _S) where _S is
a meta.
Merge branch 'master' into classes
don't freeze rigidly constrained metas in instance search

If there's a constraint _M us = D vs it's safe to let (recursive)
instance search instantiate _M.

This is the final piece of the puzzle to make constructor classes (Monad, Functor, etc) work properly.
don't compute instance candidates for blocked goals
removed note about meta-variables in instance goals

it no longer applies and I don't think the current behaviour needs
documenting in the release notes, since it's very low-level internal
behaviour
[ comments ] some comments on inert improvement
solving rigidly constrained metas means improveInert is not needed!

The whole point of inert improvement was to reveal the IO in
constraints like _M Nat = IO Nat, but if we allow instance search
to instantiate _M when trying the Monad IO instance it's ok if it's
not solved.
[ debug ] prettyTCM instead of show in debug output
fixed deBruijn error for dependent instance arguments
Merge branch 'classes'
[ release-notes ] changed instance search example and added some notes