aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/coercion.ml13
-rw-r--r--pretyping/evarconv.ml123
-rw-r--r--pretyping/evarconv.mli8
-rw-r--r--pretyping/evarutil.ml53
-rw-r--r--pretyping/evarutil.mli13
-rw-r--r--pretyping/pretype_errors.ml46
-rw-r--r--pretyping/pretype_errors.mli28
-rw-r--r--pretyping/pretyping.ml3
-rw-r--r--pretyping/unification.ml8
9 files changed, 185 insertions, 110 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5503a147a6..bedd3eb749 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -79,6 +79,7 @@ end
module Default = struct
(* Typing operations dealing with coercions *)
exception NoCoercion
+ exception NoCoercionNoUnifier of evar_map * unification_error
(* Here, funj is a coercion therefore already typed in global context *)
let apply_coercion_args env argl funj =
@@ -186,11 +187,11 @@ module Default = struct
with Not_found -> raise NoCoercion
in
try (the_conv_x_leq env t' c1 evd, v')
- with Reduction.NotConvertible -> raise NoCoercion
+ with NotUnifiable _ -> raise NoCoercion
let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
try (the_conv_x_leq env t c1 evd, v)
- with Reduction.NotConvertible ->
+ with NotUnifiable (best_failed_evd,e) ->
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
@@ -218,7 +219,7 @@ module Default = struct
| Some v2 -> Retyping.get_type_of env1 evd' v2 in
let (evd'',v2') = inh_conv_coerce_to_fail loc env1 evd' rigidonly v2 t2 u2 in
(evd'', Option.map (fun v2' -> mkLambda (name, u1, v2')) v2')
- | _ -> raise NoCoercion
+ | _ -> raise (NoCoercionNoUnifier (best_failed_evd,e))
(* Look for cj' obtained from cj by inserting coercions, s.t. cj'.typ = t *)
let inh_conv_coerce_to_gen rigidonly loc env evd cj (n, t) =
@@ -227,12 +228,12 @@ module Default = struct
let (evd', val') =
try
inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
+ with NoCoercionNoUnifier (best_failed_evd,e) ->
let evd = saturate_evd env evd in
try
inh_conv_coerce_to_fail loc env evd rigidonly (Some cj.uj_val) cj.uj_type t
- with NoCoercion ->
- error_actual_type_loc loc env evd cj t
+ with NoCoercionNoUnifier _ ->
+ error_actual_type_loc loc env best_failed_evd cj t e
in
let val' = match val' with Some v -> v | None -> assert(false) in
(evd',{ uj_val = val'; uj_type = t })
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 8b7fde3c29..cd505b1b77 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -19,6 +19,7 @@ open Recordops
open Evarutil
open Libnames
open Evd
+open Pretype_errors
type flex_kind_of_term =
| Rigid of constr
@@ -128,39 +129,42 @@ let rec ise_try evd = function
[] -> assert false
| [f] -> f evd
| f1::l ->
- let (evd',b) = f1 evd in
- if b then (evd',b) else ise_try evd l
+ match f1 evd with
+ | Success _ as x -> x
+ | UnifFailure _ -> ise_try evd l
let ise_and evd l =
let rec ise_and i = function
[] -> assert false
| [f] -> f i
| f1::l ->
- let (i',b) = f1 i in
- if b then ise_and i' l else (evd,false) in
+ match f1 i with
+ | Success i' -> ise_and i' l
+ | UnifFailure _ as x -> x in
ise_and evd l
let ise_list2 evd f l1 l2 =
let rec ise_list2 i l1 l2 =
match l1,l2 with
- [], [] -> (i, true)
+ [], [] -> Success i
| [x], [y] -> f i x y
| x::l1, y::l2 ->
- let (i',b) = f i x y in
- if b then ise_list2 i' l1 l2 else (evd,false)
- | _ -> (evd, false) in
+ (match f i x y with
+ | Success i' -> ise_list2 i' l1 l2
+ | UnifFailure _ as x -> x)
+ | _ -> UnifFailure (evd, NotSameArgSize) in
ise_list2 evd l1 l2
let ise_array2 evd f v1 v2 =
let rec allrec i = function
- | -1 -> (i,true)
+ | -1 -> Success i
| n ->
- let (i',b) = f i v1.(n) v2.(n) in
- if b then allrec i' (n-1) else (evd,false)
- in
+ match f i v1.(n) v2.(n) with
+ | Success i' -> allrec i' (n-1)
+ | UnifFailure _ as x -> x in
let lv1 = Array.length v1 in
if lv1 = Array.length v2 then allrec evd (pred lv1)
- else (evd,false)
+ else UnifFailure (evd,NotSameArgSize)
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
@@ -176,7 +180,8 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
else None
else None in
match ground_test with
- Some b -> (evd,b)
+ | Some true -> Success evd
+ | Some false -> UnifFailure (evd,ConversionFailed (env,term1,term2))
| None ->
(* Until pattern-unification is used consistently, use nohdbeta to not
destroy beta-redexes that can be used for 1st-order unification *)
@@ -217,9 +222,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
ise_and i
[(fun i -> ise_list2 i
(fun i -> evar_conv_x ts env i CONV) l1 l2);
- (fun i -> solve_refl (evar_conv_x ts) env i sp1 al1 al2,
- true)]
- else (i,false)
+ (fun i ->
+ Success (solve_refl
+ (fun env i pbty a1 a2 ->
+ is_success (evar_conv_x ts env i pbty a1 a2))
+ env i sp1 al1 al2))]
+ else UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2]
@@ -247,12 +255,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
[(fun i -> ise_list2 i
(fun i -> evar_conv_x ts env i CONV) l1 rest2);
(fun i -> evar_conv_x ts env i pbty term1 (applist(term2,deb2)))]
- else (i,false)
+ else UnifFailure (i,NotSameArgSize)
and f2 i =
match eval_flexible_term env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2]
@@ -279,12 +287,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
[(fun i -> ise_list2 i
(fun i -> evar_conv_x ts env i CONV) rest1 l2);
(fun i -> evar_conv_x ts env i pbty (applist(term1,deb1)) term2)]
- else (i,false)
+ else UnifFailure (i,NotSameArgSize)
and f2 i =
match eval_flexible_term env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2]
@@ -311,12 +319,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
if flex1 = flex2 then
ise_list2 i (fun i -> evar_conv_x ts env i CONV) l1 l2
else
- (i,false)
+ UnifFailure (i,NotSameHead)
and f2 i =
(try conv_record ts env i
(try check_conv_record appr1 appr2
with Not_found -> check_conv_record appr2 appr1)
- with Not_found -> (i,false))
+ with Not_found -> UnifFailure (i,NoCanonicalStructure))
and f3 i =
(* heuristic: unfold second argument first, exception made
if the first argument is a beta-redex (expand a constant
@@ -331,7 +339,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
match eval_flexible_term env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
else
match eval_flexible_term env flex2 with
| Some v2 ->
@@ -340,7 +348,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
match eval_flexible_term env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2; f3]
end
@@ -391,8 +399,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(decompose_app (beta_applist (c1,l1))) appr2
else
(* Postpone the use of an heuristic *)
- add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
- true
+ Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd)
| (Rigid _ | PseudoRigid _ as c1), Flexible ev2 ->
if
@@ -411,30 +418,29 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
(decompose_app (beta_applist (c2,l2)))
else
(* Postpone the use of an heuristic *)
- add_conv_pb (pbty,env,applist appr1,applist appr2) evd,
- true
+ Success (add_conv_pb (pbty,env,applist appr1,applist appr2) evd)
| MaybeFlexible flex1, (Rigid _ | PseudoRigid _) ->
let f3 i =
(try conv_record ts env i (check_conv_record appr1 appr2)
- with Not_found -> (i,false))
+ with Not_found -> UnifFailure (i,NoCanonicalStructure))
and f4 i =
match eval_flexible_term env flex1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (evar_apprec env i l1 v1) appr2
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f3; f4]
| (Rigid _ | PseudoRigid _), MaybeFlexible flex2 ->
let f3 i =
(try conv_record ts env i (check_conv_record appr2 appr1)
- with Not_found -> (i,false))
+ with Not_found -> UnifFailure (i,NoCanonicalStructure))
and f4 i =
match eval_flexible_term env flex2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (evar_apprec env i l2 v2)
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f3; f4]
@@ -442,7 +448,8 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
match kind_of_term c1, kind_of_term c2 with
| Sort s1, Sort s2 when l1=[] & l2=[] ->
- (evd, base_sort_cmp pbty s1 s2)
+ if base_sort_cmp pbty s1 s2 then Success evd
+ else UnifFailure (evd,NotSameHead)
| Prod (n,c1,c'1), Prod (_,c2,c'2) when l1=[] & l2=[] ->
ise_and evd
@@ -454,12 +461,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
| Ind sp1, Ind sp2 ->
if eq_ind sp1 sp2 then
ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
- else (evd, false)
+ else UnifFailure (evd,NotSameHead)
| Construct sp1, Construct sp2 ->
if eq_constructor sp1 sp2 then
ise_list2 evd (fun i -> evar_conv_x ts env i CONV) l1 l2
- else (evd, false)
+ else UnifFailure (evd,NotSameHead)
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
if i1=i2 then
@@ -471,10 +478,12 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
bds1 bds2);
(fun i -> ise_list2 i
(fun i -> evar_conv_x ts env i CONV) l1 l2)]
- else (evd,false)
+ else UnifFailure (evd,NotSameHead)
- | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ -> (evd,false)
- | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) -> (evd,false)
+ | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _), _ ->
+ UnifFailure (evd,NotSameHead)
+ | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _) ->
+ UnifFailure (evd,NotSameHead)
| (App _ | Meta _ | Cast _ | Case _ | Fix _), _ -> assert false
| (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
@@ -503,10 +512,10 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
bds1 bds2);
(fun i -> ise_list2 i
(fun i -> evar_conv_x ts env i CONV) l1 l2)]
- else (evd,false)
+ else UnifFailure (evd,NotSameHead)
| (Meta _ | Case _ | Fix _ | CoFix _),
- (Meta _ | Case _ | Fix _ | CoFix _) -> (evd,false)
+ (Meta _ | Case _ | Fix _ | CoFix _) -> UnifFailure (evd,NotSameHead)
| (App _ | Ind _ | Construct _ | Sort _ | Prod _), _ -> assert false
| _, (App _ | Ind _ | Construct _ | Sort _ | Prod _) -> assert false
@@ -519,9 +528,9 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
end
- | PseudoRigid _, Rigid _ -> (evd,false)
+ | PseudoRigid _, Rigid _ -> UnifFailure (evd,NotSameHead)
- | Rigid _, PseudoRigid _ -> (evd,false)
+ | Rigid _, PseudoRigid _ -> UnifFailure (evd,NotSameHead)
and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
let (evd',ks,_) =
@@ -577,12 +586,12 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
& array_for_all (fun a -> a = term2 or isEvar a) args1 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
- choose_less_dependent_instance evk1 evd term2 args1, true
+ Success (choose_less_dependent_instance evk1 evd term2 args1)
| (Rel _|Var _), Evar (evk2,args2) when l1 = [] & l2 = []
& array_for_all (fun a -> a = term1 or isEvar a) args2 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
- choose_less_dependent_instance evk2 evd term1 args2, true
+ Success (choose_less_dependent_instance evk2 evd term1 args2)
| Evar ev1,_ when List.length l1 <= List.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
first_order_unification ts env evd (ev1,l1) appr2
@@ -597,8 +606,10 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
let (evd,pbs) = extract_all_conv_pbs evd in
let heuristic_solved_evd = List.fold_left
(fun evd (pbty,env,t1,t2) ->
- let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
- if b then evd' else Pretype_errors.error_cannot_unify env evd (t1, t2))
+ match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
+ | Success evd' -> evd'
+ | UnifFailure (evd,reason) ->
+ Pretype_errors.error_cannot_unify env evd ~reason (t1, t2))
evd pbs in
Evd.fold_undefined (fun ev ev_info evd' -> match ev_info.evar_source with
|_,ImpossibleCase ->
@@ -607,22 +618,24 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
(* Main entry points *)
+exception NotUnifiable of evar_map * unification_error
+
let the_conv_x ?(ts=full_transparent_state) env t1 t2 evd =
match evar_conv_x ts env evd CONV t1 t2 with
- (evd',true) -> evd'
- | _ -> raise Reduction.NotConvertible
+ | Success evd' -> evd'
+ | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e))
let the_conv_x_leq ?(ts=full_transparent_state) env t1 t2 evd =
match evar_conv_x ts env evd CUMUL t1 t2 with
- (evd', true) -> evd'
- | _ -> raise Reduction.NotConvertible
+ | Success evd' -> evd'
+ | UnifFailure (evd',e) -> raise (NotUnifiable (evd',e))
let e_conv ?(ts=full_transparent_state) env evd t1 t2 =
match evar_conv_x ts env !evd CONV t1 t2 with
- (evd',true) -> evd := evd'; true
- | _ -> false
+ | Success evd' -> evd := evd'; true
+ | _ -> false
let e_cumul ?(ts=full_transparent_state) env evd t1 t2 =
match evar_conv_x ts env !evd CUMUL t1 t2 with
- (evd',true) -> evd := evd'; true
- | _ -> false
+ | Success evd' -> evd := evd'; true
+ | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index e1f507b0ac..d2d74ff962 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -13,7 +13,9 @@ open Environ
open Reductionops
open Evd
-(** returns exception Reduction.NotConvertible if not unifiable *)
+exception NotUnifiable of evar_map * Pretype_errors.unification_error
+
+(** returns exception NotUnifiable with best known evar_map if not unifiable *)
val the_conv_x : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
val the_conv_x_leq : ?ts:transparent_state -> env -> constr -> constr -> evar_map -> evar_map
@@ -25,11 +27,11 @@ val e_cumul : ?ts:transparent_state -> env -> evar_map ref -> constr -> constr -
(**/**)
(* For debugging *)
val evar_conv_x : transparent_state ->
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
+ env -> evar_map -> conv_pb -> constr -> constr -> Evarutil.unification_result
val evar_eqappr_x : transparent_state ->
env -> evar_map ->
conv_pb -> constr * constr list -> constr * constr list ->
- evar_map * bool
+ Evarutil.unification_result
(**/**)
val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 774180c67b..13d193658f 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -584,6 +584,9 @@ let clear_hyps_in_evi evdref hyps concl ids =
in
(nhyps,nconcl)
+(***************)
+(* Unification *)
+
(* Inverting constructors in instances (common when inferring type of match) *)
let find_projectable_constructor env evd cstr k args cstr_subst =
@@ -945,7 +948,7 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
(* Filter and restrict if needed *)
let evd,evk,args =
restrict_upon_filter evd evi evk
- (fun (a1,a2) -> snd (conv_algo env evd Reduction.CONV a1 a2))
+ (fun (a1,a2) -> conv_algo env evd Reduction.CONV a1 a2)
(List.combine (Array.to_list argsv1) (Array.to_list argsv2)) in
(* Leave a unification problem *)
let args1,args2 = List.split args in
@@ -976,9 +979,17 @@ let solve_refl conv_algo env evd evk argsv1 argsv2 =
* Σ; Γ, y1..yk |- φ(u1..un) = c /\ x1..xn |- φ(x1..xn)
*)
+type unification_result =
+ | Success of evar_map
+ | UnifFailure of evar_map * unification_error
+
+let is_success = function Success _ -> true | UnifFailure _ -> false
+
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress
exception OccurCheckIn of evar_map * constr
+exception MetaOccurInBodyInternal
+exception InstanceNotSameTypeInternal
let rec invert_definition choose env evd (evk,argsv as ev) rhs =
let aliases = make_alias_map env in
@@ -1093,7 +1104,7 @@ and occur_existential evm c =
and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd =
try
let (evd',body) = invert_definition choose env evd ev rhs in
- if occur_meta body then error "Meta cannot occur in evar body.";
+ if occur_meta body then raise MetaOccurInBodyInternal;
(* invert_definition may have instantiate some evars of rhs with evk *)
(* so we recheck acyclicity *)
if occur_evar evk body then raise (OccurCheckIn (evd',body));
@@ -1119,18 +1130,17 @@ and evar_define ?(choose=false) env (evk,argsv as ev) rhs evd =
with
| NotEnoughInformationToProgress ->
postpone_evar_term env evd ev rhs
- | NotInvertibleUsingOurAlgorithm t ->
- error_not_clean env evd evk t (evar_source evk evd)
+ | NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
+ raise e
| OccurCheckIn (evd,rhs) ->
(* last chance: rhs actually reduces to ev *)
let c = whd_betadeltaiota env evd rhs in
match kind_of_term c with
| Evar (evk',argsv2) when evk = evk' ->
- solve_refl
- (fun env sigma pb c c' -> (evd,is_fconv pb env sigma c c'))
+ solve_refl (fun env sigma pb c c' -> is_fconv pb env sigma c c')
env evd evk argsv argsv2
| _ ->
- error_occur_check env evd evk rhs
+ raise (OccurCheckIn (evd,rhs))
(*-------------------*)
(* Auxiliary functions for the conversion algorithms modulo evars
@@ -1307,10 +1317,10 @@ let check_instance_type conv_algo env evd ev1 t2 =
if isEvar typ2 then (* Don't want to commit too early too *) evd
else
let typ1 = existential_type evd ev1 in
- let evd,b = conv_algo env evd Reduction.CUMUL typ2 typ1 in
- if b then evd else
- user_err_loc (fst (evar_source (fst ev1) evd),"",
- str "Unable to find a well-typed instantiation")
+ match conv_algo env evd Reduction.CUMUL typ2 typ1 with
+ | Success evd -> evd
+ | UnifFailure _ ->
+ raise InstanceNotSameTypeInternal
(* Tries to solve problem t1 = t2.
* Precondition: t1 is an uninstantiated evar
@@ -1324,7 +1334,9 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
let evd = match kind_of_term t2 with
| Evar (evk2,args2 as ev2) ->
if evk1 = evk2 then
- solve_refl conv_algo env evd evk1 args1 args2
+ solve_refl
+ (fun env evd pbty a b -> is_success (conv_algo env evd pbty a b))
+ env evd evk1 args1 args2
else
if pbty = None
then solve_evar_evar evar_define env evd ev1 ev2
@@ -1353,11 +1365,20 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
in
let (evd,pbs) = extract_changed_conv_pbs evd status_changed in
List.fold_left
- (fun (evd,b as p) (pbty,env,t1,t2) ->
- if b then conv_algo env evd pbty t1 t2 else p) (evd,true)
+ (fun p (pbty,env,t1,t2) ->
+ match p with
+ | Success evd -> conv_algo env evd pbty t1 t2
+ | UnifFailure _ as x -> x) (Success evd)
pbs
- with e when precatchable_exception e ->
- (evd,false)
+ with
+ | NotInvertibleUsingOurAlgorithm t ->
+ UnifFailure (evd,NotClean (evk1,t))
+ | OccurCheckIn (evd,rhs) ->
+ UnifFailure (evd,OccurCheck (evk1,rhs))
+ | MetaOccurInBodyInternal ->
+ UnifFailure (evd,MetaOccurInBody evk1)
+ | InstanceNotSameTypeInternal ->
+ UnifFailure (evd,InstanceNotSameType evk1)
(** The following functions return the set of evars immediately
contained in the object, including defined evars *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index a4c07a0196..705ab356fb 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -74,13 +74,20 @@ val whd_head_evar : evar_map -> constr -> constr
val is_ground_term : evar_map -> constr -> bool
val is_ground_env : evar_map -> env -> bool
val solve_refl :
- (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
+ (env -> evar_map -> conv_pb -> constr -> constr -> bool)
-> env -> evar_map -> existential_key -> constr array -> constr array ->
evar_map
+
+type unification_result =
+ | Success of evar_map
+ | UnifFailure of evar_map * Pretype_errors.unification_error
+
+val is_success : unification_result -> bool
+
val solve_simple_eqn :
- (env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool)
+ (env -> evar_map -> conv_pb -> constr -> constr -> unification_result)
-> ?choose:bool -> env -> evar_map -> bool option * existential * constr ->
- evar_map * bool
+ unification_result
(** [check_evars env initial_sigma extended_sigma c] fails if some
new unresolved evar remains in [c] *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6d1c54e63d..f663496dfb 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,15 +18,26 @@ open Type_errors
open Glob_term
open Inductiveops
+type unification_error =
+ | OccurCheck of existential_key * constr
+ | NotClean of existential_key * constr
+ | NotSameArgSize
+ | NotSameHead
+ | NoCanonicalStructure
+ | ConversionFailed of env * constr * constr
+ | MetaOccurInBody of existential_key
+ | InstanceNotSameType of existential_key
+
type pretype_error =
(* Old Case *)
| CantFindCaseType of constr
- (* Unification *)
- | OccurCheck of existential_key * constr
- | NotClean of existential_key * constr * Evd.hole_kind
+ (* Type inference unification *)
+ | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ (* Tactic unification *)
+ | UnifOccurCheck of existential_key * constr
| UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
Evd.unsolvability_explanation option
- | CannotUnify of constr * constr
+ | CannotUnify of constr * constr * unification_error option
| CannotUnifyLocal of constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
@@ -95,6 +106,15 @@ let contract2 env a b = match contract env [a;b] with
let contract3 env a b c = match contract env [a;b;c] with
| env, [a;b;c] -> env,a,b,c | _ -> assert false
+let contract4 env a b c d = match contract env [a;b;c;d] with
+ | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
+
+let contract3' env a b c = function
+ | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
+ | NotClean (evk,d) -> let x,d = contract4 env a b c d in x,NotClean(evk,d)
+ | NotSameArgSize | NotSameHead | NoCanonicalStructure | ConversionFailed _
+ | MetaOccurInBody _ | InstanceNotSameType _ as x -> contract3 env a b c, x
+
let raise_pretype_error (loc,env,sigma,te) =
Loc.raise loc (PretypeError(env,sigma,te))
@@ -102,10 +122,11 @@ let raise_located_type_error (loc,env,sigma,te) =
Loc.raise loc (PretypeError(env,sigma,TypingError te))
-let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
- let env, c, actty, expty = contract3 env c actty expty in
+let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason =
+ let (env, c, actty, expty), reason = contract3' env c actty expty reason in
let j = {uj_val=c;uj_type=actty} in
- raise_located_type_error (loc, env, sigma, ActualType (j, expty))
+ raise_pretype_error
+ (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason))
let error_cant_apply_not_functional_loc loc env sigma rator randl =
raise_located_type_error
@@ -137,23 +158,20 @@ let error_not_a_type_loc loc env sigma j =
a precise location. *)
let error_occur_check env sigma ev c =
- raise (PretypeError (env, sigma, OccurCheck (ev,c)))
-
-let error_not_clean env sigma ev c (loc,k) =
- Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
+ raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
let error_unsolvable_implicit loc env sigma evi e explain =
Loc.raise loc
(PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
-let error_cannot_unify env sigma (m,n) =
- raise (PretypeError (env, sigma,CannotUnify (m,n)))
+let error_cannot_unify env sigma ?reason (m,n) =
+ raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
let error_cannot_unify_local env sigma (m,n,sn) =
raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
let error_cannot_coerce env sigma (m,n) =
- raise (PretypeError (env, sigma,CannotUnify (m,n)))
+ raise (PretypeError (env, sigma,CannotUnify (m,n,None)))
let error_cannot_find_well_typed_abstraction env sigma p l =
raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index 30ee6aaf67..f95514ade4 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -17,15 +17,26 @@ open Inductiveops
(** {6 The type of errors raised by the pretyper } *)
+type unification_error =
+ | OccurCheck of existential_key * constr
+ | NotClean of existential_key * constr
+ | NotSameArgSize
+ | NotSameHead
+ | NoCanonicalStructure
+ | ConversionFailed of env * constr * constr
+ | MetaOccurInBody of existential_key
+ | InstanceNotSameType of existential_key
+
type pretype_error =
(** Old Case *)
| CantFindCaseType of constr
- (** Unification *)
- | OccurCheck of existential_key * constr
- | NotClean of existential_key * constr * Evd.hole_kind
+ (** Type inference unification *)
+ | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ (** Tactic Unification *)
+ | UnifOccurCheck of existential_key * constr
| UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
Evd.unsolvability_explanation option
- | CannotUnify of constr * constr
+ | CannotUnify of constr * constr * unification_error option
| CannotUnifyLocal of constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
@@ -59,7 +70,8 @@ val jv_nf_betaiotaevar :
(** Raising errors *)
val error_actual_type_loc :
- loc -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+ loc -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+ unification_error -> 'b
val error_cant_apply_not_functional_loc :
loc -> env -> Evd.evar_map ->
@@ -93,14 +105,12 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b
val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b
-val error_not_clean :
- env -> Evd.evar_map -> existential_key -> constr -> loc * Evd.hole_kind -> 'b
-
val error_unsolvable_implicit :
loc -> env -> Evd.evar_map -> Evd.evar_info -> Evd.hole_kind ->
Evd.unsolvability_explanation option -> 'b
-val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
+val error_cannot_unify : env -> Evd.evar_map -> ?reason:unification_error ->
+ constr * constr -> 'b
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 1ea2dbd002..003f507dcf 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -640,7 +640,8 @@ module Pretyping_F (Coercion : Coercion.S) = struct
try
ignore (Reduction.vm_conv Reduction.CUMUL env cty tval); cj
with Reduction.NotConvertible ->
- error_actual_type_loc loc env !evdref cj tval
+ error_actual_type_loc loc env !evdref cj tval
+ (ConversionFailed (env,cty,tval))
end
| _ -> inh_conv_coerce_to_tycon loc env evdref cj (mk_tycon tval)
in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6121ba7d87..6e39d9831c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -638,9 +638,11 @@ let order_metas metas =
(* Solve an equation ?n[x1=u1..xn=un] = t where ?n is an evar *)
let solve_simple_evar_eqn ts env evd ev rhs =
- let evd,b = solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) in
- if not b then error_cannot_unify env evd (mkEvar ev,rhs);
- Evarconv.consider_remaining_unif_problems env evd
+ match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
+ | UnifFailure (evd,reason) ->
+ error_cannot_unify env evd ~reason (mkEvar ev,rhs);
+ | Success evd ->
+ Evarconv.consider_remaining_unif_problems env evd
(* [w_merge env sigma b metas evars] merges common instances in metas
or in evars, possibly generating new unification problems; if [b]
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 17:14:55 +0000