Merge PR #12893: Fix incorrect debruijn handling when Record calls maybe_unify_params_in

Reviewed-by: maximedenes

5 files changed, 33 insertions, 9 deletions

diff --git a/test-suite/output/bug_12887.out b/test-suite/output/bug_12887.out
new file mode 100644
index 0000000000..5ea7722bc6
--- /dev/null
+++ b/test-suite/output/bug_12887.out
@@ -0,0 +1,10 @@
+The command has indeed failed with message:
+Cannot infer this placeholder of type "Type" in
+environment:
+Functor : (Type -> Type) -> Type
+F : Type -> Type
+fmap : forall A B : Type, (A -> B) -> F A -> F B
+The command has indeed failed with message:
+Cannot infer an existential variable of type "nat" in
+environment:
+R : nat -> Type
diff --git a/test-suite/output/bug_12887.v b/test-suite/output/bug_12887.v
new file mode 100644
index 0000000000..4208c3e8e9
--- /dev/null
+++ b/test-suite/output/bug_12887.v
@@ -0,0 +1,10 @@
+Arguments id {_} _.
+
+Fail Record Functor (F : Type -> Type) := {
+  fmap : forall A B, (A -> B) -> F A -> F B;
+  fmap_identity : fmap _ _ id = id;
+}.
+
+Fail Inductive R (x:nat) := { y : R ltac:(clear x) }.
+
+Inductive R (x:nat) := { y : bool; z : R _ }.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 673124296d..452de69b1d 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -451,7 +451,7 @@ let interp_params env udecl uparamsl paramsl =
    do the unification.
    [env_ar_par] is [uparams; inds; params]
  *)
-let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
+let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams ~binders:k c =
   let is_ind sigma k c = match EConstr.kind sigma c with
     | Constr.Rel n ->
       (* env is [uparams; inds; params; k other things] *)
@@ -462,14 +462,18 @@ let maybe_unify_params_in env_ar_par sigma ~ninds ~nparams c =
     | Constr.App (h,args) when is_ind sigma k h ->
       Array.fold_left_i (fun i sigma arg ->
           if i >= nparams || not (EConstr.isEvar sigma arg) then sigma
-          else Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i)))
+          else begin try Evarconv.unify_delay env sigma arg (EConstr.mkRel (k+nparams-i))
+            with Evarconv.UnableToUnify _ ->
+              (* ignore errors, we will get a "Cannot infer ..." error instead *)
+              sigma
+          end)
         sigma args
     | _ -> Termops.fold_constr_with_full_binders
              sigma
              (fun d (env,k) -> EConstr.push_rel d env, k+1)
              aux envk sigma c
   in
-  aux (env_ar_par,0) sigma c
+  aux (env_ar_par,k) sigma c
 
 let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) notations ~cumulative ~poly ~private_ind finite =
   check_all_names_different indl;
@@ -527,7 +531,7 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let sigma =
     List.fold_left (fun sigma (_,ctyps,_) ->
         List.fold_left (fun sigma ctyp ->
-            maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ctyp)
+            maybe_unify_params_in env_ar_params sigma ~ninds ~nparams ~binders:0 ctyp)
           sigma ctyps)
       sigma constructors
   in
diff --git a/vernac/comInductive.mli b/vernac/comInductive.mli
index 9c876787a3..91e8f609d5 100644
--- a/vernac/comInductive.mli
+++ b/vernac/comInductive.mli
@@ -81,8 +81,8 @@ val template_polymorphism_candidate
    monomorphic universe context that can be made parametric in its
    conclusion sort, if one is given. *)
 
-val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int
+val maybe_unify_params_in : Environ.env -> Evd.evar_map -> ninds:int -> nparams:int -> binders:int
   -> EConstr.t -> Evd.evar_map
 (** [nparams] is the number of parameters which aren't treated as
     uniform, ie the length of params (including letins) where the env
-    is [uniform params, inductives, params]. *)
+    is [uniform params, inductives, params, binders]. *)
diff --git a/vernac/record.ml b/vernac/record.ml
index d0036e40f9..bd5b71cd6b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -81,12 +81,12 @@ let interp_fields_evars env sigma ~ninds ~nparams impls_env nots l =
          (EConstr.push_rel d env, sigma, impl :: uimpls, d::params, impls))
       (env, sigma, [], [], impls_env) nots l
   in
-  let _, sigma = Context.Rel.fold_outside ~init:(env,sigma) (fun f (env,sigma) ->
+  let _, _, sigma = Context.Rel.fold_outside ~init:(env,0,sigma) (fun f (env,k,sigma) ->
       let sigma = RelDecl.fold_constr (fun c sigma ->
-          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams c)
+          ComInductive.maybe_unify_params_in env sigma ~ninds ~nparams ~binders:k c)
           f sigma
       in
-      EConstr.push_rel f env, sigma)
+      EConstr.push_rel f env, k+1, sigma)
       newfs
   in
   sigma, (impls, newfs)