Allow static reveal of instance function in new resolver

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

@@ -1085,8 +1085,11 @@ private void ConstrainOperandTypes(IToken tok, string opString, Expression e0, E
     /// <param name="allowMethodCall">If false, generates an error if the name denotes a method. If true and the name denotes a method, returns
     /// a MemberSelectExpr whose .Member is a Method.</param>
     /// <param name="complain"></param>
+    /// <param name="specialOpaqueHackAllowance">If "true", treats an expression "f" where "f" is an instance function, as "this.f", even though
+    /// there is no "this" in scope. This seems like a terrible hack, because it breaks scope invariants about the AST. But, for now, it's here
+    /// to mimic what the legacy resolver does.</param>
     Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<ActualBinding> args,
-      ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true) {
+      ResolutionContext resolutionContext, bool allowMethodCall, bool complain = true, bool specialOpaqueHackAllowance = false) {
       Contract.Requires(expr != null);
       Contract.Requires(!expr.WasResolved());
       Contract.Requires(resolutionContext != null);
@@ -1135,7 +1138,7 @@ Expression ResolveNameSegment(NameSegment expr, bool isLastNameSegment, List<Act
             (TopLevelDeclWithMembers)member.EnclosingClass, true);
           receiver.PreType = Type2PreType(receiver.Type);
         } else {
-          if (!scope.AllowInstance) {
+          if (!scope.AllowInstance && !specialOpaqueHackAllowance) {
             if (complain) {
               ReportError(expr.tok, "'this' is not allowed in a 'static' context"); //TODO: Rephrase this
             } else {

Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs

@@ -868,7 +868,13 @@ void ResolveAttributes(IAttributeBearingDeclaration attributeHost, ResolutionCon
 #endif
         }
         if (attr.Args != null) {
-          attr.Args.ForEach(arg => ResolveExpression(arg, opts));
+          foreach (var arg in attr.Args) {
+            if (Attributes.Contains(attributeHost.Attributes, "opaque_reveal") && attr.Name is "revealedFunction" && arg is NameSegment nameSegment) {
+              ResolveNameSegment(nameSegment, true, null, opts, false, specialOpaqueHackAllowance: true);
+            } else {
+              ResolveExpression(arg, opts);
+            }
+          }
           if (solveConstraints) {
             Constraints.SolveAllTypeConstraints($"attribute of {attributeHost.ToString()}");
           }

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

@@ -1,5 +1,5 @@
-// RUN: %dafny /compile:0 "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
+// RUN: %testDafnyForEachResolver "%s"
+
 
 module M1 {
   class C {
@@ -8,4 +8,4 @@ module M1 {
 }
 
 module M2 refines M1 {
-}
+}

docs/dev/news/4733.fix

@@ -0,0 +1 @@
+The new type checker now also supports static reveals for instance functions