Test ResolutionErrors[45679] with new resolver (#5333)

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

``` dafny
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.


<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>

Source/DafnyCore/AST/Expressions/Conditional/TernaryExpr.cs

@@ -8,8 +8,7 @@ public class TernaryExpr : Expression, ICloneable<TernaryExpr> {
  public readonly Expression E0;
  public readonly Expression E1;
  public readonly Expression E2;
- public enum Opcode { /*SOON: IfOp,*/ PrefixEqOp, PrefixNeqOp }
- public static readonly bool PrefixEqUsesNat = false; // "k" is either a "nat" or an "ORDINAL"
+ public enum Opcode { PrefixEqOp, PrefixNeqOp }
 
  public TernaryExpr(Cloner cloner, TernaryExpr original) : base(cloner, original) {
  Op = original.Op;

Source/DafnyCore/Resolver/NameResolutionAndTypeInference/XConstraint.cs

@@ -141,19 +141,11 @@ public class XConstraint {
  break;
  case "IntOrORDINAL":
  if (!(t is TypeProxy)) {
- if (TernaryExpr.PrefixEqUsesNat) {
- satisfied = t.IsNumericBased(Type.NumericPersuasion.Int);
- } else {
- satisfied = t.IsNumericBased(Type.NumericPersuasion.Int) || t.IsBigOrdinalType;
- }
+ satisfied = t.IsNumericBased(Type.NumericPersuasion.Int) || t.IsBigOrdinalType;
  } else if (fullstrength) {
  var proxy = (TypeProxy)t;
- if (TernaryExpr.PrefixEqUsesNat) {
- resolver.AssignProxyAndHandleItsConstraints(proxy, Type.Int);
- } else {
- // let's choose ORDINAL over int
- resolver.AssignProxyAndHandleItsConstraints(proxy, Type.BigOrdinal);
- }
+ // let's choose ORDINAL over int
+ resolver.AssignProxyAndHandleItsConstraints(proxy, Type.BigOrdinal);
  convertedIntoOtherTypeConstraints = true;
  satisfied = true;
  } else {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -703,7 +703,7 @@ public partial class PreTypeResolver {
  }
 
  private void SetupCollectionProducingExpr(string typeName, string exprKind, Expression expr, PreType elementPreType, PreType valuePreType = null) {
- expr.PreType = CreatePreTypeProxy($"{exprKind}");
+ expr.PreType = CreatePreTypeProxy(exprKind);
 
  var arguments = valuePreType == null ? new List<PreType>() { elementPreType } : new List<PreType>() { elementPreType, valuePreType };
  var defaultType = new DPreType(BuiltInTypeDecl(typeName), arguments);
@@ -1071,9 +1071,9 @@ public partial class PreTypeResolver {
  }
  }
  if (members == null) {
- ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+ ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKindAndName}");
  } else if (!members.TryGetValue(nameToBeRevealed, out var member)) {
- ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+ ReportError(tok, $"member '{nameToBeRevealed}' does not exist in {receiverDecl.WhatKindAndName}");
  } else if (member is not (ConstantField or Function)) {
  Contract.Assert(!member.IsOpaque);
  ReportError(tok,
@@ -1082,12 +1082,12 @@ public partial class PreTypeResolver {
  ReportError(tok, $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it is not opaque");
  } else if (member is Function { Body: null }) {
  ReportError(tok,
- $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+ $"{member.WhatKind} '{nameToBeRevealed}' cannot be revealed, because it has no body in {receiverDecl.WhatKindAndName}");
  } else {
  ReportError(tok, $"cannot reveal '{nameToBeRevealed}'");
  }
  } else {
- ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+ ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKindAndName}");
  }
  }
 

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -1008,6 +1008,7 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  } else {
  if (initialResolutionPass == dd.Var.Type is TypeProxy) {
  scope.PushMarker();
+ scope.AllowInstance = false;
  ScopePushExpectSuccess(dd.Var, dd.WhatKind + " variable", false);
  ResolveExpression(dd.Constraint, new ResolutionContext(new CodeContextWrapper(dd, true), false));
  ConstrainTypeExprBool(dd.Constraint, dd.WhatKind + " constraint must be of type bool (instead got {0})");
@@ -1020,7 +1021,10 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
 
  if (!initialResolutionPass && dd.Witness != null) {
  var codeContext = new CodeContextWrapper(dd, dd.WitnessKind == SubsetTypeDecl.WKind.Ghost);
+ scope.PushMarker();
+ scope.AllowInstance = false;
  ResolveExpression(dd.Witness, new ResolutionContext(codeContext, false));
+ scope.PopMarker();
  AddSubtypeConstraint(dd.Var.PreType, dd.Witness.PreType, dd.Witness.tok, "witness expression must have type '{0}' (got '{1}')");
  Constraints.SolveAllTypeConstraints($"{dd.WhatKind} '{dd.Name}' witness");
  }
@@ -1033,7 +1037,12 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  void ResolveConstRHS(ConstantField cfield, bool initialResolutionPass) {
  if (cfield.Rhs != null && initialResolutionPass == cfield.Type is TypeProxy) {
  var opts = new ResolutionContext(cfield, false);
+ scope.PushMarker();
+ if (cfield.IsStatic) {
+ scope.AllowInstance = false;
+ }
  ResolveExpression(cfield.Rhs, opts);
+ scope.PopMarker();
  AddSubtypeConstraint(cfield.PreType, cfield.Rhs.PreType, cfield.Tok, "RHS (of type {1}) not assignable to LHS (of type {0})");
  Constraints.SolveAllTypeConstraints($"{cfield.WhatKind} '{cfield.Name}' constraint");
  }
@@ -1086,7 +1095,12 @@ private PreTypeResolver(ModuleResolver resolver, PreTypeInferenceModuleState pre
  Contract.Requires(currentClass != null);
 
  if (member is ConstantField cfield) {
+ scope.PushMarker();
+ if (cfield.IsStatic) {
+ scope.AllowInstance = false;
+ }
  ResolveAttributes(member, new ResolutionContext(new NoContext(currentClass.EnclosingModuleDefinition), false), true);
+ scope.PopMarker();
  ResolveConstRHS(cfield, false);
 
  } else if (member is Field) {

Source/DafnyCore/Verifier/BoogieGenerator.ExpressionTranslator.cs

@@ -1250,7 +1250,7 @@ public ExpressionTranslator(ExpressionTranslator etran, Boogie.Expr heap)
  case TernaryExpr ternaryExpr: {
  var e = ternaryExpr;
  var e0 = TrExpr(e.E0);
- if (!TernaryExpr.PrefixEqUsesNat && !e.E0.Type.IsBigOrdinalType) {
+ if (!e.E0.Type.IsBigOrdinalType) {
  e0 = FunctionCall(e0.tok, "ORD#FromNat", predef.BigOrdinalType, e0);
  }
  var e1 = TrExpr(e.E1);

Source/DafnyCore/Verifier/BoogieGenerator.SplitExpr.cs

@@ -173,7 +173,7 @@ public partial class BoogieGenerator {
  // Note: First off, (*) is used only when ORDINAL is involved. Moreover, if there's an error among the first checked
  // conditions, it seems confusing to get yet another error message. Therefore, we add a middle disjunct to (*), namely
  // the conjunction of all the previous RHSs.
- var kAsORD = !e.E0.Type.IsBigOrdinalType && !TernaryExpr.PrefixEqUsesNat ? FunctionCall(k.tok, "ORD#FromNat", Bpl.Type.Int, k) : k;
+ var kAsORD = !e.E0.Type.IsBigOrdinalType ? FunctionCall(k.tok, "ORD#FromNat", Bpl.Type.Int, k) : k;
  var prefixEqK = CoEqualCall(codecl, e1type.TypeArgs, e2type.TypeArgs, kAsORD, etran.layerInterCluster.LayerN((int)FuelSetting.FuelAmount.HIGH), A, B); // FunctionCall(expr.tok, CoPrefixName(codecl, 1), Bpl.Type.Bool, k, A, B);
  Bpl.Expr kHasSuccessor, kMinusOne;
  if (e.E0.Type.IsBigOrdinalType) {
@@ -182,9 +182,7 @@ public partial class BoogieGenerator {
  } else {
  kHasSuccessor = Bpl.Expr.Lt(Bpl.Expr.Literal(0), k);
  kMinusOne = Bpl.Expr.Sub(k, Bpl.Expr.Literal(1));
- if (!TernaryExpr.PrefixEqUsesNat) {
- kMinusOne = FunctionCall(k.tok, "ORD#FromNat", Bpl.Type.Int, kMinusOne);
- }
+ kMinusOne = FunctionCall(k.tok, "ORD#FromNat", Bpl.Type.Int, kMinusOne);
  }
  // for the inlining of the definition of prefix equality, translate the two main equality operands arguments with a higher offset (to obtain #2 functions)
  var etran2 = etran.LayerOffset(1);

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy

@@ -642,3 +642,57 @@ module SubSequences {
  r := arr[..];
  }
 }
+
+module TLAStyleOperators {
+ newtype MyBool = bool
+
+ function A(): MyBool {
+ && true
+ }
+
+ function B(b: MyBool): MyBool {
+ && b
+ }
+
+ function C(b: bool): MyBool {
+ && b // error: got bool, expected MyBool
+ }
+
+ function D(x: int): MyBool {
+ && x // error: got int, expected MyBool
+ }
+
+ function E(): MyBool {
+ && true
+ && false
+ }
+
+ function F(b: bool): MyBool {
+ && true
+ && b // error: got bool, expected MyBool
+ }
+
+ predicate P(b: MyBool) {
+ b // error: got bool, expected MyBool
+ }
+
+ predicate Q(b: MyBool) {
+ && b // error: got bool, expected MyBool
+ }
+
+ predicate R(b: MyBool) {
+ && b && b // error: got bool, expected MyBool
+ }
+
+ predicate S(b: MyBool) {
+ && b as bool
+ }
+
+ predicate T(b: MyBool) {
+ && (b as bool) // same as in S
+ }
+
+ predicate U(b: MyBool) {
+ (&& b) as bool
+ }
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/GeneralNewtypeResolution.dfy.expect

@@ -134,7 +134,16 @@ GeneralNewtypeResolution.dfy(621,10): Error: resulting sequence (seq<?94>) type
 GeneralNewtypeResolution.dfy(622,10): Error: resulting sequence (seq<?95>) type does not agree with source sequence type (MySequence)
 GeneralNewtypeResolution.dfy(623,10): Error: resulting sequence (seq<?96>) type does not agree with source sequence type (MySequence)
 GeneralNewtypeResolution.dfy(624,10): Error: resulting sequence (seq<?97>) type does not agree with source sequence type (MySequence)
-136 resolution/type errors detected in GeneralNewtypeResolution.dfy
+GeneralNewtypeResolution.dfy(647,10): Error: a newtype ('MyBool') must be based on some numeric type (got bool)
+GeneralNewtypeResolution.dfy(657,11): Error: Function body type mismatch (expected MyBool, got bool)
+GeneralNewtypeResolution.dfy(661,11): Error: Function body type mismatch (expected MyBool, got int)
+GeneralNewtypeResolution.dfy(662,4): Error: boolean literal used as if it had type int
+GeneralNewtypeResolution.dfy(662,4): Error: type of && must be a boolean (got int)
+GeneralNewtypeResolution.dfy(670,11): Error: Function body type mismatch (expected MyBool, got bool)
+GeneralNewtypeResolution.dfy(675,12): Error: Function body type mismatch (expected bool, got MyBool)
+GeneralNewtypeResolution.dfy(679,12): Error: Function body type mismatch (expected bool, got MyBool)
+GeneralNewtypeResolution.dfy(683,12): Error: Function body type mismatch (expected bool, got MyBool)
+145 resolution/type errors detected in GeneralNewtypeResolution.dfy
 GeneralNewtypeResolution.dfy(34,10): Error: a newtype ('MyOrdinal') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got ORDINAL)
 GeneralNewtypeResolution.dfy(40,10): Error: a newtype ('MyObject') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got object)
 GeneralNewtypeResolution.dfy(41,10): Error: a newtype ('MyTrait') must be based on some non-reference, non-trait, non-arrow, non-ORDINAL, non-datatype type (got Trait)
@@ -245,4 +254,12 @@ GeneralNewtypeResolution.dfy(621,10): Error: resulting sequence (seq<?94>) type
 GeneralNewtypeResolution.dfy(622,10): Error: resulting sequence (seq<?95>) type does not agree with source sequence type (MySequence)
 GeneralNewtypeResolution.dfy(623,10): Error: resulting sequence (seq<?96>) type does not agree with source sequence type (MySequence)
 GeneralNewtypeResolution.dfy(624,10): Error: resulting sequence (seq<?97>) type does not agree with source sequence type (MySequence)
-109 resolution/type errors detected in GeneralNewtypeResolution.dfy
+GeneralNewtypeResolution.dfy(657,11): Error: Function body type mismatch (expected MyBool, got bool)
+GeneralNewtypeResolution.dfy(661,11): Error: Function body type mismatch (expected MyBool, got int)
+GeneralNewtypeResolution.dfy(662,4): Error: boolean literal used as if it had type int
+GeneralNewtypeResolution.dfy(662,4): Error: type of && must be a boolean (got int)
+GeneralNewtypeResolution.dfy(670,11): Error: Function body type mismatch (expected MyBool, got bool)
+GeneralNewtypeResolution.dfy(675,12): Error: Function body type mismatch (expected bool, got MyBool)
+GeneralNewtypeResolution.dfy(679,12): Error: Function body type mismatch (expected bool, got MyBool)
+GeneralNewtypeResolution.dfy(683,12): Error: Function body type mismatch (expected bool, got MyBool)
+117 resolution/type errors detected in GeneralNewtypeResolution.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/ResolutionErrors4.dfy

@@ -1,5 +1,5 @@
-// RUN: %exits-with 2 %verify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
 
 // ------------------- infer array types for Indexable and MultiIndexable XConstraints ----------
 // ------------------- using weaker subtyping constraints ----------
@@ -15,7 +15,8 @@ module AdvancedIndexableInference {
  var xx := c[25].x;
  } else if * {
  var c := d;
- var xx := c[25..50][10].x;
+ var xx := c[25..50][10].x; // Unfortunately, this gives an error with the new resolver, because it doesn't see to get the element type of c[25..50]
+ // The best way to improve this is to make name lookups be GuardedConstraints in the resolver, so this may change in the future.
  } else if * {
  var c := e;
  var xx := c[25].x;
@@ -25,7 +26,6 @@ module AdvancedIndexableInference {
  }
  }
 }
-
 // --------------------------
 
 module TypeConversions {
@@ -35,10 +35,10 @@ module TypeConversions {
  method M() returns (x: int, n: nat, o: object, j: J, c: C) {
  n := x as nat; // yes, this is allowed now
  o := j;
- j := o; // OK for type resolution, but must be proved
+ j := o; // OK for type resolution, but must be proved (new resolver: error, because it requires an explicit cast here)
  j := o as J; // yes, this is allowed now
  j := c;
- c := j; // OK for type resolution, but must be proved
+ c := j; // OK for type resolution, but must be proved (new resolver: error, because it requires an explicit cast here)
  c := j as C; // yes, this is allowed now
  var oo := o as realint; // error: there's no such type as "realint" (this once used to crash Dafny)
  }