dafny icon indicating copy to clipboard operation
dafny copied to clipboard

internal error on match with static const of newtype

Open erniecohen opened this issue 9 months ago • 2 comments

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, List1 paths, Cons1 consMatchees) at Microsoft.Dafny.MatchFlattener.CompilePatternPaths(MatchCompilationState state, MatchingContext context, SinglyLinkedList1 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(Func2 beforeChildren, Action1 afterChildren, Action1 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()

erniecohen avatar May 03 '24 15:05 erniecohen

no crash when match is replaced with conditionals

erniecohen avatar May 03 '24 15:05 erniecohen

Moved to dafny-lang/dafny since this does not seem IDE related.

keyboardDrummer avatar May 06 '24 09:05 keyboardDrummer