Merge PR #13624: Fixing #13581: missing support for let-ins in arity of inductive types for extraction

Reviewed-by: pi8027

3 files changed, 71 insertions, 4 deletions

diff --git a/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst
new file mode 100644
index 0000000000..6a34f5a70e
--- /dev/null
+++ b/doc/changelog/08-cli-tools/13624-master+fix13581-extraction-letin-in-ind-arity.rst
@@ -0,0 +1,6 @@
+- **Fixed:**
+  Failure of extraction in the presence of inductive types with local
+  definitions in parameters
+  (`#13624 <https://github.com/coq/coq/pull/13624>`_,
+  fixes `#13581 <https://github.com/coq/coq/issues/13581>`_,
+  by Hugo Herbelin).
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index ca4f5429a2..30f90dd1fc 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -427,6 +427,7 @@ and extract_really_ind env kn mib =
     (* Everything concerning parameters. *)
     (* We do that first, since they are common to all the [mib]. *)
     let mip0 = mib.mind_packets.(0) in
+    let ndecls = List.length mib.mind_params_ctxt in
     let npar = mib.mind_nparams in
     let epar = push_rel_context mib.mind_params_ctxt env in
     let sg = Evd.from_env env in
@@ -462,17 +463,17 @@ and extract_really_ind env kn mib =
       if not p.ip_logical then
         let types = arities_of_constructors env ((kn,i),u) in
         for j = 0 to Array.length types - 1 do
-          let t = snd (decompose_prod_n npar types.(j)) in
+          let t = snd (decompose_prod_n_assum ndecls types.(j)) in
           let prods,head = dest_prod epar t in
           let nprods = List.length prods in
           let args = match Constr.kind head with
             | App (f,args) -> args (* [Constr.kind f = Ind ip] *)
             | _ -> [||]
           in
-          let dbmap = parse_ind_args p.ip_sign args (nprods + npar) in
-          let db = db_from_ind dbmap npar in
+          let dbmap = parse_ind_args p.ip_sign args (nprods + ndecls) in
+          let db = db_from_ind dbmap ndecls in
           p.ip_types.(j) <-
-            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (npar+1)
+            extract_type_cons epar sg db dbmap (EConstr.of_constr t) (ndecls+1)
         done
     done;
     (* Third pass: we determine special cases. *)
diff --git a/test-suite/bugs/closed/bug_13581.v b/test-suite/bugs/closed/bug_13581.v
new file mode 100644
index 0000000000..910537cf11
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13581.v
@@ -0,0 +1,60 @@
+From Coq Require Extraction.
+
+Record mixin_of T0 (b : unit) (T := T0) := Mixin { _ : T0 -> let U:=T0 in U }.
+Definition d := Mixin nat tt (fun x => x).
+
+Extraction TestCompile d.
+
+(* Extra tests *)
+
+Record R T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) := Build
+  { g : T0 -> let U:=T0 in U ; h : d = d ; x : nat ; y := x+x }.
+
+Definition r := {| g := (fun x : nat => x) ; h := eq_refl (eq_refl 0) ; x := 0 |}.
+
+Extraction TestCompile r.
+(*
+(** val r0 : nat r **)
+
+let r0 =
+  { g = (fun x0 -> x0); x = O }
+*)
+
+Inductive I T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall d (e:=S d) (h : S d = e), Type :=
+| C : I T a b 0 eq_refl
+| D : J T a b true eq_refl -> I T a b 1 eq_refl
+with J T (a:T) (U:=T) (b:T) (c:=(a,b)) : forall (d:bool) (h:d = true), Type :=
+| E : I T a b 0 eq_refl -> J T a b true eq_refl.
+
+Definition c := D _ _ _ (E _ _ _ (C nat 0 0)).
+
+Extraction TestCompile c.
+
+(*
+(** val c : nat i **)
+
+let c =
+  D (E C)
+*)
+
+CoInductive V T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { k : T; b := c+e ; m : nat; z : option (W nat 0 0 eq_refl) }
+with W T0 (b:nat) (c:=b) (T:=T0) (e:nat) (d:c=e) :=
+  { l : V nat 0 0 eq_refl }.
+
+CoFixpoint v :=
+  {| k := 0 ; m := 0 ; z := Some w ; |}
+with w := {| l := v |}.
+
+Extraction TestCompile v.
+(*
+(** val v0 : nat v **)
+
+let rec v0 =
+  lazy (Build_V (O, O, (Some w0)))
+
+(** val w0 : nat w **)
+
+and w0 =
+  lazy (Build_W v0)
+*)