Concrete import inside abstract module produces malformed code under refinement

[ssomayyajula]

Dafny version

latest

Code to produce this issue

// lib.dfy
module Library {
  abstract module Abstract {
    predicate ImplementThis()
  }

  module Concrete {
    predicate Something() { true }
  }

  abstract module ExtendedAbstract refines Abstract {
    import C: Concrete

    predicate Compute() {
      C.Something() && ImplementThis()
    }
  }
}

// main.dfy
module Driver refines Library.ExtendedAbstract {
  predicate ImplementThis() { true }
}

method Main() {
  print Driver.Compute();
}

# dfyconfig.toml
includes = ["main.dfy", "lib.dfy"]

Command to run and resulting output

> dafny build --target:cs dfyconfig.toml

Failed to compile C# source code using 'dotnet build .../lib.csproj -o ...'. Command output was:
  Determining projects to restore...
  All projects are up-to-date for restore.
.../lib.cs(5746,15): error CS0103: The name 'Library__mExtendedAbstract' does not exist in the current context [.../lib.csproj]

Build FAILED.

.../lib.cs(5746,15): error CS0103: The name 'Library__mExtendedAbstract' does not exist in the current context [.../lib.csproj]
    0 Warning(s)
    1 Error(s)

What happened?

If you look at lib.cs, the compiled Driver module is making references to Library__mExtendedAbstract.C when it should just be making references to C or Concrete. The guarantee that abstract modules disappear at compile time isn't holding.

What type of operating system are you experiencing the problem on?

Mac

[ssomayyajula]

Closing this b/c import C: Concrete is actually an abstract import, not a concrete import. However, this is still a bug - the program should be rejected.

[keyboardDrummer]

However, this is still a bug - the program should be rejected.

Why not repurpose this ticket for reporting that bug?