Dictionary Error With Object Update Syntax

[GenericMonkey]

Dafny version

VSCode : 4.0.0.50303

Code to produce this issue

datatype Type = 
  | Cons()


datatype Test = Test(
  y : Type,
  y : Type
) 

predicate pred(t: Test, t': Test)
{
  && t' == t.(y := Cons())
}

Command to run and resulting output

[Error - 2:47:04 PM] Request textDocument/hover failed.
  Message: Internal Error - System.ArgumentException: An item with the same key has already been added. Key: y
   at System.Collections.Generic.Dictionary`2.TryInsert(TKey key, TValue value, InsertionBehavior behavior)
   at Microsoft.Dafny.Resolver.<>c__DisplayClass83_0.<ResolveActualParameters>b__1(Formal f)
   at System.Collections.Generic.List`1.ForEach(Action`1 action)
   at Microsoft.Dafny.Resolver.ResolveActualParameters(ActualBindings bindings, List`1 formals, IToken callTok, Object context, ResolutionContext resolutionContext, Dictionary`2 typeMap, Expression receiver)
   at Microsoft.Dafny.Resolver.ResolveDatatypeValue(ResolutionContext resolutionContext, DatatypeValue dtv, DatatypeDecl dt, Type ty, Boolean complain)
   at Microsoft.Dafny.Resolver.DesugarDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List`1 candidateResultCtors, Dictionary`2 rhsBindings, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveDatatypeUpdate(IToken tok, Expression root, DatatypeDecl dt, List`1 memberUpdates, ResolutionContext resolutionContext, List`1& members, List`1& legalSourceConstructors)
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext)
   at Microsoft.Dafny.Resolver.ResolveFunction(Function f)
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl)
   at Microsoft.Dafny.Resolver.ResolveNamesAndInferTypesForOneDeclaration(TopLevelDecl topd)
   at Microsoft.Dafny.Resolver.ResolveNamesAndInferTypes(List`1 declarations, Boolean initialRound)
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport)
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(TextDocumentItem document, Program program)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(TextDocumentItem textDocument, Program program, Boolean& canDoVerification, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.LoadInternal(DocumentTextBuffer textDocument, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Workspace.TextDocumentLoader.<>c__DisplayClass13_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.GetSnapshotAfterResolutionAsync()
   at Microsoft.Dafny.LanguageServer.Handlers.DafnyHoverHandler.Handle(HoverParams 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 code should soft error in VSCode, detecting the duplicate field name (y).
However, it instead crashes with an internal dictionary error when the second y is added to the datatype Test.
This is the minimal repro I was able to create -- the update syntax in the pred predicate is necessary for the crash to happen from my tinkering on it.

Thanks for your hard work!

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

Windows

[keyboardDrummer]

Thanks for the report !