Merge PR #13386: Fixes #9971: a useless situation where the type of a primitive projection was wrongly supposed to be already inferred

Reviewed-by: gares

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/bugs/closed/bug_9971.v b/test-suite/bugs/closed/bug_9971.v
new file mode 100644
index 0000000000..ef526dcd7d
--- /dev/null
+++ b/test-suite/bugs/closed/bug_9971.v
@@ -0,0 +1,27 @@
+(* Test that it raises a normal error and not an anomaly *)
+Set Primitive Projections.
+Record prod A B := pair { fst : A ; snd : B }.
+Arguments fst {A B} _.
+Arguments snd {A B} _.
+Arguments pair {A B} _ _.
+Record piis := { dep_types : Type; indep_args : dep_types -> Type }.
+Import EqNotations.
+Goal forall (id : Set) (V : id) (piiio : id -> piis)
+            (Z : {ridc : id & prod (dep_types (piiio ridc)) True})
+            (P : dep_types (piiio V) -> Type) (W : {x : dep_types (piiio V) & P x}),
+    let ida := fun (x : id) (y : dep_types (piiio x)) => indep_args (piiio x) y in
+    prod True (ida V (projT1 W)) ->
+    Z = existT _ V (pair (projT1 W) I) ->
+    ida (projT1 Z) (fst (projT2 Z)).
+  intros.
+  refine  (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+               H in
+              let v := I in
+              _);
+    refine (snd X).
+  Undo.
+Fail refine (rew <- [fun k' => ida (projT1 k') (fst (projT2 k'))]
+              H in
+             let v := I in
+             snd X).
+Abort.