New resolver crash on qualified data constructor reference

[robin-aws]

Dafny version

4.9.1

Code to produce this issue

datatype Foo = Foo(x: int)

const f := Foo.Foo(0)

Command to run and resulting output

% dafny verify Scratch.dfy --type-system-refresh
Encountered internal compilation exception: Object reference not set to an instance of an object.
Unhandled exception: System.NullReferenceException: Object reference not set to an instance of an object.
   at Microsoft.Dafny.PreTypeResolver.ResolveActualParameters(ActualBindings bindings, List`1 formals, IOrigin callTok, Object context, ResolutionContext opts, Dictionary`2 typeMap, Expression receiver) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.ActualParameters.cs:line 129
   at Microsoft.Dafny.PreTypeResolver.ResolveDatatypeValue(ResolutionContext resolutionContext, DatatypeValue dtv, DatatypeDecl datatypeDecl, DPreType ty, Boolean complain) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs:line 2460
   at Microsoft.Dafny.PreTypeResolver.ResolveDotSuffix(ExprDotName expr, Boolean allowStaticReferenceToInstance, Boolean isLastNameSegment, List`1 args, ResolutionContext resolutionContext, Boolean allowMethodCall) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs:line 1852
   at Microsoft.Dafny.PreTypeResolver.ResolveApplySuffix(ApplySuffix e, ResolutionContext resolutionContext, Boolean allowMethodCall) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs:line 2032
   at Microsoft.Dafny.PreTypeResolver.ResolveExpression(Expression expr, ResolutionContext resolutionContext) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.Expressions.cs:line 205
   at Microsoft.Dafny.PreTypeResolver.ResolveConstRHS(ConstantField cfield, Boolean initialResolutionPass) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 1093
   at Microsoft.Dafny.PreTypeResolver.<FillInPreTypesInSignature>g__ComputePreTypeField|54_1(Field field) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 842
   at Microsoft.Dafny.PreTypeResolver.FillInPreTypesInSignature(Declaration declaration) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 922
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarationSignature(Declaration d) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 818
   at Microsoft.Dafny.PreTypeResolver.ResolvePreTypeSignature(Declaration d, PreTypeInferenceModuleState preTypeInferenceModuleState, ModuleResolver resolver) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 771
   at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List`1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/PreType/PreTypeResolve.cs:line 726
   at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, String moduleDescription, Boolean isAnExport) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 1155
   at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/AST/Modules/ModuleDefinition.cs:line 494
   at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/AST/Modules/LiteralModuleDecl.cs:line 138
   at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/ModuleResolver.cs:line 185
   at Microsoft.Dafny.ProgramResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 173
   at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Resolver/ProgramResolver.cs:line 67
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.RunDafnyResolver(Compilation compilation, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 54
   at Microsoft.Dafny.LanguageServer.Language.Symbols.DafnyLangSymbolResolver.ResolveSymbols(Compilation compilation, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyLanguageServer/Language/Symbols/DafnyLangSymbolResolver.cs:line 41
   at Microsoft.Dafny.TextDocumentLoader.ResolveInternal(Compilation compilation, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Pipeline/TextDocumentLoader.cs:line 56
   at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Pipeline/TextDocumentLoader.cs:line 46
   at Microsoft.Dafny.Compilation.ResolveAsync() in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Pipeline/Compilation.cs:line 276
   at Microsoft.Dafny.VerifyCommand.HandleVerification(DafnyOptions options) in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/Commands/VerifyCommand.cs:line 66
   at Microsoft.Dafny.Compilation.LogExceptions() in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyCore/Pipeline/Compilation.cs:line 120
   at Microsoft.Dafny.DafnyNewCli.<>c__DisplayClass5_0.<<SetHandlerUsingDafnyOptionsContinuation>g__Handle|0>d.MoveNext() in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 146
--- 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() in /Users/salkeldr/Documents/GitHub/dafny/Source/DafnyDriver/DafnyNewCli.cs:line 277
--- 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?

Does not crash if --type-system-refresh is omitted, or if Foo.Foo(0) is replaced by just Foo(0).

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

Mac