The Coq mailing list

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

Hi Xavier,

Thanks for your reply.

On 2019-10-30 14:19, Xavier Leroy wrote:
> Structurally equal types are equal.  What you mean is "two inductive types 
> that have the same constructors with the same argument types", and the 
> answer is no, it is not possible.

Thanks for the clarification.

> Not exactly what you describe, but "Extract Constant" and "Extract 
> Inductive" could help.
> Consider:
> 
> Inductive t := A | B (n: nat) | C (b: bool).
> Extract Inductive t => "Lib.t" [ "Lib.A" "Lib.B" "Lib.C" ].
> 
> Then, t will be defined as an abbreviation for Lib.t, and the code for f 
> will use constructors prefixed with Lib.  That might do what you want.

The problem with this strategy is that I need to do the same trick not just 
on `t`, but on any types used by `t`; otherwise the generated code will apply 
Lib.B to its own copy of nat, rather than the one in the original library, 
and OCaml will reject the application.

So, in your example, I'd need to add extraction commands for `nat` and `bool` 
as well.  In my case the types used in the ASTs are more complex, and that 
task will introduce a mess of had-to-maintain extraction commands :/

>     * Add unsafe casts and hope for the best, which I think should work 
> fine, but won't detect issues like version mismatches between the FooBarBaz 
> library used on the OCaml and the FooBar library used on the Coq side.
> 
> Hmph.  What's the point of proving code if you're adding unsafe casts in 
> the end?

The extracted code is already full of Obj.magic, whose justification is 
meta-theoretical, to pacify the OCaml typechecker; wouldn't these be of a 
similar nature?

> Don't use unsafe casts :-)

Is there any way to make them safer? For example, can I use compiler 
libraries to ensure that the two types are the same?

Hopefully I've been doing this all wrong, and there's an obvious solution 
that I've missed ^^
Clément.