dafny
dafny copied to clipboard
internal error on match with static const of newtype
Failing code
newtype T = nat {
static const C := 0 as T
const V:bool := match this case C => true
}
Steps to reproduce the issue
- Dafny version: 4.6.0.0
- Dafny VSCode extension version: 3.3.0
- type-system-refresh, general-traits = full
Expected behavior
not crashing
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.MatchFlattener.LetBind(IdPattern var, Expression genExpr, PatternPath bodyPath)
at Microsoft.Dafny.MatchFlattener.LetBindNonWildCard(IdPattern idPattern, Expression expr, PatternPath bodyPath)
at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass14_0.<CompilePatternPathsForMatchee>b__4(PatternPath path)
at System.Linq.Enumerable.SelectListIterator2.ToList() at Microsoft.Dafny.MatchFlattener.CompilePatternPathsForMatchee(MatchCompilationState state, MatchingContext context, List
1 paths, Cons1 consMatchees) at Microsoft.Dafny.MatchFlattener.CompilePatternPaths(MatchCompilationState state, MatchingContext context, SinglyLinkedList
1 matchees, List1 paths) at Microsoft.Dafny.MatchFlattener.CompileNestedMatchExpr(NestedMatchExpr nestedMatchExpr) at Microsoft.Dafny.MatchFlattener.<>c__DisplayClass5_0.<FlattenNode>b__0(INode node) at Microsoft.Dafny.Node.Visit(Func
2 beforeChildren, Action1 afterChildren, Action
1 reportError)
at Microsoft.Dafny.MatchFlattener.FlattenNode(Node root)
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.<Resolve>b__0()
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()
no crash when match is replaced with conditionals
Moved to dafny-lang/dafny
since this does not seem IDE related.