Refining modules inside a module refinement in Dafny?

Question

I'm trying to refine an abstract module inside the refinement of an abstract module, but am having trouble working out how to do it.

I get the following error

to redeclare and refine declaration 'Inputs' from module 'Model', you must use the refining (...)

for the following code

abstract module Flattenable {
  const length: nat
  type T
  function tobits(i: T): (r: seq<bool>)
    ensures |r| == length
}

abstract module Model {
  module Inputs refines Flattenable {}
}

module ModelX refines Model {
  module Inputs refines Flattenable {
         ^^^^^^
    type T = bool
    const length: nat := 1
    function tobits(i: T): (r: seq<bool>)
    {
      [i]
    }
  }
}

Answer 1

What I needed to do was define the internal abstract module as an import i.e. import Inputs : Flattenable. This information was in the reference manual in the Module Abstraction section.

abstract module Flattenable {
  const length: nat
  type T
  function tobits(i: T): (r: seq<bool>)
    ensures |r| == length
}

abstract module Model {
  import Inputs : Flattenable
}

module ModelX refines Model {
  module Inputs refines Flattenable {
    type T = bool
    const length: nat := 1
    function tobits(i: T): (r: seq<bool>)
    {
      [i]
    }
  }
}