From 1e92ed4d129aea5ea4e9300a24e1135cc186c341 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Thu, 2 Jul 2020 15:30:07 +0200
Subject: Fix Canonical with universe polymorphism and primitive projection

Perhaps we should thread an evar map with the Var universes added
through to cs_pattern_of_constr but that would be significantly more invasive.

Fix #12528
---
 pretyping/recordops.ml             | 2 +-
 pretyping/retyping.ml              | 3 +++
 pretyping/retyping.mli             | 4 ++++
 test-suite/bugs/closed/bug_12528.v | 6 ++++++
 4 files changed, 14 insertions(+), 1 deletion(-)
 create mode 100644 test-suite/bugs/closed/bug_12528.v

diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index a8e934d3c6..c26da8ccc7 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -185,7 +185,7 @@ let rec cs_pattern_of_constr env t =
   | 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 { Environ.uj_type = ty } = Typeops.infer env c in
+    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]
   | Sort s -> Sort_cs (Sorts.family s), None, []
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index bb518bc2f9..7a1af7f41a 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -257,6 +257,9 @@ let get_type_of ?(polyprop=true) ?(lax=false) env sigma c =
 (* Makes an unsafe judgment from a constr *)
 let get_judgment_of env evc c = { uj_val = c; uj_type = get_type_of env evc c }
 
+let get_type_of_constr ?polyprop ?lax env ?(uctx=UState.from_env env) c =
+  EConstr.Unsafe.to_constr (get_type_of ?polyprop ?lax env (Evd.from_ctx uctx) (EConstr.of_constr c))
+
 (* Returns sorts of a context *)
 let sorts_of_context env evc ctxt =
   let rec aux = function
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 16bc251c2a..2e19ffdfcd 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -30,6 +30,10 @@ exception RetypeError of retype_error
 val get_type_of :
   ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> types
 
+(** No-evar version of [get_type_of] *)
+val get_type_of_constr : ?polyprop:bool -> ?lax:bool
+  -> env -> ?uctx:UState.t -> Constr.t -> Constr.types
+
 val get_sort_of :
   ?polyprop:bool -> env -> evar_map -> types -> Sorts.t
 
diff --git a/test-suite/bugs/closed/bug_12528.v b/test-suite/bugs/closed/bug_12528.v
new file mode 100644
index 0000000000..4ab05ac9b8
--- /dev/null
+++ b/test-suite/bugs/closed/bug_12528.v
@@ -0,0 +1,6 @@
+Set Primitive Projections.
+Set Universe Polymorphism.
+Record ptd := Ptd { t : Type ; p : t }.
+Definition type := Ptd Type (unit:Type).
+Definition type' := Ptd Type (p type).
+Canonical type'.
-- 
cgit v1.2.3