Fix: Ability to use .Key as a constant name in datatypes and classes (d…

…afny-lang#4423)

This PR fixes dafny-lang#4394
I added the corresponding test.

<small>By submitting this pull request, I confirm that my contribution
is made under the terms of the [MIT
license](https://github.com/dafny-lang/dafny/blob/master/LICENSE.txt).</small>

---------

Co-authored-by: Rustan Leino <[email protected]>

Source/DafnyCore/Verifier/Translator.cs

@@ -22,6 +22,7 @@
 using static Microsoft.Dafny.Util;
 using Core;
 using Microsoft.BaseTypes;
+using Microsoft.Dafny.Compilers;
 using Microsoft.Dafny.Triggers;
 using Action = System.Action;
 using PODesc = Microsoft.Dafny.ProofObligationDescription;
@@ -6662,10 +6663,11 @@ Bpl.Function GetReadonlyField(Field f) {
           return predef.ArrayLength;
         } else if (f.EnclosingClass is ValuetypeDecl { Name: "real" } && f.Name == "Floor") {
           return predef.RealFloor;
-        } else if (f is SpecialField && !(f is DatatypeDestructor)) {
+        } else if (f is SpecialField && !(f is DatatypeDestructor || f.EnclosingClass is TopLevelDeclWithMembers and not ValuetypeDecl)) {
           if (f.Name is "Keys" or "Values" or "Items") {
-            Contract.Assert(f.Type is SetType);
-            var setType = (SetType)f.Type;
+            var fType = f.Type.NormalizeExpand();
+            Contract.Assert(fType is SetType);
+            var setType = (SetType)fType;
             return f.Name switch {
               "Keys" => setType.Finite ? predef.MapDomain : predef.IMapDomain,
               "Values" => setType.Finite ? predef.MapValues : predef.IMapValues,

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

@@ -0,0 +1,32 @@
+// RUN: %baredafny verify %args "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+datatype T = T(
+    f:map<nat,nat>
+) {
+    const Keys := f.Keys // Used to be an error
+}
+
+codatatype codatatypeT = CT(
+    f:map<nat,nat>
+) {
+    const Keys := f.Keys // Used to be an error
+}
+
+type opaqueT {
+  const f: map<nat, nat>
+  const Keys := f.Keys
+}
+
+newtype newT = x: int | true {
+  const f: map<nat, nat> := map[]
+  const Keys := f.Keys
+}
+
+class C {
+  const Keys: set<nat>
+
+  constructor(f:map<nat,nat>) {
+    this.Keys := f.Keys;
+  }
+}

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

@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors

docs/dev/news/4394.fix

@@ -0,0 +1 @@
+Ability to use .Key as a constant name in datatypes and classes