This repository contains a fairly minimal example of a problem I’m encountering with the Coq module system with ocaml extraction.

The code I have works in Coq, but upon extraction I get compilation errors with ocaml like the following:

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

Should be able to just:

cd src
make extracted

To see the error. There are no dependencies beyond Coq and coq_makefile.

If you use nix, this project has a flake that you can use to get the same versions of Coq as me (8.16). Running nix build -L . should try to build the project and give you a build log.

The issue seems to arise because of the Module Language := Make_Lang LP MEM line in InterpreterStack_common. It seems like the mixture of having a module like Byte in the Module Type Memory and the Declare Module MEM : Memory LP results in an incorrect module interface getting extracted. The ocaml .mli file has this:

module Make_InterpreterStack :
 functor (LP':LanguageParams) ->
 functor (MEM':sig
  module Byte :
   sig
    type value_byte =
    | ExtractByte of LP'.V.value * nat

    val value_byte_rect : (LP'.V.value -> nat -> 'a1) -> value_byte -> 'a1

    val value_byte_rec : (LP'.V.value -> nat -> 'a1) -> value_byte -> 'a1
   end
 end) ->
 sig
  module LP :
   LanguageParams

  module MEM :
   sig
    module Byte :
     sig
      type value_byte = MEM'.Byte.value_byte =
      | ExtractByte of LP'.V.value * nat

      val value_byte_rect : (LP'.V.value -> nat -> 'a1) -> value_byte -> 'a1

      val value_byte_rec : (LP'.V.value -> nat -> 'a1) -> value_byte -> 'a1
     end
   end

  module Language :
   sig
    module MEM :
     sig
      module Byte :
       sig
        type value_byte = MEM'.Byte.value_byte =
        | ExtractByte of LP.V.value * nat

        val value_byte_rect : (LP.V.value -> nat -> 'a1) -> value_byte -> 'a1

        val value_byte_rec : (LP.V.value -> nat -> 'a1) -> value_byte -> 'a1
       end
     end
   end
 end

And the problem seems to be that the Language module ends up using LP.V.value from the LP module declared here:

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

But it doesn’t know that this LP = LP'. Coq itself seems to be okay with this arrangement of modules, but it doesn’t work when extracted.

Interestingly the MEM module seems to use LP'.V.value directly… I guess that might be because it gets defined using with Module MEM := MEM'. Thus must act differently behind the scenes?