diff --git a/Source/DafnyCore/Verifier/Translator.cs b/Source/DafnyCore/Verifier/Translator.cs
index 6eadac8ff71..0bbd988d355 100644
--- a/Source/DafnyCore/Verifier/Translator.cs
+++ b/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;
@@ -6695,10 +6696,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,
diff --git a/Test/git-issues/git-issue-4394.dfy b/Test/git-issues/git-issue-4394.dfy
new file mode 100644
index 00000000000..2c371d5c594
--- /dev/null
+++ b/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;
+  }
+}
\ No newline at end of file
diff --git a/Test/git-issues/git-issue-4394.dfy.expect b/Test/git-issues/git-issue-4394.dfy.expect
new file mode 100644
index 00000000000..823a60a105c
--- /dev/null
+++ b/Test/git-issues/git-issue-4394.dfy.expect
@@ -0,0 +1,2 @@
+
+Dafny program verifier finished with 1 verified, 0 errors
diff --git a/docs/dev/news/4394.fix b/docs/dev/news/4394.fix
new file mode 100644
index 00000000000..2b35bca5c9f
--- /dev/null
+++ b/docs/dev/news/4394.fix
@@ -0,0 +1 @@
+Ability to use .Key as a constant name in datatypes and classes
\ No newline at end of file