CODEWITHSUNDEEP
coqcoq-extraction
Konstantin Weitz
Konstantin Weitz

Reputation: 6432

Extraction of Type Scheme

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?

Upvotes: 3

Views: 134

Answers (1)

flockshade
flockshade

Reputation: 46

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".

Upvotes: 3

Related Questions