Crash in Resolver.CheckLinearExtendedPattern

[gauravpartha]

The following Dafny program crashes on master (commit 1647032):

method a() 
{
    var tok := (0,0);
    match tok {
      case "B" => 
      case _ => 
    }
}

The error message + stack trace is:

Unhandled exception. System.AggregateException: One or more errors occurred. (Unable to cast object of type 'Microsoft.Dafny.LitPattern' to type 'Microsoft.Dafny.IdPattern'.)
 ---> System.InvalidCastException: Unable to cast object of type 'Microsoft.Dafny.LitPattern' to type 'Microsoft.Dafny.IdPattern'.
   at Microsoft.Dafny.Resolver.CheckLinearExtendedPattern(Type type, ExtendedPattern pat, ResolveOpts opts) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 12684
   at Microsoft.Dafny.Resolver.CheckLinearNestedMatchCase(Type type, NestedMatchCase mc, ResolveOpts opts) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 12758
   at Microsoft.Dafny.Resolver.CheckLinearNestedMatchStmt(Type dtd, NestedMatchStmt ms, ResolveOpts opts) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 12778
   at Microsoft.Dafny.Resolver.ResolveNestedMatchStmt(NestedMatchStmt s, ResolveOpts opts) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 11726
   at Microsoft.Dafny.Resolver.ResolveStatement(Statement stmt, ICodeContext codeContext) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 11643
   at Microsoft.Dafny.Resolver.ResolveStatementWithLabels(Statement stmt, ICodeContext codeContext) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 13627
   at Microsoft.Dafny.Resolver.ResolveBlockStatement(BlockStmt blockStmt, ICodeContext codeContext) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 13597
   at Microsoft.Dafny.Resolver.ResolveMethod(Method m) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 10392
   at Microsoft.Dafny.Resolver.ResolveClassMemberBodies(TopLevelDeclWithMembers cl) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 9605
   at Microsoft.Dafny.Resolver.ResolveTopLevelDecls_Core(List`1 declarations, Graph`1 datatypeDependencies, Graph`1 codatatypeDependencies, Boolean isAnExport) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 2818
   at Microsoft.Dafny.Resolver.ResolveModuleDefinition(ModuleDefinition m, ModuleSignature sig, Boolean isAnExport) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 1032
   at Microsoft.Dafny.Resolver.ResolveProgram(Program prog) in /dafny_versions/dafny_master/Source/Dafny/Resolver.cs:line 507
   at Microsoft.Dafny.Main.Resolve(Program program, ErrorReporter reporter) in /dafny_versions/dafny_master/Source/Dafny/DafnyMain.cs:line 162
   at Microsoft.Dafny.Main.ParseCheck(IList`1 files, String programName, ErrorReporter reporter, Program& program) in /dafny_versions/dafny_master/Source/Dafny/DafnyMain.cs:line 113
   at Microsoft.Dafny.DafnyDriver.ProcessFiles(IList`1 dafnyFiles, ReadOnlyCollection`1 otherFileNames, ErrorReporter reporter, Boolean lookForSnapshots, String programId) in /dafny_versions/dafny_master/Source/DafnyDriver/DafnyDriver.cs:line 249
   --- End of inner exception stack trace ---
   at System.Threading.Tasks.Task.ThrowIfExceptional(Boolean includeTaskCanceledExceptions)
   at System.Threading.Tasks.Task`1.GetResultCore(Boolean waitCompletionNotification)
   at System.Threading.Tasks.Task`1.get_Result()
   at Microsoft.Dafny.DafnyDriver.ThreadMain(String[] args) in /dafny_versions/dafny_master/Source/DafnyDriver/DafnyDriver.cs:line 67
   at Microsoft.Dafny.DafnyDriver.<>c__DisplayClass6_0.<Main>b__0() in /dafny_versions/dafny_master/Source/DafnyDriver/DafnyDriver.cs:line 47
   at System.Threading.Thread.StartCallback()

[cpitclaudel]

Similar issue here:

datatype T = T(T, T) {
  predicate P() {
    match this
      case T(0, 1) => false
  }
}