fix: Resolve :- expressions with void outcomes in new resolver

Source/DafnyCore/Resolver/PreType/PreTypeAdvice.cs

@@ -33,26 +33,40 @@ public Advice(PreType preType, Target advice) {
 
     public bool Apply(PreTypeResolver preTypeResolver) {
       if (PreType.Normalize() is PreTypeProxy proxy) {
-        preTypeResolver.Constraints.DebugPrint($"    DEBUG: acting on advice, setting {proxy} := {WhatString}");
-
-        Type StringDecl() {
-          var s = preTypeResolver.resolver.moduleInfo.TopLevels["string"];
-          return new UserDefinedType(s.tok, s.Name, s, new List<Type>());
-        }
-
-        var target = What switch {
-          Target.Bool => preTypeResolver.Type2PreType(Type.Bool),
-          Target.Char => preTypeResolver.Type2PreType(Type.Char),
-          Target.Int => preTypeResolver.Type2PreType(Type.Int),
-          Target.Real => preTypeResolver.Type2PreType(Type.Real),
-          Target.String => preTypeResolver.Type2PreType(StringDecl()),
-          Target.Object => preTypeResolver.Type2PreType(preTypeResolver.resolver.SystemModuleManager.ObjectQ()),
-          _ => throw new cce.UnreachableException() // unexpected case
-        };
-        proxy.Set(target);
+        ActOnAdvice(proxy, preTypeResolver);
         return true;
       }
       return false;
     }
+
+    public bool ApplyFor(PreTypeProxy proxy, PreTypeResolver preTypeResolver) {
+      if (PreType.Normalize() == proxy) {
+        ActOnAdvice(proxy, preTypeResolver);
+        return true;
+      }
+      return false;
+    }
+
+    private void ActOnAdvice(PreTypeProxy proxy, PreTypeResolver preTypeResolver) {
+      // Note, the following debug print may come out _before_ the "Type inference state ..." header, if ActOnAdvice is called
+      // during what is only a partial constraint solving round.
+      preTypeResolver.Constraints.DebugPrint($"    DEBUG: acting on advice, setting {proxy} := {WhatString}");
+
+      Type StringDecl() {
+        var s = preTypeResolver.resolver.moduleInfo.TopLevels["string"];
+        return new UserDefinedType(s.tok, s.Name, s, new List<Type>());
+      }
+
+      var target = What switch {
+        Target.Bool => preTypeResolver.Type2PreType(Type.Bool),
+        Target.Char => preTypeResolver.Type2PreType(Type.Char),
+        Target.Int => preTypeResolver.Type2PreType(Type.Int),
+        Target.Real => preTypeResolver.Type2PreType(Type.Real),
+        Target.String => preTypeResolver.Type2PreType(StringDecl()),
+        Target.Object => preTypeResolver.Type2PreType(preTypeResolver.resolver.SystemModuleManager.ObjectQ()),
+        _ => throw new cce.UnreachableException() // unexpected case
+      };
+      proxy.Set(target);
+    }
   }
 }

Source/DafnyCore/Resolver/PreType/PreTypeConstraints.cs

@@ -74,7 +74,7 @@ public DPreType ApproximateReceiverType(IToken tok, PreType preType, [CanBeNull]
     /// Expecting that "preType" is a type that does not involve traits, return that type, if possible.
     /// </summary>
     [CanBeNull]
-    public DPreType FindDefinedPreType(PreType preType) {
+    public DPreType FindDefinedPreType(PreType preType, bool applyAdvice) {
       Contract.Requires(preType != null);
 
       PartiallySolveTypeConstraints();
@@ -89,10 +89,13 @@ public DPreType FindDefinedPreType(PreType preType) {
         foreach (var super in AllSuperBounds(proxy, new HashSet<PreTypeProxy>())) {
           return super;
         }
-        return null;
+
+        if (applyAdvice) {
+          TryApplyDefaultAdviceFor(proxy);
+        }
       }
 
-      return preType as DPreType;
+      return preType.Normalize() as DPreType;
     }
 
     /// <summary>
@@ -456,6 +459,15 @@ bool TryApplyDefaultAdvice() {
       return anythingChanged;
     }
 
+    bool TryApplyDefaultAdviceFor(PreTypeProxy proxy) {
+      foreach (var advice in defaultAdvice) {
+        if (advice.ApplyFor(proxy, PreTypeResolver)) {
+          return true;
+        }
+      }
+      return false;
+    }
+
     public void AddConfirmation(CommonConfirmationBag check, PreType preType, IToken tok, string errorFormatString) {
       confirmations.Add(() => {
         if (!ConfirmConstraint(check, preType, null)) {

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

@@ -611,6 +611,7 @@ resolutionContext.CodeContext is ConstantField ||
       } else if (expr is LetOrFailExpr) {
         var e = (LetOrFailExpr)expr;
         e.ResolvedExpression = DesugarElephantExpr(e, resolutionContext);
+        ResolveExpression(e.ResolvedExpression, resolutionContext);
         e.PreType = e.ResolvedExpression.PreType;
         Constraints.AddGuardedConstraint(() => {
           if (e.Rhs.PreType.NormalizeWrtScope() is DPreType receiverPreType) {
@@ -1029,7 +1030,7 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E
     /// "receiverPreType" is an unresolved proxy type and that, after solving more type constraints, "receiverPreType"
     /// eventually gets set to a type more specific than "tentativeReceiverType".
     /// </summary>
-    (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName) {
+    (MemberDecl/*?*/, DPreType/*?*/) FindMember(IToken tok, PreType receiverPreType, string memberName, bool reportErrorOnMissingMember = true) {
       Contract.Requires(tok != null);
       Contract.Requires(receiverPreType != null);
       Contract.Requires(memberName != null);
@@ -1045,7 +1046,9 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E
         // TODO: does this case need to do something like this?  var cd = ctype?.AsTopLevelTypeWithMembersBypassInternalSynonym;
 
         if (!resolver.GetClassMembers(receiverDeclWithMembers).TryGetValue(memberName, out var member)) {
-          if (memberName == "_ctor") {
+          if (!reportErrorOnMissingMember) {
+            // don't report any error
+          } else if (memberName == "_ctor") {
             ReportError(tok, $"{receiverDecl.WhatKind} '{receiverDecl.Name}' does not have an anonymous constructor");
           } else {
             ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
@@ -1057,7 +1060,9 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E
           return (member, dReceiver);
         }
       }
-      ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+      if (reportErrorOnMissingMember) {
+        ReportError(tok, $"member '{memberName}' does not exist in {receiverDecl.WhatKind} '{receiverDecl.Name}'");
+      }
       return (null, null);
     }
 
@@ -1623,7 +1628,7 @@ ModuleResolver.MethodCallInformation ResolveApplySuffix(ApplySuffix e, Resolutio
       }
       if (r == null) {
         // e.Lhs denotes a function value, or at least it's used as if it were
-        var dp = Constraints.FindDefinedPreType(e.Lhs.PreType);
+        var dp = Constraints.FindDefinedPreType(e.Lhs.PreType, false);
         if (dp != null && DPreType.IsArrowType(dp.Decl)) {
           // e.Lhs does denote a function value
           // In the general case, we'll resolve this as an ApplyExpr, but in the more common case of the Lhs
@@ -2142,7 +2147,7 @@ private void EnsureSupportsErrorHandling(IToken tok, DPreType burritoPreType, bo
 
       var (memberIsFailure, _) = FindMember(tok, burritoPreType, "IsFailure");
       var (memberPropagate, _) = FindMember(tok, burritoPreType, "PropagateFailure");
-      var (memberExtract, _) = FindMember(tok, burritoPreType, "Extract");
+      var (memberExtract, _) = FindMember(tok, burritoPreType, "Extract", reportErrorOnMissingMember: expectExtract);
 
       if (keyword != null) {
         if (memberIsFailure == null || (memberExtract != null) != expectExtract) {

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

@@ -1007,7 +1007,7 @@ private void ResolveAssignOrReturnStmt(AssignOrReturnStmt s, ResolutionContext r
       }
       TopLevelDeclWithMembers failureSupportingType = null;
       if (firstPreType != null) {
-        Constraints.PartiallySolveTypeConstraints();
+        Constraints.FindDefinedPreType(firstPreType, true);
         failureSupportingType = (firstPreType.Normalize() as DPreType)?.Decl as TopLevelDeclWithMembers;
         if (failureSupportingType != null) {
           if (failureSupportingType.Members.Find(x => x.Name == "IsFailure") == null) {

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

@@ -1033,15 +1033,6 @@ datatype Tree =
 // 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.
 
 
-// ------------------
-// From Clement:
-
-method copy<T>(a: array<T>) returns (a': array<T>) {
-  a' := new T[a.Length](k requires k < a.Length reads a => a[k]);
-}
-
-// The lambda in a new T is supposed to take a nat, but Dafny infers k to be an int and rejects a[k]
-
 // ------------------
 // In this program, one has to write "n + d != 0" instead of "n != -d", because of a previously known problem with type inference
 
@@ -1071,14 +1062,4 @@ predicate method downup_search'(n: int, d: nat)
   */
 }
 
-// ------------------------
-// From https://github.com/dafny-lang/dafny/issues/1292:
-
-datatype List <T> = None | Cons (hd: T, tl: List<T>)
-
-method m (x: List<int>)  {
-  match x
-    case None => {assert 4 > 3;}
-    case Cons(None, t) => {assert 4 > 3;}
-}
 ****************************************************************************************/

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/Exceptions1Expressions.dfy

@@ -1,4 +1,4 @@
-// RUN: %testDafnyForEachCompiler "%s" -- --relax-definite-assignment
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s" -- --relax-definite-assignment
 include "./NatOutcomeDt.dfy"
 include "./VoidOutcomeDt.dfy"
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy

@@ -1,5 +1,5 @@
-// RUN: %exits-with 2 %dafny "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
 include "./NatOutcome.dfy"
 include "./VoidOutcome.dfy"
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/ParseErrors.dfy.refresh.expect

@@ -0,0 +1,4 @@
+ParseErrors.dfy(9,15): Error: number of lhs (2) must match number of rhs (1) for a rhs type (NatOutcome) with member Extract
+ParseErrors.dfy(10,15): Error: member IsFailure does not exist in int, in :- statement
+ParseErrors.dfy(16,4): Error: number of lhs (0) must be one less than number of rhs (2) for a rhs type (VoidOutcome) without member Extract
+3 resolution/type errors detected in ParseErrors.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy

@@ -1,5 +1,5 @@
-// RUN: %exits-with 2 %dafny "%s" /dprint:"%t.dprint" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=2 "%s"
+
 include "./NatOutcome.dfy"
 include "./VoidOutcome.dfy"
 
@@ -10,11 +10,11 @@ method TestTypecheckingInDesugaredTerm_Nat() returns (res: NatOutcome) {
 }
 
 method RedeclareVar_Nat() returns (res: NatOutcome) {
-    var a := MakeNatSuccess(42);
+    var x := MakeNatSuccess(42);
     var a :- MakeNatSuccess(43);
     var b :- MakeNatSuccess(44);
-    var b := MakeNatSuccess(45);
-    return a;
+    var y := MakeNatSuccess(45);
+    return x;
 }
 
 trait BadOutcome1 {

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.expect

@@ -1,7 +1,5 @@
 TypecheckErrors.dfy(7,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string)
 TypecheckErrors.dfy(8,28): Error: incorrect argument type for method in-parameter 'n' (expected nat, found string)
-TypecheckErrors.dfy(14,8): Error: Duplicate local-variable name: a
-TypecheckErrors.dfy(16,8): Error: Duplicate local-variable name: b
 TypecheckErrors.dfy(39,10): Error: member IsFailure does not exist in BadOutcome1?, in :- statement
 TypecheckErrors.dfy(43,10): Error: member 'PropagateFailure' does not exist in trait 'BadOutcome2'
 TypecheckErrors.dfy(43,10): Error: The right-hand side of ':-', which is of type 'BadOutcome2?', must have functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'
@@ -11,4 +9,4 @@ TypecheckErrors.dfy(71,4): Error: member IsFailure does not exist in BadVoidOutc
 TypecheckErrors.dfy(75,4): Error: member 'PropagateFailure' does not exist in trait 'BadVoidOutcome2'
 TypecheckErrors.dfy(75,4): Error: The right-hand side of ':-', which is of type 'BadVoidOutcome2?', must have functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'
 TypecheckErrors.dfy(79,4): Error: number of lhs (0) must match number of rhs (1) for a rhs type (BadVoidOutcome3?) with member Extract
-13 resolution/type errors detected in TypecheckErrors.dfy
+11 resolution/type errors detected in TypecheckErrors.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/TypecheckErrors.dfy.refresh.expect

@@ -0,0 +1,12 @@
+TypecheckErrors.dfy(7,29): Error: string literal used as if it had type int
+TypecheckErrors.dfy(8,29): Error: string literal used as if it had type int
+TypecheckErrors.dfy(39,10): Error: member IsFailure does not exist in BadOutcome1, in :- statement
+TypecheckErrors.dfy(43,10): Error: member 'PropagateFailure' does not exist in trait 'BadOutcome2'
+TypecheckErrors.dfy(43,10): Error: The right-hand side of ':-', which is of type 'BadOutcome2', must have functions 'IsFailure()', 'PropagateFailure()', and 'Extract()'
+TypecheckErrors.dfy(47,10): Error: number of lhs (1) must be one less than number of rhs (1) for a rhs type (BadOutcome3) without member Extract
+TypecheckErrors.dfy(51,23): Error: integer literal used as if it had type seq<char>
+TypecheckErrors.dfy(71,4): Error: member IsFailure does not exist in BadVoidOutcome1, in :- statement
+TypecheckErrors.dfy(75,4): Error: member 'PropagateFailure' does not exist in trait 'BadVoidOutcome2'
+TypecheckErrors.dfy(75,4): Error: The right-hand side of ':-', which is of type 'BadVoidOutcome2', must have functions 'IsFailure()' and 'PropagateFailure()', but not 'Extract()'
+TypecheckErrors.dfy(79,4): Error: number of lhs (0) must match number of rhs (1) for a rhs type (BadVoidOutcome3) with member Extract
+11 resolution/type errors detected in TypecheckErrors.dfy

Source/IntegrationTests/TestFiles/LitTests/LitTest/exceptions/VerificationErrors.dfy

@@ -1,5 +1,5 @@
-// RUN: %exits-with 4 %dafny "%s" /rprint:"%t.rprint" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s"
+
 
 include "./NatOutcome.dfy"
 include "./VoidOutcome.dfy"

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy

@@ -0,0 +1,29 @@
+// RUN: %testDafnyForEachResolver "%s"
+
+datatype Option<T> = Some(val: T) | None {
+  predicate  IsFailure() {
+    None?
+  }
+
+  function  PropagateFailure<V>(): Option<V>
+    requires None?
+  {
+    None
+  }
+
+  function Extract(): T
+    requires Some?
+  {
+    val
+  }
+}
+
+function Foo0(): Option<bool> {
+  var x: Option<bool> :- None;
+  None
+}
+
+function Foo1(): Option<bool> {
+  var x: Option<int> :- None;
+  None
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4731.dfy.expect

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 3 verified, 0 errors

docs/dev/news/4734.fix

@@ -0,0 +1 @@
+Resolve :- expressions with void outcomes in new resolver