Merge PR #13181: Guard unify_leq_delay calls in Typing

Reviewed-by: ppedrot

6 files changed, 27 insertions, 19 deletions

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 1e8441dd8a..1dddc5622d 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -48,7 +48,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
-  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option
   | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
   | NonLinearUnification of Name.t * constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 45997e9a66..714d68165e 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -54,7 +54,7 @@ type pretype_error =
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | NoOccurrenceFound of constr * Id.t option
-  | CannotFindWellTypedAbstraction of constr * constr list * (env * type_error) option
+  | CannotFindWellTypedAbstraction of constr * constr list * (env * pretype_error) option
   | WrongAbstractionType of Name.t * constr * types * types
   | AbstractionOverMeta of Name.t * Name.t
   | NonLinearUnification of Name.t * constr
@@ -132,7 +132,7 @@ val error_cannot_unify : ?loc:Loc.t -> env -> Evd.evar_map ->
 val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
 
 val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
-      constr -> constr list -> (env * type_error) option -> 'b
+      constr -> constr list -> (env * pretype_error) option -> 'b
 
 val error_wrong_abstraction_type :  env -> Evd.evar_map ->
       Name.t -> constr -> types -> types -> 'b
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 756ccd3438..40d3faa98c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -220,14 +220,15 @@ let check_allowed_sort env sigma ind c p =
   else
     Sorts.relevance_of_sort_family ksort
 
+let check_actual_type env sigma cj t =
+  try Evarconv.unify_leq_delay env sigma cj.uj_type t
+  with Evarconv.UnableToUnify (sigma,e) -> error_actual_type env sigma cj t e
+
 let judge_of_cast env sigma cj k tj =
   let expected_type = tj.utj_val in
-  match Evarconv.unify_leq_delay env sigma cj.uj_type expected_type with
-  | exception Evarconv.UnableToUnify _ ->
-    error_actual_type_core env sigma cj expected_type;
-  | sigma ->
-    sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
-             uj_type = expected_type }
+  let sigma = check_actual_type env sigma cj expected_type in
+  sigma, { uj_val = mkCast (cj.uj_val, k, expected_type);
+           uj_type = expected_type }
 
 let check_fix env sigma pfix =
   let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
@@ -340,7 +341,7 @@ let judge_of_array env sigma u tj defj tyj =
   let sigma = Evd.set_leq_sort env sigma tyj.utj_type
       (Sorts.sort_of_univ (Univ.Universe.make ulev))
   in
-  let check_one sigma j = Evarconv.unify_leq_delay env sigma j.uj_type tyj.utj_val in
+  let check_one sigma j = check_actual_type env sigma j tyj.utj_val in
   let sigma = check_one sigma defj in
   let sigma = Array.fold_left check_one sigma tj in
   let arr = EConstr.of_constr @@ type_of_array env u in
@@ -391,7 +392,7 @@ let rec execute env sigma cstr =
             let t = mkApp (mkIndU (ci.ci_ind,univs), args) in
             let sigma, tj = execute env sigma t in
             let sigma, tj = type_judgment env sigma tj in
-            let sigma = Evarconv.unify_leq_delay env sigma cj.uj_type tj.utj_val in
+            let sigma = check_actual_type env sigma cj tj.utj_val in
             sigma
         in
         judge_of_case env sigma ci pj iv cj lfj
@@ -492,10 +493,7 @@ and execute_array env = Array.fold_left_map (execute env)
 
 let check env sigma c t =
   let sigma, j = execute env sigma c in
-  match Evarconv.unify_leq_delay env sigma j.uj_type t with
-  | exception Evarconv.UnableToUnify _ ->
-    error_actual_type_core env sigma j t
-  | sigma -> sigma
+  check_actual_type env sigma j t
 
 (* Type of a constr *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 207a03d80f..ccfb508964 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -134,8 +134,8 @@ let abstract_list_all env evd typ c l =
     | Type_errors.TypeError (env',x) ->
         (* FIXME: plug back the typing information *)
         error_cannot_find_well_typed_abstraction env evd p l None
-    | Pretype_errors.PretypeError (env',evd,TypingError x) ->
-        error_cannot_find_well_typed_abstraction env evd p l (Some (env',x)) in
+    | Pretype_errors.PretypeError (env',evd,e) ->
+        error_cannot_find_well_typed_abstraction env evd p l (Some (env',e)) in
   evd,(p,typp)
 
 let set_occurrences_of_last_arg n =
diff --git a/test-suite/bugs/closed/bug_13171.v b/test-suite/bugs/closed/bug_13171.v
new file mode 100644
index 0000000000..0564722729
--- /dev/null
+++ b/test-suite/bugs/closed/bug_13171.v
@@ -0,0 +1,10 @@
+Primitive array := #array_type.
+
+Goal False.
+Proof.
+  unshelve epose (_:nat). exact_no_check true.
+  Fail let c := open_constr:([| n | 0 |]) in
+       let c := eval cbv in c in
+       let c := type of c in
+       idtac c.
+Abort.
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index a9de01bfd0..5f7eb78a40 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -866,7 +866,7 @@ let explain_unsatisfiable_constraints env sigma constr comp =
     let info = Evar.Map.find ev undef in
     explain_typeclass_resolution env sigma info k ++ fnl () ++ cstr
 
-let explain_pretype_error env sigma err =
+let rec explain_pretype_error env sigma err =
   let env = Evardefine.env_nf_betaiotaevar sigma env in
   let env = make_all_name_different env sigma in
   match err with
@@ -893,7 +893,7 @@ let explain_pretype_error env sigma err =
   | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env sigma m n
   | CannotFindWellTypedAbstraction (p,l,e) ->
       explain_cannot_find_well_typed_abstraction env sigma p l
-        (Option.map (fun (env',e) -> explain_type_error env' sigma e) e)
+        (Option.map (fun (env',e) -> explain_pretype_error env' sigma e) e)
   | WrongAbstractionType (n,a,t,u) ->
       explain_wrong_abstraction_type env sigma n a t u
   | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n