3

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?

Anton Trunov
  • 15,074
  • 2
  • 23
  • 43
Konstantin Weitz
  • 6,180
  • 8
  • 26
  • 43

1 Answers1

3

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".
flockshade
  • 46
  • 1