Another "item with the same key has already been added" instance

[atomb]

Dafny version

3.9.1 (and 35a0478)

Code to produce this issue

Load this file in the IDE.

Command to run and resulting output

In the "Dafny Language Server" log pane, you'll see something like:

[Error - 1:21:29 PM] Request textDocument/codeAction failed.
  Message: Internal Error - System.ArgumentException: An item with the same key has already been added. Key: Microsoft.Dafny.DatatypeUpdateExpr
   at System.Collections.Generic.Dictionary`2.TryInsert(TKey key, TValue value, InsertionBehavior behavior)
   at System.Linq.Enumerable.ToDictionary[TSource,TKey,TElement](List`1 source, Func`2 keySelector, Func`2 elementSelector, IEqualityComparer`1 comparer)
   at Microsoft.Dafny.LanguageServer.Workspace.SymbolTable..ctor(Document document, IReadOnlyList`1 usages)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.SymbolTableFactory.CreateFrom(Program program, Document document, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass12_0.<<LoadAsync>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadAsync(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.Compilation.ResolveAsync()
   at Microsoft.Dafny.LanguageServer.Workspace.DocumentManager.GetLastDocumentAsync()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyCodeActionHandler.Handle(CodeActionParams request, CancellationToken cancellationToken)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.SemanticTokensDeltaPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.LanguageServer.Server.Pipelines.ResolveCommandPipeline`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPreProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestPostProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at MediatR.Pipeline.RequestExceptionActionProcessorBehavior`2.Handle(TRequest request, CancellationToken cancellationToken, RequestHandlerDelegate`1 next)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.<RouteRequest>g__InnerRoute|7_0(IServiceScopeFactory serviceScopeFactory, Request request, TDescriptor descriptor, Object params, CancellationToken token, ILogger logger)
   at OmniSharp.Extensions.JsonRpc.RequestRouterBase`1.RouteRequest(IRequestDescriptor`1 descriptors, Request request, CancellationToken token)
   at OmniSharp.Extensions.JsonRpc.DefaultRequestInvoker.<>c__DisplayClass10_0.<<RouteRequest>b__5>d.MoveNext()
  Code: -32603 

What happened?

This is the same exception as in #1790, #2951, and #3105, but thrown from a different location, so I don't think it's the same issue.

What type of operating system are you experiencing the problem on?

Mac

[GenericMonkey]

FWIW, I found another instance with a similar callstack (via System.Linq.Enumerable.ToDictionary method), and was able to narrow down to a pretty small repro: seems related to update syntax that doesn't specify a variant.

datatype Test =
    | A(field: int)
    | B(field: int)


predicate updateTest(test: Test, test': Test)
{
    test' == test.(field := 1)
}

More Stack info:

[Error - 12:07:17 AM] Request textDocument/codeAction failed.
  Message: Internal Error - System.ArgumentException: An item with the same key has already been added. Key: Microsoft.Dafny.DatatypeUpdateExpr
   at System.Collections.Generic.Dictionary`2.TryInsert(TKey key, TValue value, InsertionBehavior behavior)
   at System.Linq.Enumerable.ToDictionary[TSource,TKey,TElement](List`1 source, Func`2 keySelector, Func`2 elementSelector, IEqualityComparer`1 comparer)
   at System.Linq.Enumerable.ToDictionary[TSource,TKey,TElement](IEnumerable`1 source, Func`2 keySelector, Func`2 elementSelector, IEqualityComparer`1 comparer)
   at Microsoft.Dafny.LanguageServer.Workspace.SymbolTable..ctor(Document document, IReadOnlyList`1 usages)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.SymbolTableFactory.CreateFrom(Program program, Document document, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass12_0.<<LoadAsync>b__0>d.MoveNext()

Hope it helps narrow things down!

[MikaelMayer]

I was bothered by this issue not later than yesterday as I was trying to use map updates. Thanks for providing an MVP !