Extend hack to use postponed constraints in retyping to template poly

See 742ef62fe8050a6865d06bd644e30cbec0e7eb02

Fix #13366
Fix #9809

1 files changed, 9 insertions, 3 deletions

diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 4bd22e76cb..34bcd0982c 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -67,6 +67,14 @@ let get_type_from_constraints env sigma t =
     | _ -> raise Not_found
   else raise Not_found
 
+let sort_of_arity_with_constraints env sigma t =
+  try Reductionops.sort_of_arity env sigma t
+  with Reduction.NotArity ->
+  try
+    let t = get_type_from_constraints env sigma t in
+    Reductionops.sort_of_arity env sigma t
+  with Not_found | Reduction.NotArity -> retype_error NotAnArity
+
 let rec subst_type env sigma typ = function
   | [] -> typ
   | h::rest ->
@@ -187,9 +195,7 @@ let retype ?(polyprop=true) sigma =
       let mip = lookup_mind_specif env ind in
       let paramtyps = Array.map_to_list (fun arg () ->
           let t = type_of env arg in
-          let s = try Reductionops.sort_of_arity env sigma t
-            with Reduction.NotArity -> retype_error NotAnArity
-          in
+          let s = sort_of_arity_with_constraints env sigma t in
           Sorts.univ_of_sort (ESorts.kind sigma s))
           args
       in