fix: Fix new resolution of unary minus (dafny-lang#4737)

Previously, an expression `-d` could be typed as `nat` given `d: nat`.
This caused a verification error, trying to prove that the result is a
`nat`. This PR fixes this problem in the new resolver.

Note, the old resolver still has this problem, but it's more difficult
to fix there. Thus, this PR solves the problem just for the new resolver
(and I propose we ignore the problem in the old resolver, since we'll be
switching everything over to the new resolver in the not too distant
future).


<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/Resolver/PreType/PreTypeResolve.Expressions.cs

@@ -40,7 +40,9 @@ void ResolveExpression(Expression expr, ResolutionContext resolutionContext) {
       } else if (expr is NegationExpression) {
         var e = (NegationExpression)expr;
         ResolveExpression(e.E, resolutionContext);
-        e.PreType = e.E.PreType;
+        e.PreType = CreatePreTypeProxy("result of unary -");
+        AddSubtypeConstraint(e.PreType, e.E.PreType, e.E.tok,
+          $"type of argument to unary - ({{1}}) must agree with the result type ({{0}})");
         AddConfirmation(PreTypeConstraints.CommonConfirmationBag.NumericOrBitvector, e.E.PreType, e.E.tok, "type of unary - must be of a numeric or bitvector type (instead got {0})");
         // Note, e.ResolvedExpression will be filled in during CheckTypeInference, at which time e.PreType has been determined
 

Source/DafnyCore/Resolver/PreType/PreTypeToType.cs

@@ -174,7 +174,7 @@ protected override void PostVisitOneExpression(Expression expr, IASTVisitorConte
     }
 
     // Case: fixed pre-type type
-    if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr) {
+    if (expr is LiteralExpr or ThisExpr or UnaryExpr or BinaryExpr or NegationExpression) {
       // Note, for the LiteralExpr "null", we expect to get a possibly-null type, whereas for a reference-type ThisExpr, we expect
       // to get the non-null type. The .PreType of these two distinguish between those cases, because the latter has a .PrintablePreType
       // field that gives the non-null type.

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

@@ -962,35 +962,51 @@ module StaticReceivers {
   }
 }
 
+module UnaryMinus {
+  // This modules contains some regression tests to make sure that -nat is an int, not a nat.
+  // This remains a problem in the old resolver, and was once a problem (for different reasons)
+  // in the new resolver.
 
-/****************************************************************************************
- ******** TO DO *************************************************************************
- ****************************************************************************************
+  predicate Simple(n: nat, d: nat) {
+    var x := -d; // type of x should be inferred to be int, not nat
+    n == x
+  }
 
-module StaticReceivers {
-  ghost predicate Caller0(s: seq<int>, list: LinkedList<int>)
-  {
-    s == list.StaticFunction(s) // uses "list" as an object to discard
+  function Abs(n: int): nat {
+    if n < 0 then -n else n
   }
 
-  ghost predicate Caller1(s: seq<int>)
+  predicate IsNat(n: int)
+    ensures IsNat(n) <==> 0 <= n
   {
-    s == LinkedList.StaticFunction(s) // type parameters inferred
+    AtMost(n, 0)
   }
 
-  ghost predicate Caller2(s: seq<int>)
+  predicate AtMost(n: int, d: nat)
+    requires d <= Abs(n)
+    ensures AtMost(n, d) <==> d <= n
+    decreases Abs(n) - d
   {
-    s == LinkedList<int>.StaticFunction(s)
+    n == d || (n + d != 0 && AtMost(n, d + 1))
   }
 
-  method Caller3()
+  predicate AtMost'(n: int, d: nat)
+    requires d <= Abs(n)
+    ensures AtMost'(n, d) <==> d <= n
+    decreases Abs(n) - d
   {
-    var s: seq;
-    var b := s == LinkedList<int>.StaticFunction(s);
+    if n == d then
+      true
+    else if n == -d then // the -d here should not pose any problems
+      false
+    else
+      AtMost'(n, d + 1)
   }
 
-  class LinkedList<UUU> {
-    static ghost function StaticFunction(sq: seq<UUU>): seq<UUU>
+  lemma Same(n: int, d: nat)
+    requires d <= Abs(n)
+    ensures AtMost(n, d) == AtMost'(n, d)
+  {
   }
 }
 
@@ -1032,34 +1048,4 @@ datatype Tree =
 // Dafny rejects the call to MaxF, claiming that forall t | t in ts :: default <= f(t) might not hold.  But default is 0 and f(t)
 // has type nat, so it should hold — and in fact just uncommenting the definition of fn above solves the issue… even if fn isn’t used.
  
-
-// ------------------
-// In this program, one has to write "n + d != 0" instead of "n != -d", because of a previously known problem with type inference
-
-predicate method ge0'(n: int)
-  ensures ge0'(n) <==> 0 <= n
-{
-  downup_search'(n, 0)
-}
-
-function method Abs(n: int): nat {
-  if n < 0 then -n else n
-}
-
-predicate method downup_search'(n: int, d: nat)
-  requires d <= Abs(n)
-  ensures downup_search'(n, d) <==> d <= n
-  decreases Abs(n) - d
-{
-  n == d || (n + d != 0 && downup_search'(n, d + 1))
-  /*
-  if n - d == 0 then
-    true
-  else if n + d == 0 then
-    false
-  else
-    downup_search'(n, d + 1)
-  */
-}
-
 ****************************************************************************************/

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

@@ -11,4 +11,4 @@ TypeInferenceRefresh.dfy(633,24): Error: value does not satisfy the subset const
 TypeInferenceRefresh.dfy(145,30): Error: element might not be in domain
 TypeInferenceRefresh.dfy(216,26): Error: result of operation might violate newtype constraint for 'int8'
 
-Dafny program verifier finished with 77 verified, 10 errors
+Dafny program verifier finished with 83 verified, 10 errors

docs/dev/news/4737.fix

@@ -0,0 +1 @@
+Fix resolution of unary minus in new resolver