ハマる

Coq の Module の Inline ディレクティブに関連して理解不能なエラーにハマった．下のコードがハマった部分を抜き出したもの．

Module Type A. End A.
Module Type B  (a : A). 
  Parameter t : Type.
End B.
Module Type Bi (a : A). 
  Parameter Inline(10) t : Type.
End Bi.
Module C  (b : B).  End C.
Module Ci (b : Bi). End Ci.
 
Module CX (b : B) (bi : Bi).
  (* These two work well.*)
  Module Cb := C b.
  Module Cbi := C bi. 
  (* These two work well too, using `!' to ignore the Inline directive. "*)  
  Module Cib := !Ci b.
  Module Cibi := !Ci bi.
  (* This fails with saying "Error: The field t is missing in Top.b."*)  
  Module Cib2 := Ci b.
  (* This fails with saying "Error: The field t is missing in Top.bi."*)  
  Module Cibi2 := Ci bi.
End CX.

ファンクタ B と Bi は Print Module Type で見ても名前以外は同じ．ファンクタ C と Ci はファンクタ B と Bi をとる．んで，この C と Ci に B と Bi の型の b と bi を適用してみると，Inline を付けた定義の Bi を受け取るという定義の Ci に関してよくわからんエラーが出る．b も bi も t というフィールドを持っているのにそれが無いとか言われ……　

とりあえず ! 付けて Inline を無視させればエラーでないということは学習した．でも Inline の意味はよくわからん．