Fix module+member name collision by prefixing imports with m_

Source/DafnyCore/AST/Modules/ModuleDefinition.cs

@@ -210,13 +210,18 @@ public string SanitizedName {
 
   string compileName;
 
+  public ModuleDefinition GetImplementedModule() {
+    return Implements is { Kind: ImplementationKind.Replacement } ? Implements.Target.Def : null;
+  }
+
   public string GetCompileName(DafnyOptions options) {
     if (compileName != null) {
       return compileName;
     }
 
-    if (Implements is { Kind: ImplementationKind.Replacement }) {
-      return Implements.Target.Def.GetCompileName(options);
+    var implemented = GetImplementedModule();
+    if (implemented != null) {
+      return implemented.GetCompileName(options);
     }
 
     var externArgs = options.DisallowExterns ? null : Attributes.FindExpressions(this.Attributes, "extern");

Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs

@@ -163,7 +163,7 @@ protected override void EmitBuiltInDecls(SystemModuleManager systemModuleManager
         wr.WriteLine("#if ISDAFNYRUNTIMELIB");
       }
 
-      var dafnyNamespace = CreateModule("Dafny", false, null, null, null, wr);
+      var dafnyNamespace = CreateModule(null, "Dafny", false, null, null, null, wr);
       EmitInitNewArrays(systemModuleManager, dafnyNamespace);
       if (Synthesize) {
         CsharpSynthesizer.EmitMultiMatcher(dafnyNamespace);
@@ -274,7 +274,8 @@ string IdProtectModule(string moduleName) {
       return string.Join(".", moduleName.Split(".").Select(IdProtect));
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtectModule(moduleName);
       return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");

Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs

@@ -159,7 +159,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"int main(DafnySequence<DafnySequence<char>> {argsParameterName})");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       var s = $"namespace {IdProtect(moduleName)} ";
       string footer = "// end of " + s + " declarations";

Source/DafnyCore/Backends/Dafny/DafnyCodeGenerator.cs

@@ -124,7 +124,8 @@ private bool NeedsExternalImport(MemberDecl memberDecl) {
              memberDecl is Function { Body: null } or Method { Body: null };
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       if (currentBuilder is ModuleContainer moduleBuilder) {
         var attributes = (Sequence<DAST.Attribute>)ParseAttributes(moduleAttributes);

Source/DafnyCore/Backends/GoLang/GoCodeGenerator.cs

@@ -53,8 +53,10 @@ string FormatDefaultTypeParameterValue(TopLevelDecl tp) {
       return $"_default_{tp.GetCompileName(Options)}";
     }
 
+    private readonly Dictionary<ModuleDefinition, Import> ModuleImports = new();
     private readonly List<Import> Imports = new(StandardImports);
     private string ModuleName;
+    private ModuleDefinition CurrentModule;
     private ConcreteSyntaxTree RootImportWriter;
     private ConcreteSyntaxTree RootImportDummyWriter;
 
@@ -134,6 +136,7 @@ public string TransformToClassName(string baseName) =>
       IdProtect(Regex.Replace(baseName, "[^_A-Za-z0-9$]", "_"));
 
     public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
+      CurrentModule = null;
       var companion = TypeName_Companion(UserDefinedType.FromTopLevelDeclWithAllBooleanTypeParameters(mainMethod.EnclosingClass), wr, mainMethod.tok, mainMethod);
 
       var wBody = wr.NewNamedBlock("func main()");
@@ -159,7 +162,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewNamedBlock("func (_this * {0}) Main({1} _dafny.Sequence)", FormatCompanionTypeName(((GoCodeGenerator.ClassWriter)cw).ClassName), argsParameterName);
     }
 
-    private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition externModule, string /*?*/ libraryName) {
+    private Import CreateImport(string moduleName, ModuleDefinition externModule,
+      string /*?*/ libraryName, string namePrefix = "m_") {
       string pkgName;
       if (libraryName != null) {
         pkgName = libraryName;
@@ -177,7 +181,7 @@ private Import CreateImport(string moduleName, bool isDefault, ModuleDefinition
       }
 
 
-      return new Import { Name = moduleName, Path = pkgName, ExternModule = externModule };
+      return new Import { Name = namePrefix + moduleName, Path = pkgName, ExternModule = externModule };
     }
 
     protected override bool ShouldCompileModule(Program program, ModuleDefinition module) {
@@ -192,7 +196,7 @@ protected override bool ShouldCompileModule(Program program, ModuleDefinition mo
       return true;
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
       ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       if (isDefault) {
@@ -209,13 +213,14 @@ protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDef
         }
       }
       ModuleName = PublicModuleIdProtect(moduleName);
-      var import = CreateImport(ModuleName, isDefault, externModule, libraryName);
+      CurrentModule = module;
+      var import = CreateImport(ModuleName, externModule, libraryName);
       var filename = string.Format("{0}/{0}.go", import.Path);
       var w = wr.NewFile(filename);
       EmitModuleHeader(w);
 
       import.Path = goModuleName + import.Path;
-      AddImport(import);
+      AddImport(module, import);
 
       return w;
     }
@@ -254,20 +259,26 @@ protected override void DependOnModule(Program program, ModuleDefinition module,
       }
 
       var publicModuleName = PublicModuleIdProtect(module.GetCompileName(Options));
-      var import = CreateImport(publicModuleName, module.IsDefaultModule, externModule, libraryName);
+      var import = CreateImport(publicModuleName, externModule, libraryName);
       import.Path = goModuleName + import.Path;
-      AddImport(import);
+      AddImport(module, import);
     }
 
     protected override void FinishModule() {
       ModuleName = MainModuleName;
     }
 
-    private void AddImport(Import import) {
+    private void AddImport(ModuleDefinition module, Import import) {
       // Import in root module
       EmitImport(import, RootImportWriter, RootImportDummyWriter);
       // Import in all subsequent modules
       Imports.Add(import);
+      ModuleImports[module] = import;
+      var implemented = module.GetImplementedModule();
+      while (implemented != null) {
+        ModuleImports[implemented] = import;
+        implemented = implemented.GetImplementedModule();
+      }
     }
 
     private void EmitImport(Import import, ConcreteSyntaxTree importWriter, ConcreteSyntaxTree importDummyWriter) {
@@ -2684,7 +2695,12 @@ private string UserDefinedTypeName(UserDefinedType udt, bool full, MemberDecl/*?
     }
 
     private string UserDefinedTypeName(TopLevelDecl cl, bool full, MemberDecl/*?*/ member = null) {
-      var enclosingModuleDefinitionId = PublicModuleIdProtect(cl.EnclosingModuleDefinition.GetCompileName(Options));
+      string enclosingModuleDefinitionId;
+      if (CurrentModule == cl.EnclosingModuleDefinition || cl.EnclosingModuleDefinition.IsDefaultModule) {
+        enclosingModuleDefinitionId = cl.EnclosingModuleDefinition.GetCompileName(Options);
+      } else {
+        enclosingModuleDefinitionId = ModuleImports[cl.EnclosingModuleDefinition].Name;
+      }
       if (IsExternMemberOfExternModule(member, cl)) {
         // omit the default class name ("_default") in extern modules, when the class is used to qualify an extern member
         Contract.Assert(!cl.EnclosingModuleDefinition.IsDefaultModule);  // default module is not marked ":extern"

Source/DafnyCore/Backends/Java/JavaCodeGenerator.cs

@@ -379,7 +379,8 @@ string IdProtectModule(string moduleName) {
       return string.Join(".", moduleName.Split(".").Select(IdProtect));
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtectModule(moduleName);
       if (isDefault) {

Source/DafnyCore/Backends/JavaScript/JavaScriptCodeGenerator.cs

@@ -63,7 +63,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return wr.NewBlock($"static Main({argsParameterName})");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       moduleName = IdProtect(moduleName);
       if (externModule == null || libraryName != null) {

Source/DafnyCore/Backends/Python/PythonCodeGenerator.cs

@@ -98,7 +98,8 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
       return mw.NewBlockPy($"def StaticMain({argsParameterName}):");
     }
 
-    protected override ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
       var pythonModuleName = PythonModuleMode ? PythonModuleName + "." : "";
 

Source/DafnyCore/Backends/SinglePassCodeGenerator/SinglePassCodeGenerator.cs

@@ -187,7 +187,8 @@ protected virtual bool ShouldCompileModule(Program program, ModuleDefinition mod
       return module.ShouldCompile(program.Compilation);
     }
 
-    protected abstract ConcreteSyntaxTree CreateModule(string moduleName, bool isDefault, ModuleDefinition externModule,
+    protected abstract ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
+      ModuleDefinition externModule,
       string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr);
     /// <summary>
     /// Indicates the current program depends on the given module without creating it.
@@ -1590,7 +1591,7 @@ private void EmitModule(Program program, ConcreteSyntaxTree programNode, ModuleD
 
       Contract.Assert(enclosingModule == null);
       enclosingModule = module;
-      var wr = CreateModule(module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
+      var wr = CreateModule(module, module.GetCompileName(Options), module.IsDefaultModule, externModule, libraryName, module.Attributes, programNode);
       var v = new CheckHasNoAssumes_Visitor(this, wr);
       foreach (TopLevelDecl d in module.TopLevelDecls) {
         if (!ProgramResolver.ShouldCompile(d)) {

Source/IntegrationTests/TestFiles/LitTests/LitTest/comp/moduleDatatypeNameCollision/moduleDatatypeNameCollision.dfy.expect

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