coq - タイプスキームの抽出

Question

Coq で書いたファイル システム コードを抽出しようとしています。FileIOモナドを Haskell のモナドに置き換えたいIO。私のコードは次のようになります。

Variable FileIO : Type -> Type.
Variable sync : FileIO unit.

Extract Inlined Constant sync => "synchronize".
Extract Inlined Constant FileIO => "IO".

Recursive Extraction append.

置換syncは問題ありませんが、置換しようとするとFileIO次IOのエラーが発生します。

Error: The type scheme axiom  FileIO needs 1 type variable(s).

このエラーは何を意味し、どうすれば回避できますか?