Coq Module Extraction Issue (ocaml extraction bug?) · Coq users

I've put together a small example of a problem I'm encountering with ocaml extraction in Coq, and I'm wondering if anybody has any insight.

The gist of it is that I have some modules set up in Coq, but when I go to extract these modules to ocaml I get a .mli file with a type error.

File "ml/extracted/MyModules.mli", lines 243-244, characters 8-41:
243 | ........type value_byte = MEM'.Byte.value_byte =
244 |         | ExtractByte of LP.V.value * nat
Error: This variant or record definition does not match that of type
         MEM'.Byte.value_byte
       Constructors do not match:
         ExtractByte of LP'.V.value * Datatypes.nat
       is not the same as:
         ExtractByte of LP.V.value * Datatypes.nat
       The type LP'.V.value is not equal to the type LP.V.value

I believe the interesting part of the Coq file is contained within this snippet:

Module Type Memory (LP: LanguageParams).
  Import LP.
  Import V.

  Module Byte := MakeByte LP.
End Memory.

Module MakeMemory (LP : LanguageParams) <: Memory LP.
  Include Memory LP.
End MakeMemory.

Module Type Lang (LP: LanguageParams).
  Export LP.

  (* Memory *)
  Declare Module MEM : Memory LP.
  Export MEM.
End Lang.

Module Make_Lang (LP : LanguageParams) (MEM' : Memory LP) <: Lang LP
with Module MEM := MEM'.
  Include Lang LP with Module MEM := MEM'.
End Make_Lang.

Module Type InterpreterStack_common (LP : LanguageParams) (MEM : Memory LP).
  (* Lang seems to be necessary to cause the bug *)
  Module Language := Make_Lang LP MEM.

  Import LP.V.
End InterpreterStack_common.

Module Type InterpreterStack.
  Declare Module LP : LanguageParams.
  Declare Module MEM : Memory LP.
  Include InterpreterStack_common LP MEM.
End InterpreterStack.

Module Make_InterpreterStack (LP' : LanguageParams) (MEM' : Memory LP') <: InterpreterStack
with Module LP := LP' with Module MEM := MEM'.
  Include InterpreterStack with Module LP := LP' with Module MEM := MEM'.
End Make_InterpreterStack.

It seems like the problem might have something to do with Declare Module and using with Module in the Make_InterpreterStack module. It seems like when the ocaml mli gets extracted it loses the information that the LP module in Make_InterpreterStack should be the same as LP'?

Does anybody have any idea what's going on? Because this works in Coq, I assume it's an ocaml extraction bug, but are there any workarounds for this issue? Currently we're manually patching the .mli files with sed, but these patches are kind of fragile and annoying, and it would be great if we didn't have to do them, or at least better understood what caused the problem in the first place!

Karl Palmskog (Oct 23 2022 at 12:02):

I'm not familiar with any workarounds besides modifying the extracted .mli via something like sed. The next generation of extraction will probably target a lower level OCaml interface though, so then the problem likely goes away (see for example this)

Calvin Beck (Oct 25 2022 at 00:45):

Thanks for the response! Glad it's a known issue and I'm not alone, at least. Hopefully the future work you pointed to ends up resolving this so we can have fewer load bearing Perl and sed scripts :sweat_smile:.

Stream: Coq users

Topic: Coq Module Extraction Issue (ocaml extraction bug?)

Calvin Beck (Oct 21 2022 at 17:37):

Karl Palmskog (Oct 23 2022 at 12:02):

Calvin Beck (Oct 25 2022 at 00:45):