I'm trying to extract some file system code that I've written in Coq. I want to replace my FileIO Monad with Haskell's IO Monad. My code looks like this:
Variable FileIO : Type -> Type.
Variable sync : FileIO unit.
Extract Inlined Constant sync => "synchronize".
Extract Inlined Constant FileIO => "IO".
Recursive Extraction append.
Replacing sync is no problem, but when I try to replace FileIO with IO I get the following error:
Error: The type scheme axiom FileIO needs 1 type variable(s).
What does this error mean, and how can I get around it?
It's probably a limitation. You need to provide an argument to FileIO and you're not allowed to inline it.
Extract Constant FileIO "x" => "IO x".