Supplying type for _ in pattern causes crash

[RustanLeino]

Dafny version

4.0.0

Code to produce this issue

datatype Fruit = Apple(u: int) | Pear(t: int)

method Jkl(fruit: Fruit)
{
  match fruit
  case Apple(_: int) => // supplying ": int" here causes a crash
    DoSomething();
  case _  =>
}

method DoSomething() {
}

Command to run and resulting output

% dafny test.dfy
Unhandled exception. System.AggregateException: One or more errors occurred. (Value cannot be null. (Parameter 'key'))
 ---> System.ArgumentNullException: Value cannot be null. (Parameter 'key')
   at System.Collections.Generic.Dictionary`2.FindValue(TKey key)
   at System.Collections.Generic.Dictionary`2.TryGetValue(TKey key, TValue& value)
   at Microsoft.Dafny.Translator.CheckDefiniteAssignment(IdentifierExpr expr, BoogieStmtListBuilder builder)
   at Microsoft.Dafny.Translator.CheckWellformedWithResult(Expression expr, WFOptions options, Expr result, Type resultType, List`1 locals, BoogieStmtListBuilder builder, ExpressionTranslator etran)
   at Microsoft.Dafny.Translator.TrStmt(Statement stmt, BoogieStmtListBuilder builder, List`1 locals, ExpressionTranslator etran)

What happened?

As can be inspected using /rprint, the desugaring of the match statement introduces a variable _v00, but omits its declaration. This causes a crash downstream in the Dafny pipeline.

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

Mac

[RustanLeino]

Note, changing _: int to just _ or to x: int works around the problem.