Parsing error after match statement with empty arm

[markrtuttle]

Dafny version

nightly-2023-12-13-2cadde8

Code to produce this issue

module Example {
  import opened Std.Wrappers

  function nonzero(n: nat): Result<nat, string> {
    if n == 0 then Failure("Zero") else Success(n)
  }

  method Main() {
    var result := nonzero(0);

    match result
    case Failure(msg) => {print msg, "\n"; return; }
    case Success(n) => {}

    if n < 5 {print "big\n"; } else {print "small\n";}
  }
}

Command to run and resulting output

dafny-nightly resolve --standard-libraries example0.dfy 

Dafny program verifier did not attempt verification

What happened?

The scope of the variable n should be limited to the case arm, which is an empty block, but nothing complains about the use of n outside of this block (in the conditional after the match statement).

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

Mac

[robin-aws]

Does not seem to relate to the use of standard libraries at least, since this also incorrectly doesn't produce a resolution error:

module Example {

  datatype Foo = Foo(n: nat)

  method Main() {
    match Foo(42)
    case Foo(n) => {}

    if n < 5 {print "big\n"; } else {print "small\n";}
  }
}

[robin-aws]

Ah the actual problem is that the parsing after match statement => symbols is greedier than you'd think, and actually binds to any statements following it. The program parses equivalently to this (which is what you get if you insert a newline before the {} and then run dafny format):

module Example {
  import opened Std.Wrappers

  function nonzero(n: nat): Result<nat, string> {
    if n == 0 then Failure("Zero") else Success(n)
  }

  method Main() {
    var result := nonzero(0);
    match result
    case Failure(msg) =>
      {print msg, "\n"; return; }
    case Success(n) =>
      {}
      if n < 5 {print "big\n"; } else {print "small\n";}
  }
}

We could probably use an FAQ entry and/or a linter warning about this though.

[RustanLeino]

I suggest we generate two warnings to help with this:

• If the entire body of a case consists of a block statement (that is, { ... }), then we can generate a warning saying that the curly braces are redundant. This would give a warning for the first case in the example above.
• If a statement in the body of a case has the same indentation as the case token itself (or has less indentation than the case token), then we can generate a warning about suspicious indentation, like we do for expressions when we try to detect operator-precedence errors. This would give a warning for the second case in the example above.

[markrtuttle]

This greedy parsing is mentioned in the manual's description of the match statement, but it requires close inspection to see it (a one-line comment at the end of the Dafny code example). I think the solution is for me to delimit the scope of my match statement by enclosing the entire match statement within braces, forming a scope containing a single statement. I think this language design borders on a soundness issue (or credibility issue) for a developer who tells the team that one thing has been proved when, in fact, something different has been proved because the language semantics do not conform to most imperative programming languages known to the team doing the developer's code reviews.

[MikaelMayer]

Normally the dafny formatter would have caught this and aligned the last statements together so you would have seen that. But I guess you cannot use the formatter right now because of dfyconfig.toml, right?

[RustanLeino]

You can of course delimit the scope of an entire match statement by enclosing it in braces, and delimit the scope of a match expression by enclosing it in parentheses. But both of these match constructs also allow you to put braces around all the cases:

match xs {
  case Nil => ...
  case Cons(x, ys) => ...
}

(I indent each case when using the { form, and align each case with the match when I don't use {.)

Another good-to-know property of the match statement: Each case is a scope by itself. That is, a local variable declared in one case goes out of scope at the end of that case.

[markrtuttle]

This a far better solution than I proposed.