Resolver falsely flags import of compiled module as abstract

[ssomayyajula]

Dafny version

latest

Code to produce this issue

abstract module Base { }

abstract module Parent {
  import Child: Base
}

abstract module RenamedBase refines Base {
  // renames members of Base for my domain
}

// analogous to RenamedBase
abstract module RenamedParent {
  import RenamedChild: RenamedBase
  import Child = RenamedChild
}

module ConcreteBase1 refines Base { }

module ConcreteParent1 refines Parent {
  import Child = ConcreteBase1
}

module ConcreteBase2 refines RenamedBase { }

module ConcreteParent2 refines RenamedParent {
  // Error: a compiled module (ConcreteParent2) is not allowed to import an abstract module (RenamedChild)
  import RenamedChild = ConcreteBase2
}

Command to run and resulting output

dafny verify --type-system-refresh

What happened?

The reported error does not occur for ConcreteParent1 but for ConcreteParent2, which implies that the resolver does not consider transitive imports of compiled modules as compiled, even though it should (of course, Child cannot be re-imported).

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

Mac

[RustanLeino]

Yes, that's a bug. Thanks for finding and reporting it.