A good example is worth a thousand words:

module Sig
  type t = private mutable {}

  val f (t: t) : int
    writes { t }
end

module Impl
  use import int.Int

  type t = { mutable size: int }

  let f (t: t) : int
    writes  { t }
    ensures { result = (old t).size }
    ensures { t.size = (old t).size + 1 }
  = let x = t.size in t.size <- t.size + 1;
    x

  clone Sig with type t = t, val f = f
end

In order for this clone to succeed, we need to add the field
[size] to the [writes] of the cloned val [f].
In the general case, we add all of the new mutable fields of
a refinement type to [writes] clause of the cloned function
(even if their values are not changed by the function execution).

FIXME: fix the case in which the type to be refined is already
declared with some mutable fields.