Feature request: destructuring assignment in `:-`

[cpitclaudel]

Dafny currently rejects the following program:

datatype Result<+T, +R> = | Success(value: T) | Failure(error: R) {
  predicate method IsFailure() { Failure? }
  function method PropagateFailure<U>(): Result<U, R> requires Failure? { Failure(this.error) }
  function method Extract(): T requires Success? { value }
}

datatype D = D(i: int, b: bool)

method Main() returns (r: Result<D, ()>) {
  var D(i0, j0) := D(0, true);
  var D(i1, j1) :- Success(D(1, false)); // Error: invalid VarDeclStatement
}

It would be nice if :- was similar to := in allowing destructuring assignment.

Hey @samuelgruetter, do you remember why this difference exists between the two kind of var statements / expressions?

[samuelgruetter]

I agree that it would be nice to allow patterns on the lhs of :-. I think when I implemented it, I first wanted to get a simple version without patterns to work, and by the time that one was merged, my internship was over... I think one reason I was hesitant to implement patterns was that I was not sure about the interaction between multi-assignment (eg var a, b := b, a), methods returning multiple values (var a, b := myMethodReturningTwoValues(x)), destructuring assignments for pairs, and what to do with methods that return multiple values and can fail: Should these methods return a Result of a tuple, or should there be a special construct to return multiple values or a failure? So instead of making potentially bad decisions that later would need breaking changes, I decided to not rush an implementation. But if you keep these considerations in mind while implementing pattern support, there are certainly good ways of doing it :)

[seebees]

Some more relevant things #4892

[seebees]

It would also be nice to support destructuring assignment with nameonly fields.

  datatype LocalFoo = LocalFoo(nameonly a: nat, nameonly b: nat)

  function work2(): LocalFoo
  function not2(): Result<LocalFoo, string>

  method notWork() {
    var LocalFoo( c := a ) := work2();
    var LocalFoo( c := a ) :- not2();
  }