The Coq mailing list

[Clément Pit-Claudel <cpitclaudel AT gmail.com>]

On 2019-10-31 11:02, Xavier Leroy wrote:
> You're right, this trick must be applied to all inductive types in your 
> hierarchy.  It is a maintenance burden, indeed.  But at least you should 
> get meaningful errors when something is wrong (missing or wrong Extract 
> Inductive command).

> [...]  For the casts inserted by extraction, type soundness was checked by 
> the Coq type-checker.  In other words, the extracted code is type-safe, 
> just not typeable in OCaml because its type system is too weak.  So, 
> assuming extraction is sound and OCaml compiles correctly in the presence 
> of Obj.magic, you can feel reasonably safe about these casts.

Well, you also need to assume that your Extract Inductive commands are sound, 
too — and you don't always get an error message: because of the Obj.magic 
that the compiler introduces, your ill-typed extraction command can silently 
go through and lead to a crash.  Arguably that's not likely, but I've seen it 
happen :/

On the other hand, and additional Obj.magic that converts between two copies 
of (what should be) the same type can only go wrong if you're using an OCaml 
library that's inconsistent with the Coq one; that can't happen if both are 
packaged in distributed together, right?

So we're looking at a problem that would only bite developers trying to 
compile a Foo program written against an copy of the Coq sources using a 
compiler linked against a different copy of the Coq sources, which sounds 
like a fairly nice issue.

Clément.