Merge PR #13181: Guard unify_leq_delay calls in Typing

Reviewed-by: ppedrot

4 files changed, 15 insertions, 17 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 =