Extraction generates invalid code for primitive records in functors

[JasonGross]

Description of the problem

Module Type Nop. End Nop.
Module Empty. End Empty.
Module M (N : Nop).
  Local Set Primitive Projections.
  Record M_t_NonEmpty elt := { M_m :> list elt }.
End M.
Module M' := M Empty.
Require Import Coq.extraction.Extraction.
Require Import Coq.extraction.ExtrOcamlBasic.
Extraction Language OCaml.
Recursive Extraction M'.
(*
module type Nop =
 sig
 end

module Empty =
 struct
 end

module M =
 functor (N:Nop) ->
 struct
  type 'elt coq_M_t_NonEmpty = 'elt list
    (* singleton inductive, whose constructor was Build_M_t_NonEmpty *)

  (** val coq_M_m : 'a1 coq_M_t_NonEmpty -> 'a1 list **)

  let coq_M_m =
    coq_M_m
 end

module M' = M(Empty)

*)
Extraction TestCompile M'.
(* Error: Unbound value coq_M_m *)

Coq Version

8.14.0

[herbelin]

Problem was a standard one: the code was relying on a imperative state which is unknown when inside a functor, leading to a self-referencing extraction.

Fixed in #17321.