This PR enhances the error message, giving more context. Fixes #5262

For example, in the context of a method where `x` is a field,

    x := 5;
    f := () => if 5 / x == 1 then 2 else 3;
                      ^ Error here

Instead of saying 

git-issue-405.dfy(19,22): Error: insufficient reads clause to read field

the new message is more helpful:

git-issue-405.dfy(19,22): Error: insufficient reads clause to read
field;
Consider extracting this.x to a local variable, or adding 'reads this'
    in the enclosing lambda specification for resolution

The first part of this message is added only for lambda expressions, the
second part is always present for scope tolerating a reads clause. For
scopes such as functions or methods, where the reads clause can
sometimes be more fine-grained, the hint `or 'reads this`x'` is added
for discoverability.
For scopes without a possible resolution, the following error message is
now emitted:

    Error: insufficient reads clause to read field; Mutable fields
    cannot be accessed within certain scopes, such as default
    values or the right-hand side of constants

For a function by method, the scope is the function and not the method
body.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>