Test ResolutionErrors[45679] with new resolver

[RustanLeino]

This PR changes the remaining 5 of the 10 dafny0/ResolutionErrors*.dfy tests so that they test not only the legacy resolver, but also the resolver refresh.

• fix: Remove this from the scope when resolving static const fields
• fix: Remove this from the scope when resolving type constraints and type witnesses
• Adjust tests and expected output for dafny0/ResolutionErrors[45679].dfy
• Add test for for unary TLA-style expressions (these worked, but did not have specific tests)
• chore: Remove TernaryExpr.PrefixEqUsesNat, which wasn't needed

Regression

The one place where the new type inference was not able to do as well as the old is the code snippet

var c := d;
var xx := c[25..50][10].x;

from dafny0/ResolutionErrors4.dfy. Here, the new resolver does not thread the element type of d through the array-to-sequence conversion c[25..50], and therefore the .x gives an error.

The workaround is to declare the type of c explicitly in the code.

I don't see a quick fix for this in the type inference. A good improvement, which I believe would also fix this problem, is to do member resolution (like .x) lazily instead of eagerly. This would allow the type-inference machinery to start making some decisions, which will lead to it figuring out a type for c, after which types for the other expressions, including the .x, can be inferred. I would love to see this improvement in the type inference, and the new resolver has "guarded constraints" that exist in order to lazy inference. However, such a change will take some effort, because the methods that currently try to do member lookup too easily generate errors (rather than saying "please try again later"). Such a change is out of scope for this PR.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[atomb]

I like that the bug fixes ultimately feel like simplifications.

The couple of reductions in type inference power are slightly unfortunate, but the workarounds seem like better style to me, so I'm not really worried about them.