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.
---
 pretyping/evarconv.ml             |  6 ++----
 pretyping/recordops.ml            |  5 +----
 test-suite/bugs/closed/bug_9971.v | 27 +++++++++++++++++++++++++++
 3 files changed, 30 insertions(+), 8 deletions(-)
 create mode 100644 test-suite/bugs/closed/bug_9971.v

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 00d4c7b3d8..16be4812fe 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -253,10 +253,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
           (proji, Sort_cs (Sorts.family s)),[]
       | Proj (p, c) ->
         let c2 = GlobRef.ConstRef (Projection.constant p) in
-        let c = Retyping.expand_projection env sigma p c [] in
-        let _, args = destApp sigma c in
-        let sk2 = Stack.append_app args sk2 in
-        lookup_canonical_conversion (proji, Const_cs c2), sk2
+        lookup_canonical_conversion (proji, Const_cs c2), Stack.append_app [|c|] sk2
       | _ ->
         let (c2, _) = try destRef sigma t2 with DestKO -> raise Not_found in
           lookup_canonical_conversion (proji, Const_cs c2),sk2
@@ -273,6 +270,7 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
     | Some c -> (* A primitive projection applied to c *)
       let ty = Retyping.get_type_of ~lax:true env sigma c in
       let (i,u), ind_args =
+        (* Are we sure that ty is not an evar? *)
         try Inductiveops.find_mrectype env sigma ty
         with _ -> raise Not_found
       in Stack.append_app_list ind_args Stack.empty, c, sk1
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index e6e5ad8dd4..f26f59d6c5 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -179,10 +179,7 @@ let rec cs_pattern_of_constr env t =
     patt, n, args @ Array.to_list vargs
   | Rel n -> Default_cs, Some n, []
   | Prod (_,a,b) when Vars.noccurn 1 b -> Prod_cs, None, [a; Vars.lift (-1) b]
-  | Proj (p, c) ->
-    let ty = Retyping.get_type_of_constr env c in
-    let _, params = Inductive.find_rectype env ty in
-    Const_cs (GlobRef.ConstRef (Projection.constant p)), None, params @ [c]
+  | Proj (p, c) -> Const_cs (GlobRef.ConstRef (Projection.constant p)), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
   | _ -> Const_cs (fst @@ destRef t) , None, []
 
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