Merge PR #11132: Fixing bugs in the computation of implicit arguments for `Fixpoint` with a let binder

Reviewed-by: Zimmi48
Reviewed-by: ejgallego

4 files changed, 43 insertions, 2 deletions

diff --git a/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
new file mode 100644
index 0000000000..f8298cdbdd
--- /dev/null
+++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
@@ -0,0 +1,13 @@
+- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments
+  in the presence of local definitions, see `#3282 <https://github.com/coq/coq/issues/3282>`_
+  (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin).
+
+  .. example::
+
+     The following features an implicit argument after a local
+     definition. It was wrongly rejected.
+
+     .. coqtop:: in
+
+        Definition f := fix f (o := true) {n : nat} m {struct m} :=
+          match m with 0 => 0 | S m' => f (n:=n+1) m' end.
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 57e2214293..ff115a3e48 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1872,7 +1872,8 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
         (* We add the recursive functions to the environment *)
         let env_rec = List.fold_left_i (fun i en name ->
            let (_,bli,tyi,_) = idl_temp.(i) in
-           let fix_args = (List.map (fun (na, bk, _, _) -> build_impls bk na) bli) in
+           let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
+           let fix_args = List.map (fun (na, bk, t, _) -> build_impls bk na) bli in
            push_name_env ntnvars (impls_type_list ~args:fix_args tyi)
            en (CAst.make @@ Name name)) 0 env lf in
         let idl = Array.map2 (fun (_,_,_,_,bd) (n,bl,ty,before_impls) ->
@@ -1903,6 +1904,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
             (bl,intern_type env' ty,bl_impls)) dl in
         let env_rec = List.fold_left_i (fun i en name ->
           let (bli,tyi,_) = idl_tmp.(i) in
+          let bli = List.filter (fun (_, _, t, _) -> t = None) bli in
           let cofix_args =  List.map (fun (na, bk, _, _) -> build_impls bk na) bli in
           push_name_env ntnvars (impls_type_list ~args:cofix_args tyi)
             en (CAst.make @@ Name name)) 0 env lf in
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml
index 77a2c1c8e6..8b457ab37b 100644
--- a/interp/implicit_quantifiers.ml
+++ b/interp/implicit_quantifiers.ml
@@ -219,6 +219,10 @@ let implicits_of_glob_constr ?(with_products=true) l =
     | GLetIn (na, b, t, c) -> aux c
     | GRec (fix_kind, nas, args, tys, bds) ->
       let nb = match fix_kind with |GFix (_, n) -> n | GCoFix n -> n in
-      List.fold_right (fun (na,bk,t,_) l -> add_impl ?loc:c.CAst.loc na bk l) args.(nb) (aux bds.(nb))
+      List.fold_right (fun (na,bk,t,_) l ->
+          match t with
+          | Some _ -> l
+          | _ -> add_impl ?loc:c.CAst.loc na bk l)
+        args.(nb) (aux bds.(nb))
     | _ -> []
   in aux l
diff --git a/test-suite/bugs/closed/bug_3282.v b/test-suite/bugs/closed/bug_3282.v
index ce7cab1cba..f32e0969c8 100644
--- a/test-suite/bugs/closed/bug_3282.v
+++ b/test-suite/bugs/closed/bug_3282.v
@@ -5,3 +5,25 @@ Definition foo := fix f (m : nat) (o := true) (n : nat) {struct n} :=
 
 Fixpoint f (m : nat) (o := true) (n : nat) {struct n} :=
   match n with 0 => 0 | S n' => f 0 n' end.
+
+Definition foo' := fix f {m : nat} (o := true) (n : nat) {struct n} :=
+  match n with 0 => 0 | S n' => f (m:=0) n' end.
+Check foo' (m:=0) 0.
+
+Fixpoint f' {m : nat} (o := true) (n : nat) {struct n} :=
+  match n with 0 => 0 | S n' => f' (m:=0) n' end.
+Check f' (m:=0) 0.
+
+CoInductive Stream := { hd : nat; tl : Stream }.
+
+Definition cofoo := cofix f (o := true) {m} := {| hd := 0; tl := f (m:=0) |}.
+Check cofoo (m:=0).
+
+CoFixpoint cof (o := true) {m} := {| hd := 0; tl := cof (m:=0) |}.
+Check cof (m:=0).
+
+Definition cofoo' := cofix f {m} (o := true) := {| hd := 0; tl := f (m:=0) |}.
+Check cofoo' (m:=0).
+
+CoFixpoint cof' {m} (o := true) := {| hd := 0; tl := cof' (m:=0) |}.
+Check cof' (m:=0).