internal error: System.NullReferenceException

Failing code

trait Ins {
    predicate safe?(s:State)
    function step(s:State):State //requires safe?(s)
}
trait Halt extends Ins {}
newtype Error extends Ins = n:nat | n == 0 {
    static const Ins := 0 as Error
    predicate safe?(s:State) { false }
    function step(s:State):State {s}//requires safe?(s) {s}
}
type Code = seq<Ins>
datatype State = S(
    //code:Code,
    pc:nat,
    reg:nat,
    clock:nat
) {
    //const fetch:Ins := if |code| <= pc then Error.Ins else code[pc]
    function fetch_():Ins
    const fetch := fetch_()
    const safe? := fetch.safe?(this)
    const step := fetch.step(this)
    const halt? := (fetch is Halt) || !safe?
    function run():State decreases clock {
        if clock == 0 || halt? then this else step.(clock := clock - 1).run()
    }
}

Steps to reproduce the issue

Dafny version: 4.6.0.0 (nightly build 4.17)
Dafny VSCode extension version: 3.3.0

Expected behavior

Actual behavior

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.ConcreteSyntaxExpression.get_TerminalExpressions()+MoveNext() at System.Linq.Enumerable.All[TSource](IEnumerable1 source, Func2 predicate) at Microsoft.Dafny.ExpressionTester.CheckIsCompilable(Expression expr, ICodeContext codeContext, Boolean insideBranchesOnly) at Microsoft.Dafny.ModuleResolver.ResolveClassMembers_Pass1(TopLevelDeclWithMembers cl) 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, Func`1 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.<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()

dafny-lang / ide-vscode