From 324cfdf1acdb47feba24052d70c0d86c5f5443d2 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Tue, 31 Oct 2023 18:20:50 -0700
Subject: [PATCH 1/3] Hack instance-reveal-in-static-context like the legacy
 resolver does

A test for this is in `git-issues/git-issue-4315.dfy`
---
 .../Resolver/PreType/PreTypeResolve.Expressions.cs        | 7 +++++--
 Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs       | 8 +++++++-
 2 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
index e7207241f5e..5ab41a4c3ae 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs
+++ b/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 {
diff --git a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs b/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
index 2028e9483fe..774e4f4382c 100644
--- a/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs
+++ b/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()}");
           }

From 50963aba1f5ae72fd70dad2c4f53d536c93cefb2 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Wed, 1 Nov 2023 11:56:27 -0700
Subject: [PATCH 2/3] Run git-issue-4315.dfy also with new resolver

---
 .../LitTests/LitTest/git-issues/git-issue-4315.dfy          | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4315.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4315.dfy
index 781be3d319f..e4363cc3b42 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4315.dfy
+++ b/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 {
-}
\ No newline at end of file
+}

From 7abaf5c658c358812252292300ff3d16cd850e88 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@amazon.com>
Date: Thu, 2 Nov 2023 13:35:38 -0700
Subject: [PATCH 3/3] Add release notes

---
 docs/dev/news/4733.fix | 1 +
 1 file changed, 1 insertion(+)
 create mode 100644 docs/dev/news/4733.fix

diff --git a/docs/dev/news/4733.fix b/docs/dev/news/4733.fix
new file mode 100644
index 00000000000..22691509665
--- /dev/null
+++ b/docs/dev/news/4733.fix
@@ -0,0 +1 @@
+The new type checker now also supports static reveals for instance functions