One more soundness fix

Source/DafnyCore/Resolver.cs

@@ -9281,13 +9281,22 @@ void LiberalRHSVisit(Expression expr) {
  }
  }
  }
- } else if (expr is FunctionCallExpr { tok: var tok, Function: { IsStatic: false } function }) {
+
+ return null; // No problem to declare for this field
+ } else if (expr is FunctionCallExpr { tok: var tok, Function: { IsStatic: false } function } && visited.Count > 0) {
  var msg = "Constant field '" + visited[0].Name + "' cannot be accessed before 'new;'";
  for (var i = 1; i < visited.Count; i++) {
  msg += (i == 1 ? " because of the dependency " + visited[0].Name : "") + " -> " + visited[i].Name;
  }
  msg += ", " + (visited.Count > 1 ? "and" : "because") + " '" + visited[visited.Count - 1].Name + "' depends on the non-static function '" + function.Name + "' that can potentially read other uninitialized constants.";
  return (msg, visited[0]);
+ } else if (expr is ThisExpr && visited.Count > 0) {
+ var msg = "Constant field '" + visited[0].Name + "' cannot be accessed before 'new;'";
+ for (var i = 1; i < visited.Count; i++) {
+ msg += (i == 1 ? " because of the dependency " + visited[0].Name : "") + " -> " + visited[i].Name;
+ }
+ msg += ", " + (visited.Count > 1 ? "and" : "because") + " '" + visited[visited.Count - 1].Name + "' depends on the object 'this' itself, that can potentially read other uninitialized constants.";
+ return (msg, visited[0]);
  }
  foreach (var subExpr in expr.SubExpressions) {
  if (GetErrorIfConstantFieldNotInitialized(subExpr, visited) is var msgField && msgField != null) {

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

@@ -181,6 +181,18 @@ class C extends Tr {
  }
 }
 
+class DeepThisError {
+ const d: Dummy
+ const t: set<DeepThisError> := {this}
+
+ constructor() {
+ var x := set n: DeepThisError | n in t :: n.d.i;
+ // Error above: cannot use 't' because it depends on "this" which might have uninitialized constants
+ d := new Dummy(1);
+ new;
+ }
+}
+
 method Main() {
  var c := new SecondInitializationError(5);
  var d := new RecursiveError();

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

@@ -10,4 +10,5 @@ git-issue-2727.dfy(139,4): Error: The constant b cannot be assigned twice.
 git-issue-2727.dfy(150,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants.
 git-issue-2727.dfy(162,9): Error: Constant field 'c' cannot be accessed before 'new;' because of the dependency c -> a, and 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants.
 git-issue-2727.dfy(178,9): Error: Constant field 'a' cannot be accessed before 'new;', because 'a' depends on the non-static function 'B' that can potentially read other uninitialized constants.
-12 resolution/type errors detected in git-issue-2727.dfy
+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.
+13 resolution/type errors detected in git-issue-2727.dfy