newtype based on bv64 crashes resolver

[erniecohen]

Dafny version

4.8.1

Code to produce this issue

newtype Foo = bv64 

// note: this problem appears only with bv64, not bv63, bv65, bv32, ...

Command to run and resulting output

building from a project file with 

general-traits = "datatype"
type-system-refresh = "true"
general-newtypes = "true"

What happened?

Dafny encountered an internal error. Please report it at https://github.com/dafny-lang/dafny/issues.
System.NullReferenceException: Object reference not set to an instance of an object.
at Microsoft.Dafny.ModuleResolver.AddToInheritedMembers(TopLevelDeclWithMembers cl, TopLevelDeclWithMembers baseOrParentTypeDecl, Dictionary2 inheritedMembers, List1 membersWithErrors)
at Microsoft.Dafny.ModuleResolver.RegisterInheritedMembers(TopLevelDeclWithMembers cl, DPreType basePreType)
at Microsoft.Dafny.PreTypeResolver.ResolvePreTypeSignature(Declaration d, PreTypeInferenceModuleState preTypeInferenceModuleState, ModuleResolver resolver)
at Microsoft.Dafny.PreTypeResolver.ResolveDeclarations(List1 declarations, ModuleResolver resolver, Boolean firstPhaseOnly) at Microsoft.Dafny.ModuleResolver.ResolveTopLevelDecls_Core(List1 declarations, Graph1 datatypeDependencies, Graph1 codatatypeDependencies, String moduleDescription, Boolean isAnExport)
at Microsoft.Dafny.ModuleDefinition.Resolve(ModuleSignature sig, ModuleResolver resolver, String exportSetName)
at Microsoft.Dafny.LiteralModuleDecl.Resolve(ModuleResolver resolver, CompilationData compilation)
at Microsoft.Dafny.ModuleResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.ResolveModuleDeclaration(CompilationData compilation, ModuleDecl decl)
at Microsoft.Dafny.ProgramResolver.Resolve(CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<b__0>d.MoveNext()
--- End of stack trace from previous location ---
at Microsoft.Dafny.PruneIfNotUsedSinceLastPruneCache2.UseAndPrune[T](Func1 use, CancellationToken cancellationToken)
at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,TKey,TValue](PruneIfNotUsedSinceLastPruneCache2 cache, Func1 useCache, ILogger logger, TelemetryPublisherBase telemetryPublisher, String programName, String activity, 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.Compilation.LogExceptions()

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

Mac

[erniecohen]

This appears to be an issue with the incremental resolver. If you restart Dafny, the resolver is happy and the code verifies. If you then add a newline to the source whitespace, the resolver crashes again.