[ refactor ] packed up results of checkLeftHandSide in a datatype

This is in preparation for proper postponing of lhs checking. Still a lot
of work to be done though.
[ test ] test case for postponing lhs (disabled at the moment)
Merge remote-tracking branch 'maint/maint-2.4.0'
[ minor refactor ] mhead instead of hand-rolled head'.
[ minor refactor ] ifNotM to get shorter branch first.

Save the parentheses!
[ new ] Lenses for Constraints in state.
[ refactor ] Use lenses for constraints.
Merge branch 'maint-2.4.0'
Merge branch 'master' of github.com:agda/agda
Merge branch 'maint-2.4.0' from github
[ issue1130 ] fixed

Copy pasted telescope reordering from with-abstraction. Would have
been nice to reuse the code, but refactoring the with-checker is
non-trivial.
[ issue1130 ] updated test case
Merge remote-tracking branch 'maint/maint-2.4.0'
[ issue1207 ] test case
[ issue1207 ] fixed

Run unlevelView on levels when quoting.
[ issue1207 ] updated affected test cases

Some reflection tests cases relied on levels being quoted to 'unknown'
[ issue1207 ] release notes
[ test suit ] Removed unnecessary --injective-type-constructors option

(and some cosmetic changes)
Merge branch 'maint-2.4.0'
Merge remote-tracking branch 'upstream/master'