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

3 files changed, 19 insertions, 21 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 00d4c7b3d8..cdf2922516 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -244,24 +244,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
         Prod (_,a,b) -> (* assert (l2=[]); *)
           let _, a, b = destProd sigma t2 in
           if noccurn sigma 1 b then
-            lookup_canonical_conversion (proji, Prod_cs),
+            lookup_canonical_conversion env (proji, Prod_cs),
             (Stack.append_app [|a;pop b|] Stack.empty)
           else raise Not_found
       | Sort s ->
         let s = ESorts.kind sigma s in
-        lookup_canonical_conversion
+        lookup_canonical_conversion env
           (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 env (proji, Proj_cs (Projection.repr p)), 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
+          lookup_canonical_conversion env (proji, Const_cs c2),sk2
     with Not_found ->
-      let (c, cs) = lookup_canonical_conversion (proji,Default_cs) in
+      let (c, cs) = lookup_canonical_conversion env (proji,Default_cs) in
         (c,cs),[]
   in
   let t', { o_DEF = c; o_CTX = ctx; o_INJ=n; o_TABS = bs;
@@ -273,6 +269,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..b6e44265ae 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -144,19 +144,21 @@ type obj_typ = {
 
 type cs_pattern =
     Const_cs of GlobRef.t
+  | Proj_cs of Projection.Repr.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
 
-let eq_cs_pattern p1 p2 = match p1, p2 with
-| Const_cs gr1, Const_cs gr2 -> GlobRef.equal gr1 gr2
+let eq_cs_pattern env p1 p2 = match p1, p2 with
+| Const_cs gr1, Const_cs gr2 -> Environ.QGlobRef.equal env gr1 gr2
+| Proj_cs p1, Proj_cs p2 -> Environ.QProjection.Repr.equal env p1 p2
 | Prod_cs, Prod_cs -> true
 | Sort_cs s1, Sort_cs s2 -> Sorts.family_equal s1 s2
 | Default_cs, Default_cs -> true
 | _ -> false
 
-let rec assoc_pat a = function
-  | ((pat, t), e) :: xs -> if eq_cs_pattern pat a then (t, e) else assoc_pat a xs
+let rec assoc_pat env a = function
+  | ((pat, t), e) :: xs -> if eq_cs_pattern env pat a then (t, e) else assoc_pat env a xs
   | [] -> raise Not_found
 
 
@@ -179,10 +181,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) -> Proj_cs (Projection.repr p), None, [c]
   | Sort s -> Sort_cs (Sorts.family s), None, []
   | _ -> Const_cs (fst @@ destRef t) , None, []
 
@@ -238,6 +237,7 @@ let compute_canonical_projections env ~warn (gref,ind) =
 
 let pr_cs_pattern = function
     Const_cs c -> Nametab.pr_global_env Id.Set.empty c
+  | Proj_cs p -> Nametab.pr_global_env Id.Set.empty (GlobRef.ConstRef (Projection.Repr.constant p))
   | Prod_cs -> str "_ -> _"
   | Default_cs -> str "_"
   | Sort_cs s -> Sorts.pr_sort_family s
@@ -253,7 +253,7 @@ let register_canonical_structure ~warn env sigma o =
     compute_canonical_projections env ~warn o |>
     List.iter (fun ((proj, (cs_pat, _ as pat)), s) ->
       let l = try GlobRef.Map.find proj !object_table with Not_found -> [] in
-      match assoc_pat cs_pat l with
+      match assoc_pat env cs_pat l with
       | exception Not_found ->
           object_table := GlobRef.Map.add proj ((pat, s) :: l) !object_table
       | _, cs ->
@@ -320,8 +320,8 @@ let check_and_decompose_canonical_structure env sigma ref =
     error_not_structure ref (str "Got too few arguments to the record or structure constructor.");
   (ref,indsp)
 
-let lookup_canonical_conversion (proj,pat) =
-  assoc_pat pat (GlobRef.Map.find proj !object_table)
+let lookup_canonical_conversion env (proj,pat) =
+  assoc_pat env pat (GlobRef.Map.find proj !object_table)
 
 let decompose_projection sigma c args =
   match EConstr.kind sigma c with
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 3be60d5e62..5b8dc8184a 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -67,6 +67,7 @@ val find_primitive_projection : Constant.t -> Projection.Repr.t option
 (** A cs_pattern characterizes the form of a component of canonical structure *)
 type cs_pattern =
     Const_cs of GlobRef.t
+  | Proj_cs of Projection.Repr.t
   | Prod_cs
   | Sort_cs of Sorts.family
   | Default_cs
@@ -88,7 +89,7 @@ val pr_cs_pattern : cs_pattern -> Pp.t
 
 type cs = GlobRef.t * inductive
 
-val lookup_canonical_conversion : (GlobRef.t * cs_pattern) -> constr * obj_typ
+val lookup_canonical_conversion : Environ.env -> (GlobRef.t * cs_pattern) -> constr * obj_typ
 val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
   cs -> unit
 val subst_canonical_structure : Mod_subst.substitution -> cs -> cs