Coq for OCaml-extraction of algebraic types

Question

When I retrieve the following Coq data types in OCaml:

Inductive Foo := | A | B.
Inductive Bar (f:Foo) := | C | D.
Extraction Language Ocaml.
Extraction "test.ml" Foo Bar.

I get the following ML code:

type foo =
| A
| B

type bar =
| C
| D

The type "bar" is different from Coq because it has an "f" as part of its type signature.

What is the best way to define types so that they are well retrievable for OCaml?

Answer 1

You cannot: OCaml does not support indexing types by urgent values, and as a result, things like Bar Athat do not make sense. Coq is forced to erase additional indexes so that the definitions are compatible with a system like OCaml.