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