From a81c2de033b37c22be1ca6794ab32347a9917610 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 17 Nov 2019 09:39:50 +0100
Subject: Fixing bugs in the computation of implicit arguments for fix with a
 let binder.

---
 ...32-master+fix-implicit-let-fixpoint-bug3282.rst |  1 +
 interp/constrintern.ml                             |  4 +++-
 interp/implicit_quantifiers.ml                     |  6 +++++-
 test-suite/bugs/closed/bug_3282.v                  | 22 ++++++++++++++++++++++
 4 files changed, 31 insertions(+), 2 deletions(-)
 create mode 100644 doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst

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..3ee3444c60
--- /dev/null
+++ b/doc/changelog/02-specification-language/11132-master+fix-implicit-let-fixpoint-bug3282.rst
@@ -0,0 +1 @@
+- Fixed bugs sometimes preventing to define valid (co)fixpoints with implicit arguments in the presence of local definitions, see #3282 (`#11132 <https://github.com/coq/coq/pull/11132>`_, by Hugo Herbelin).
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index f2cb4ae5c7..f420637e3f 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 455471a472..4301242fd9 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).
-- 
cgit v1.2.3