Dafny中如何在模块细化内细化抽象模块？报错求助

在TLA+中尝试细化抽象模块Model的子模块Inputs时，触发如下报错：

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

对应的代码示例：

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]
    }
  }
}

报错核心原因是：细化父模块中已存在的子模块时，不能直接用refines指向最原始的抽象模块，必须明确声明当前子模块是细化父模块里的对应子模块，使用refining(...)语法。

修改后的正确代码：

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 refining(Model!Inputs) {
    type T = bool
    const length: nat := 1
    function tobits(i: T): (r: seq<bool>)
    {
      [i]
    }
  }
}

• refining(Model!Inputs)明确告知TLA+，当前ModelX中的Inputs子模块是对Model模块内Inputs子模块的细化，而非直接重新细化Flattenable。
• 由于Model里的Inputs已经继承了Flattenable的抽象约束，只需要在ModelX的Inputs中实现具体内容即可，无需再次声明refines Flattenable。

内容的提问来源于stack exchange，提问作者Ben Reynwar