diff --git a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
index 39ba59fd09..a4d93a820e 100644
--- a/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
+++ b/Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs
@@ -346,7 +346,7 @@ private void DatatypeFieldsAndConstructor(DatatypeCtor ctor, ConcreteSyntaxTree
 
     private string DtCtorDeclarationName(DatatypeCtor ctor, bool full = false) {
       var dt = ctor.EnclosingDatatype;
-      return $"{(full ? dt.GetFullCompileName(Options) : dt.GetCompileName(Options))}_{ctor.GetCompileName(Options)}";
+      return $"{(full ? dt.GetFullCompileName(Options) : IdProtect(dt.GetCompileName(Options)))}_{ctor.GetCompileName(Options)}";
     }
 
     protected IClassWriter DeclareType(TopLevelDecl d, SubsetTypeDecl.WKind witnessKind, Expression witness, ConcreteSyntaxTree wr) {
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy
new file mode 100644
index 0000000000..f55fe494d5
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy
@@ -0,0 +1,15 @@
+// RUN: %testDafnyForEachCompiler --refresh-exit-code=0 "%s"
+
+module SomeDependencyModule {
+  datatype None = None
+}
+
+module SomeModule {
+  import SomeDependencyModule
+
+  const test := SomeDependencyModule.None
+}
+
+method Main() {
+  print SomeModule.test, "\n";
+}
\ No newline at end of file
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect
new file mode 100644
index 0000000000..2954079eab
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.expect
@@ -0,0 +1 @@
+SomeDependencyModule.None.None
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check
new file mode 100644
index 0000000000..2e0db5d532
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-5469.dfy.rs.check
@@ -0,0 +1 @@
+CHECK: error
\ No newline at end of file
diff --git a/docs/dev/news/5476.fix b/docs/dev/news/5476.fix
new file mode 100644
index 0000000000..156ae3c64f
--- /dev/null
+++ b/docs/dev/news/5476.fix
@@ -0,0 +1 @@
+Apply name mangling to datatype names in Python more often