Remove one instance of static state in the compilation pipeline

Source/DafnyCore/Resolver.cs

@@ -27,6 +27,7 @@ public partial class Resolver {
     ModuleSignature moduleInfo = null;
 
     public ErrorReporter Reporter => reporter;
+    public List<TypeConstraint.ErrorMsg> TypeConstraintErrorsToBeReported { get; } = new();
 
     private bool RevealedInScope(Declaration d) {
       Contract.Requires(d != null);
@@ -4590,7 +4591,7 @@ private bool ConstrainSubtypeRelation_Aux(Type super, Type sub, TypeConstraint c
         // set "headSymbolsAgree" to "false" if it's clear the head symbols couldn't be the same; "true" means they may be the same
         bool headSymbolsAgree = Type.IsHeadSupertypeOf(super.NormalizeExpand(keepConstraints), sub);
         if (!headSymbolsAgree) {
-          c.FlagAsError();
+          c.FlagAsError(this);
           return false;
         }
         // TODO: inspect type parameters in order to produce some error messages sooner
@@ -4830,7 +4831,7 @@ private bool ImposeSubtypingConstraint(Type super, Type sub, TypeConstraint.Erro
       sub = sub.NormalizeExpandKeepConstraints();
       List<int> polarities = ConstrainTypeHead_Recursive(super, ref sub);
       if (polarities == null) {
-        errorMsg.FlagAsError();
+        errorMsg.FlagAsError(this);
         return false;
       }
       bool keepConstraints = KeepConstraints(super, sub);
@@ -5524,7 +5525,7 @@ public bool Confirm(Resolver resolver, bool fullstrength, out bool convertedInto
             return false;  // to please the compiler
         }
         if (!satisfied) {
-          errorMsg.FlagAsError();
+          errorMsg.FlagAsError(resolver);
         }
         return true;  // the XConstraint has served its purpose
       }
@@ -6529,7 +6530,7 @@ void SolveAllTypeConstraints() {
           // unexpected condition -- PartiallySolveTypeConstraints is supposed to have continued until no more sub-typing constraints can be satisfied
           Contract.Assume(false, string.Format("DEBUG: Unexpectedly satisfied supertype relation ({0} :> {1}) |||| ", constraint.Super, constraint.Sub));
         } else {
-          constraint.FlagAsError();
+          constraint.FlagAsError(this);
         }
       }
       foreach (var xc in AllXConstraints) {
@@ -6540,10 +6541,10 @@ void SolveAllTypeConstraints() {
         } else if (xc.CouldBeAnything()) {
           // suppress the error message; it will later be flagged as an underspecified type
         } else {
-          xc.errorMsg.FlagAsError();
+          xc.errorMsg.FlagAsError(this);
         }
       }
-      TypeConstraint.ReportErrors(reporter);
+      TypeConstraint.ReportErrors(this, reporter);
       AllTypeConstraints.Clear();
       AllXConstraints.Clear();
     }

Source/DafnyCore/Resolver/TypeConstraint.cs

@@ -18,22 +18,21 @@
 
 namespace Microsoft.Dafny {
   public record TypeConstraint(Type Super, Type Sub, TypeConstraint.ErrorMsg ErrMsg, bool KeepConstraints) {
-    private static readonly List<ErrorMsg> ErrorsToBeReported = new List<ErrorMsg>();
-    public static void ReportErrors(ErrorReporter reporter) {
+    public static void ReportErrors(Resolver resolver, ErrorReporter reporter) {
       Contract.Requires(reporter != null);
-      foreach (var err in ErrorsToBeReported) {
+      foreach (var err in resolver.TypeConstraintErrorsToBeReported) {
         err.ReportAsError(reporter);
       }
-      ErrorsToBeReported.Clear();
+      resolver.TypeConstraintErrorsToBeReported.Clear();
     }
     public abstract class ErrorMsg {
       public abstract IToken Tok { get; }
       bool reported;
-      public void FlagAsError() {
+      public void FlagAsError(Resolver resolver) {
         if (DafnyOptions.O.TypeInferenceDebug) {
           Console.WriteLine($"DEBUG: flagging error: {ApproximateErrorMessage()}");
         }
-        TypeConstraint.ErrorsToBeReported.Add(this);
+        resolver.TypeConstraintErrorsToBeReported.Add(this);
       }
       internal void ReportAsError(ErrorReporter reporter) {
         Contract.Requires(reporter != null);
@@ -111,8 +110,8 @@ public ErrorMsgWithBase(ErrorMsg baseMsg, string msg, params object[] msgArgs) {
 
       protected override string ApproximateErrorMessage() => string.Format(Msg, MsgArgs);
     }
-    public void FlagAsError() {
-      ErrMsg.FlagAsError();
+    public void FlagAsError(Resolver resolver) {
+      ErrMsg.FlagAsError(resolver);
     }
   }
 }

docs/dev/news/3065.fix

@@ -0,0 +1 @@
+Resolved an instance in which the Dafny language server could enter a broken state.