The Coq mailing list

[Thomas Braibant <thomas.braibant AT gmail.com>]

Hi List,

While trying to extract my development (using Extraction Library), I
ended up with the following error message

Error: The informative inductive type sig has a Prop instance.
This happens when a sort-polymorphic singleton inductive type
has logical parameters, such as (I,I) : (True * True) : Prop.
The Ocaml extraction cannot handle this situation yet.
Instead, use a sort-monomorphic type such as (True /\ True)
or extract to Haskell.

After I located the module that generated this error message (linear
search over the modules I use doing Extraction Library Foo), I
realized that [sig] was not used in the module (I only use [sigT] in
my development). Yet, in some proofs, I used the following lemma
EqdepFacts.eq_sigT_sig_eq:
  forall (X : Type) (P : X -> Type) (x1 x2 : X) (H1 : P x1) (H2 : P x2),
  existT P x1 H1 = existT P x2 H2 <->
  {H : x1 = x2 | eq_rect x1 P H1 x2 H = H2}

When I replaced all occurences of this lemmas in my proofs with a
combination of EqdepTheory.inj_pair2 and EqdepFacts.eq_sigT_fst, the
extraction went through.

What happened? Well, it appears that in order to get working code from
extraction, I need to set the (v8.4) option Set Extraction
AccessOpaque. Otherwise, a few lemmas like
List.exists_last : forall l, l <> [] -> { l' : (list A) & { a : A | l
= l' ++ [a]}}
(from the standard library) get extracted to something like
let exists_last = failwith "AXIOM TO BE REALIZED"
(which makes the generated code impossible to run, because this raises an 
error)

Therefore, my "proof" that used some instance of sig inside was
extracted! And, changing the proof made the problem disappear.

But, of course, what I really wanted was the new (8.4) Separate
Extraction command, that hits a sweet spot between Extraction Library
(that extracts even the lemmas),  and Recursive Extraction. And now
everything works fine.  So I decided to share the story, in case
somebody gets bitten by the same thing in the near future.

Thomas