Unsound use of `{this}` in constant initialization

[MikaelMayer]

The following crashes:

class Dummy {
  const i: int
  constructor(i: int) {
    this.i := i;
  }
}
class ThisError {
  const d: Dummy
  const t: set<ThisError> := {this}

  constructor() {
    var x := set n: ThisError | n in t :: n.d.i;
    d := new Dummy(1);
    new;
  }
}

method Main() {
  var x := new ThisError();
}

[RustanLeino]

In the first phase of a class constructor, there are restrictions on how a const field of this can be used in the RHS of an assignment. Currently, those restrictions are lifted if the const field has been declared with a defining RHS. For example:

class MyClass {
  const a: int := 5
  const b: int
  const c: int

  constructor (x: int) {
    b := x;
    if {
      case true =>
        var x := this.a; // this is currently allowed, because 'a' has a RHS
        var y := this.b; // this is not allowed
      case true =>
        // both of the following are allowed, because the RHS is exactly one field
        this.c := this.a;
        this.c := this.b;
      case true =>
        this.c := 1 + this.a; // because 'a' has a RHS, it's currently allowed in any RHS expression
        this.c := 1 + this.b; // but 'b' is not
    }
    new;
  }
}

I think all const fields should have to those restrictions. That is, we should not lift those restrictions for const fields with a defining RHS. This would solve the reported issue, because it would disallow the use of this.t in the RHS of the assignment to x.

(Note, the restrictions I have mentioned are enforced by the Resolver. Additionally, definite assignment rules apply, which are enforced by the Verifier. My suggested fix involves only the Resolver.)

[MikaelMayer]

I think that "all const fields should have to those restrictions" would be sufficient to solve this issue, but not necessary.
In the PR #2862 I implemented the following straightforward fix that does not have the burdening restriction that you suggest.
Specifically, in the case above, one would get the following error:

dafny/Test/git-issues/git-issue-2727.dfy.expect

Line 13 in 5555cde

git-issue-2727.dfy(189,41): Error: Constant field 't' cannot be accessed before 'new;', because 't' depends on the object 'this' itself, that can potentially read other uninitialized constants.