Crash when named class constructor is used inside match case

[RustanLeino]

Dafny version

4.10

Code to produce this issue

datatype Color = Red | Blue
    
class C {
  constructor Init(x: int) { }
}
  
method Test(color: Color) {
  match color
  case Red =>
    var v := new C.Init(165); // This line causes Dafny to crash
  case Blue =>
}

Command to run and resulting output

% dafny resolve test.dfy

Encountered internal compilation exception: Value cannot be null. (Parameter 'key')
Unhandled exception: System.ArgumentNullException: Value cannot be null. (Parameter 'key')
   at System.Collections.Generic.Dictionary`2.FindValue(TKey key)
   at System.Collections.Generic.Dictionary`2.TryGetValue(TKey key, TValue& value)
   at Microsoft.Dafny.Util.GetOrDefault[K,V,V2](IReadOnlyDictionary`2 dictionary, K key, Func`1 createValue)
   at Microsoft.Dafny.Cloner.GetCloneIfAvailable(TopLevelDecl topLevelDecl)
   at Microsoft.Dafny.UserDefinedType..ctor(Cloner cloner, UserDefinedType original)
   at Microsoft.Dafny.Cloner.CloneType(Type t)
   at Microsoft.Dafny.TypeRhs..ctor(Cloner cloner, TypeRhs original)
   at Microsoft.Dafny.TypeRhs.Clone(Cloner cloner)
   at Microsoft.Dafny.Cloner.CloneRHS(AssignmentRhs rhs)
   at System.Linq.Enumerable.SelectListIterator`2.Fill(ReadOnlySpan`1 source, Span`1 destination, Func`2 func)
   at System.Linq.Enumerable.SelectListIterator`2.ToList()
   at Microsoft.Dafny.AssignStatement..ctor(Cloner cloner, AssignStatement original)
   at Microsoft.Dafny.AssignStatement.Clone(Cloner cloner)
   at Microsoft.Dafny.Cloner.CloneStmt(Statement stmt, Boolean isReference)
   at Microsoft.Dafny.VarDeclStmt..ctor(Cloner cloner, VarDeclStmt original)
   at Microsoft.Dafny.VarDeclStmt.Clone(Cloner cloner)
   at Microsoft.Dafny.Cloner.CloneStmt(Statement stmt, Boolean isReference)
   at Microsoft.Dafny.NestedMatchCaseStmt.<>c__DisplayClass9_0.<.ctor>b__0(Statement stmt)
   at System.Linq.Enumerable.SelectListIterator`2.Fill(ReadOnlySpan`1 source, Span`1 destination, Func`2 func)
   at System.Linq.Enumerable.SelectListIterator`2.ToList()
   at Microsoft.Dafny.NestedMatchCaseStmt..ctor(Cloner cloner, NestedMatchCaseStmt original)
   at Microsoft.Dafny.NestedMatchCaseStmt.Clone(Cloner cloner)
   at Microsoft.Dafny.MatchFlattener.<>c.<CompileNestedMatchStmt>b__6_0(NestedMatchCaseStmt nms)
   at System.Linq.Enumerable.SelectEnumerableIterator`2.ToList()
   at Microsoft.Dafny.MatchFlattener.CompileNestedMatchStmt(NestedMatchStmt nestedMatchStmt)
   at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass4_0.<FlattenNode>b__0(INode node)
   at Microsoft.Dafny.Node.Visit(Func`2 beforeChildren, Action`1 afterChildren, Action`1 reportError)
   at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root)
   at Microsoft.Dafny.MatchFlattener.PostResolve(ModuleDefinition module)
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken)
   at Microsoft.Dafny.Compilation.ResolveAsync()
   at Microsoft.Dafny.ResolveCommand.<>c.<<Create>b__0_0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Invocation.AnonymousCommandHandler.InvokeAsync(InvocationContext context)
   at System.CommandLine.Invocation.InvocationPipeline.<>c__DisplayClass4_0.<<BuildInvocationChain>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass17_0.<<UseParseErrorReporting>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass12_0.<<UseHelp>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass17_0.<<AddDeveloperHelp>b__1>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass22_0.<<UseVersionOption>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass19_0.<<UseTypoCorrections>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<UseSuggestDirective>b__18_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass16_0.<<UseParseDirective>b__0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c.<<RegisterWithDotnetSuggest>b__5_0>d.MoveNext()
--- End of stack trace from previous location ---
   at System.CommandLine.Builder.CommandLineBuilderExtensions.<>c__DisplayClass8_0.<<UseExceptionHandler>b__0>d.MoveNext()

What happened?

Dafny crashes. The problem seems related to match desugaring.

Everything is fine if constructor Init(x: int) is changed to the anonymous constructor (x: int) and the new is updated accordingly. It's also find if new C.Init(165) is called outside the match.

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

Mac