Fix: Position of default argument to be at the call site, not definition

Source/DafnyCore/AST/Expressions.cs

@@ -88,15 +88,15 @@ public virtual IEnumerable<Expression> SubExpressions {
     get { yield break; }
   }
 
-  private RangeToken rangeToken;
+  private RangeToken rangeToken = null;
 
   // Contains tokens that did not make it in the AST but are part of the expression,
   // Enables ranges to be correct.
   protected IToken[] FormatTokens = null;
 
   /// Creates a token on the entire range of the expression.
   /// Used only for error reporting.
-  public RangeToken RangeToken {
+  public virtual RangeToken RangeToken {
     get {
       if (rangeToken == null) {
         if (tok is RangeToken tokAsRange) {
@@ -4087,6 +4087,8 @@ public DefaultValueExpression(IToken tok, Formal formal,
     TypeMap = typeMap;
     Type = Resolver.SubstType(formal.Type, typeMap);
   }
+
+  public override RangeToken RangeToken => new RangeToken(tok, tok);
 }
 
 /// <summary>

Source/DafnyLanguageServer.Test/Synchronization/DiagnosticsTest.cs

@@ -13,6 +13,7 @@
 using System.Linq;
 using System.Threading;
 using System.Threading.Tasks;
+using Microsoft.Boogie;
 using Microsoft.Dafny.LanguageServer.Workspace.ChangeProcessors;
 using Range = OmniSharp.Extensions.LanguageServer.Protocol.Models.Range;
 
@@ -162,6 +163,29 @@ decreases y
       await AssertNoDiagnosticsAreComing(CancellationToken);
     }
 
+    [TestMethod]
+    public async Task OpeningDocumentWithDefaultParamErrorHighlightsCallSite() {
+      var source = @"
+function test(x: int := 99): bool
+  requires x >= 100
+{
+  false
+}
+
+method A()
+{
+  var b := test();
+} ".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var diagnostics = await GetLastDiagnostics(documentItem, CancellationToken);
+      Assert.AreEqual(1, diagnostics.Length);
+      Assert.AreEqual(MessageSource.Verifier.ToString(), diagnostics[0].Source);
+      Assert.AreEqual(DiagnosticSeverity.Error, diagnostics[0].Severity);
+      Assert.AreEqual(diagnostics[0].Range.Start.Line, 8);
+      await AssertNoDiagnosticsAreComing(CancellationToken);
+    }
+
     [TestMethod]
     public async Task OpeningDocumentWithVerificationErrorDoesNotReportDiagnosticsWithVerificationErrorsIfNotVerifyOnChange() {
       var source = @"
@@ -898,7 +922,7 @@ await SetUp(new Dictionary<string, string>() {
 
     private static void AssertDiagnosticListsAreEqualBesidesMigration(Diagnostic[] expected, Diagnostic[] actual) {
       Assert.AreEqual(expected.Length, actual.Length, $"expected: {expected.Stringify()}, but was: {actual.Stringify()}");
-      foreach (var t in expected.Zip(actual)) {
+      foreach (var t in Enumerable.Zip(expected, actual)) {
         Assert.AreEqual(Relocator.OutdatedPrefix + t.First.Message, t.Second.Message, t.Second.ToString());
       }
     }

docs/dev/news/2826.fix

@@ -0,0 +1 @@
+Correct error highlighting on function called with default arguments