Abstract import of concrete module is allowed, produces invalid target code

[ssomayyajula]

Dafny version

latest

Code to produce this issue

module Concrete {
  method DoNothing() { }
}

abstract module Abstract {
  import C: Concrete
}

module MoreConcrete refines Abstract {

}

method Main() {
  MoreConcrete.C.DoNothing();
}

Command to run and resulting output

dafny run ...

error CS0103: The name 'Abstract' does not exist in the current context

What happened?

The abstract import of a concrete module should be disallowed.

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

Mac