Support for explicitly pass this receiver as a parameter of method

[Ao-senXiong]

Summary

Consider the following Example method, which already use this receiver in the method body.

class C {
  var f: int
  var x: int
  method Example() returns (b: bool)
  {
    var x: int;
    b := f == this.f;
  }
}

However, Dafny current does not support explicit pass this receiver as a parameter like the following and reject the code.

  method Example(this: C) returns (b: bool)
  {
    var x: int;
    b := f == this.f;
  }

Background and Motivation

Rustan mentioned there could be two potential use of it.

1. Support extension method in the future.
2. Use it as a nullable receiver this: C?.

Proposed Feature

Explicit pass in this should not be rejected by the compiler and should behave the same as use this for field read and write directly.

Alternatives

No response