From a27fb3c67238cc41dc24308a233a02422e0f83f3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 15 Nov 2020 10:28:04 +0100
Subject: Fixes #9971: expand_projections failing on primitive projections of
 unknown type.

This was a case where expand_projections was calling find_mrectype
which was expecting the argument of the projection to be an inductive.

We could have ensured that this type is at least the appropriate
inductive applied to fresh evars, but this expand_projections was in
practice used for checking the applicability of canonical structures
and the unifiability of the parameters of the projections is anyway a
consequence of the unifiability of the principal argument of the
projections. So, the latter is enough.
---
 test-suite/bugs/closed/bug_9971.v | 27 +++++++++++++++++++++++++++
 1 file changed, 27 insertions(+)
 create mode 100644 test-suite/bugs/closed/bug_9971.v

(limited to 'test-suite')

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.
-- 
cgit v1.2.3