Fix incorrect debruijn handling when Record calls maybe_unify_params_in

Fix #12887

2 files changed, 20 insertions, 0 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 _ }.