internal error on static constants in newtypes based on bitvectors

[erniecohen]

Dafny version

4.6

Code to produce this issue

newtype T = bv1 {
    static const c := 0 as T
}
const c := T.c

Command to run and resulting output

vscode

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.DetectUnderspecificationVisitor.VisitOneExpr(Expression expr) at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable1 coll, Action1 action) at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) at Microsoft.Boogie.CollectionExtensions.ForEach[T](IEnumerable1 coll, Action1 action) at Microsoft.Dafny.BottomUpVisitor.Visit(Expression expr) at Microsoft.Dafny.UnderspecificationDetector.CheckExpression(Expression expr, UnderspecificationDetectorContext context) at Microsoft.Dafny.UnderspecificationDetector.CheckMember(MemberDecl member) at Microsoft.Dafny.UnderspecificationDetector.CheckMembers(TopLevelDeclWithMembers cl) at Microsoft.Dafny.UnderspecificationDetector.Check(List1 declarations) 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.ProgramResolver.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.<>n__0(CancellationToken cancellationToken) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.<>c__DisplayClass5_0.<Resolve>b__0() at Microsoft.Dafny.LanguageServer.Language.CacheExtensions.ProfileAndPruneCache[T,Key,Value](PruneIfNotUsedSinceLastPruneCache2 cache, Func1 useCache, TelemetryPublisherBase telemetryPublisher, String programName, String activity) at Microsoft.Dafny.LanguageServer.Language.CachingResolver.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.<>c__DisplayClass5_0.<<ResolveAsync>b__0>d.MoveNext() --- End of stack trace from previous location --- at Microsoft.Dafny.TextDocumentLoader.ResolveAsync(Compilation compilation, Program program, CancellationToken cancellationToken) at Microsoft.Dafny.Compilation.ResolveAsync()

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

Mac

[keyboardDrummer]

I can't reproduce this on 4.6, neither in the IDE nor the CLI:

rwillems@bcd0745419f2 Sync % dafny --version
4.6.0
rwillems@bcd0745419f2 Sync % dafny verify ./temp.dfy
Temp/temp.dfy(4,6): Error: the type of this const is underspecified
  |
4 | const c := T.c
  |       ^

1 resolution/type errors detected in temp.dfy
rwillems@bcd0745419f2 Sync % dafny verify --type-system-refresh ./temp.dfy

Dafny program verifier finished with 0 verified, 0 errors

[stefan-aws]

Closing this issue as I can't reproduce it either. Feel free to push again if needed.

[erniecohen]

I should have mentioned that this is with --type-system-refresh --general-newtypes.

[keyboardDrummer]

With the above I can reproduce it. Note that just --type-system-refresh is not enough