ProveField false positive for var parameters

[etan-status]

Description

A ProveField warning is emitted when accessing a field of a case object that is passed as var.

{.push warning[ProveField]:on.}

type Foo = object
  case a: bool
  of false:
    x: int
  of true:
    y: float

# Warning: cannot prove that field 'f.x' is accessible
# Warning: cannot prove that field 'f.y' is accessible
proc foo(f: var Foo) =
  case f.a
  of false:
    echo $f.x
  of true:
    echo $f.y

var f = Foo(a: false, x: 42)
f.foo

# No warning emitted
proc bar(f: Foo) =
  case f.a
  of false:
    echo $f.x
  of true:
    echo $f.y

var g = Foo(a: false, x: 42)
g.bar

Nim Version

% nim -v
Nim Compiler Version 1.6.12 [MacOSX: amd64]
Compiled at 2023-06-09
Copyright (c) 2006-2023 by Andreas Rumpf

git hash: 1aa9273640c0c51486cf3a7b67282fe58f360e91
active boot switches: -d:release

Current Output

./test.nim(10, 1) template/generic instantiation from here
./test.nim(13, 12) Warning: cannot prove that field 'f.x' is accessible [ProveField]
      echo $f.x
             ^
./test.nim(10, 1) template/generic instantiation from here
./test.nim(15, 12) Warning: cannot prove that field 'f.y' is accessible [ProveField]
      echo $f.y
             ^

Expected Output

No `ProveField` warning

Possible Solution

The warning is suppressable by surrounding the function:

{.push warning[ProveField]:off.}
proc foo(f: var Foo) =
  case f.a
  of false:
    echo $f.x
  of true:
    echo $f.y
{.push warning[ProveField]:on.}

Note that warnings are not suppressable inside the proc:

proc foo(f: var Foo) =
  {.push warning[ProveField]:off.}
  case f.a
  of false:
    echo $f.x
  of true:
    echo $f.y
  {.push warning[ProveField]:on.}

Additional Information

No response

[Araq]

But a var is mutable and you could in theory mutate the object in between the case match and the access to the field.

[etan-status]

Yes, but it would be great if the error would be emitted in the situation when the case is actually changed.

Or, provide the ability to suppress a warning for a block or even a line. Right now, it's very difficult to suppress warnings when using templates.