[ clarify ] Removed defacto identity substitution in BasicOps.give.

When meta instantiations became open terms in context (instead of
lambdas), it was not recognized that the application sequence
corresponds to the identity substitution.
https://github.com/agda/agda/commit/5e6ffac27d7f37dbe6d9701fcf0feff3d7431827
[ cosmetics ] and comments.
[ interaction ] Better error message when type checking given expr fails.
[ debug ] printing in Give and checkExpr QuestionMark.
[ Issue 1342 ] Fixed by outlawing with on module parameter.

The module free variables should stay free, so no with on them.
[ Issue 1342 ] Test cases that trigger the new error.
[ Issue 1342 ] CHANGELOG