--warn-missing-constructor-parentheses doesn't warn when missing constructor arguments

[robin-aws]

Dafny version

4.6.0 (but pretty sure it's always been like this)

Code to produce this issue

datatype Foo = Bar(a: int) | Baz | Quaz

predicate Dorp(f: Foo) {
  match f {
    case Baz() => false
    case Bar => true
  }
}

Command to run and resulting output

% dafny resolve Scratch.dfy --warn-missing-constructor-parentheses

Dafny program verifier did not attempt verification

What happened?

--warn-missing-constructor-parentheses is intended to warn against typos when trying to reference a data constructor in a match case, which results in binding the value to a new symbol instead. The code above is an instance of this mistake, where there is no warning that Bar is actually a new symbol instead of a reference to Bar, and also no verifier warning that Quaz is not handled. If Bar(a: int) is changed to just Bar the warning does occur.

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

Mac