diff options
| -rw-r--r-- | parsing/printer.ml | 1 | ||||
| -rw-r--r-- | parsing/printer.mli | 1 | ||||
| -rw-r--r-- | plugins/subtac/subtac_cases.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_coercion.ml | 19 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 13 | ||||
| -rw-r--r-- | pretyping/evarconv.ml | 123 | ||||
| -rw-r--r-- | pretyping/evarconv.mli | 8 | ||||
| -rw-r--r-- | pretyping/evarutil.ml | 53 | ||||
| -rw-r--r-- | pretyping/evarutil.mli | 13 | ||||
| -rw-r--r-- | pretyping/pretype_errors.ml | 46 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 28 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/unification.ml | 8 | ||||
| -rw-r--r-- | proofs/clenv.ml | 3 | ||||
| -rw-r--r-- | proofs/evar_refiner.ml | 20 | ||||
| -rw-r--r-- | proofs/logic.ml | 5 | ||||
| -rw-r--r-- | proofs/proofview.ml | 3 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 53 |
18 files changed, 258 insertions, 144 deletions
diff --git a/parsing/printer.ml b/parsing/printer.ml index f1f5d4c9f..27dcffcea 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -120,6 +120,7 @@ let pr_global_env = pr_global_env let pr_global = pr_global_env Idset.empty let pr_constant env cst = pr_global_env (Termops.vars_of_env env) (ConstRef cst) +let pr_existential_key evk = str (string_of_existential evk) let pr_existential env ev = pr_lconstr_env env (mkEvar ev) let pr_inductive env ind = pr_lconstr_env env (mkInd ind) let pr_constructor env cstr = pr_lconstr_env env (mkConstruct cstr) diff --git a/parsing/printer.mli b/parsing/printer.mli index ca91cfd4f..6a256bd59 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -76,6 +76,7 @@ val pr_global_env : Idset.t -> global_reference -> std_ppcmds val pr_global : global_reference -> std_ppcmds val pr_constant : env -> constant -> std_ppcmds +val pr_existential_key : existential_key -> std_ppcmds val pr_existential : env -> existential -> std_ppcmds val pr_constructor : env -> constructor -> std_ppcmds val pr_inductive : env -> inductive -> std_ppcmds diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml index 4f8344745..5e574ce53 100644 --- a/plugins/subtac/subtac_cases.ml +++ b/plugins/subtac/subtac_cases.ml @@ -1576,7 +1576,7 @@ let constr_of_pat env isevars arsign pat avoid = in let neq = eq_id avoid id in (Name neq, Some (mkRel 0), eq_t) :: sign, 2, neq :: avoid - with Reduction.NotConvertible -> sign, 1, avoid + with NotUnifiable _ -> sign, 1, avoid in (* Mark the equality as a hole *) pat', sign, lift i app, lift i apptype, realargs, n + i, avoid diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml index 5a2d84057..2610ed4ed 100644 --- a/plugins/subtac/subtac_coercion.ml +++ b/plugins/subtac/subtac_coercion.ml @@ -112,7 +112,7 @@ module Coercion = struct try isevars := the_conv_x_leq env x y !isevars; None - with Reduction.NotConvertible -> coerce' env x y + with NotUnifiable _ -> coerce' env x y and coerce' env x y : (Term.constr -> Term.constr) option = let subco () = subset_coerce env isevars x y in let dest_prod c = @@ -129,12 +129,12 @@ module Coercion = struct let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in aux (hdx :: tele) (subst1 hdx restT) (subst1 hdy restT') (succ i) co - with Reduction.NotConvertible -> + with NotUnifiable _ -> let (n, eqT), restT = dest_prod typ in let (n', eqT'), restT' = dest_prod typ' in let _ = try isevars := the_conv_x_leq env eqT eqT' !isevars - with Reduction.NotConvertible -> raise NoSubtacCoercion + with NotUnifiable _ -> raise NoSubtacCoercion in (* Disallow equalities on arities *) if Reduction.is_arity env eqT then raise NoSubtacCoercion; @@ -323,6 +323,7 @@ module Coercion = struct (* appliquer le chemin de coercions de patterns p *) exception NoCoercion + exception NoCoercionNoUnifier of evar_map * unification_error let apply_pattern_coercion loc pat p = List.fold_left @@ -418,12 +419,12 @@ module Coercion = 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 @@ -447,7 +448,7 @@ module Coercion = struct let t2 = Termops.subst_term v1 t2 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) as _tycon) = @@ -458,12 +459,12 @@ module Coercion = struct inh_conv_coerce_to_fail loc env evd rigidonly (Some (nf_evar evd cj.uj_val)) (nf_evar evd cj.uj_type) (nf_evar evd t) - with NoCoercion -> + with NoCoercionNoUnifier (best_failed_evd,e) -> let sigma = evd in try coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t with NoSubtacCoercion -> - error_actual_type_loc loc env sigma cj t + error_actual_type_loc loc env sigma cj t e in let val' = match val' with Some v -> v | None -> assert(false) in (evd',{ uj_val = val'; uj_type = t }) @@ -490,7 +491,7 @@ module Coercion = struct in try fst (try inh_conv_coerce_to_fail loc env' isevars false None t t' - with NoCoercion -> + with NoCoercionNoUnifier _ -> coerce_itf loc env' isevars None t t') with NoSubtacCoercion -> error_cannot_coerce env' isevars (t, t')) diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 5503a147a..bedd3eb74 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 8b7fde3c2..cd505b1b7 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 e1f507b0a..d2d74ff96 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 774180c67..13d193658 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 a4c07a019..705ab356f 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 6d1c54e63..f663496df 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 30ee6aaf6..f95514ade 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 1ea2dbd00..003f507dc 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 6121ba7d8..6e39d9831 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] diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 8c4faa11c..b5770c8a7 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -431,7 +431,8 @@ let clenv_unify_binding_type clenv c t u = let evd,c = w_coerce_to_type (cl_env clenv) clenv.evd c t u in TypeProcessed, { clenv with evd = evd }, c with - | PretypeError (_,_,NotClean _) as e -> raise e + | PretypeError (_,_,ActualTypeNotCoercible (_,_,NotClean _)) as e -> + raise e | e when precatchable_exception e -> TypeNotProcessed, clenv, c diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 36268de1e..3d3707442 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,15 +25,17 @@ let depends_on_evar evk _ (pbty,_,t1,t2) = with NoHeadEvar -> false let define_and_solve_constraints evk c evd = - try - let evd = define evk c evd in - let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in - fst (List.fold_left - (fun (evd,b as p) (pbty,env,t1,t2) -> - if b then Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 else p) (evd,true) - pbs) - with e when Pretype_errors.precatchable_exception e -> - error "Instance does not satisfy constraints." + let evd = define evk c evd in + let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evk) in + match + List.fold_left + (fun p (pbty,env,t1,t2) -> match p with + | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2 + | UnifFailure _ as x -> x) (Success evd) + pbs + with + | Success evd -> evd + | UnifFailure _ -> error "Instance does not satisfy the constraints." let w_refine (evk,evi) (ltac_var,rawc) sigma = if Evd.is_defined sigma evk then diff --git a/proofs/logic.ml b/proofs/logic.ml index 2835eb542..747291869 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -55,8 +55,9 @@ let rec catchable_exception = function | Tacred.ReductionTacticError _ (* unification errors *) | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ - |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ - |CannotFindWellTypedAbstraction _|OccurCheck _ + |NoOccurrenceFound _|CannotUnifyBindingType _ + |ActualTypeNotCoercible _|UnifOccurCheck _ + |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true | Typeclasses_errors.TypeClassError (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 2802acfc1..87a1e02a8 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -401,7 +401,8 @@ let rec catchable_exception = function | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _) (* unification errors *) | PretypeError(_,_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _ - |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _ + |NoOccurrenceFound _|CannotUnifyBindingType _ + |ActualTypeNotCoercible _ |CannotFindWellTypedAbstraction _ |UnsolvableImplicit _)) -> true | Typeclasses_errors.TypeClassError diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6af1f9d56..f86d6d271 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -153,16 +153,46 @@ let explain_generalization env (name,var) j = str "it has type" ++ spc () ++ pt ++ spc () ++ str "which should be Set, Prop or Type." -let explain_actual_type env sigma j pt = +let explain_unification_error env p1 p2 = function + | None -> mt() + | Some e -> + match e with + | OccurCheck (evk,rhs) -> + spc () ++ str "(cannot define " ++ quote (pr_existential_key evk) ++ + strbrk " with term " ++ pr_lconstr_env env rhs ++ + strbrk "that would depend on itself)" + | NotClean (evk,c) -> + spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk) + ++ strbrk " because " ++ pr_lconstr_env env c ++ + strbrk " is out of scope)" + | NotSameArgSize | NotSameHead | NoCanonicalStructure -> + (* Error speaks from itself *) mt () + | ConversionFailed (env,t1,t2) -> + if t1 <> p1 || t2 <> p2 then + spc () ++ str "(cannot unify " ++ pr_lconstr_env env t1 ++ + strbrk " and " ++ pr_lconstr_env env t2 ++ str ")" + else mt () + | MetaOccurInBody evk -> + spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++ + strbrk " refers to a metavariable - please report your example)" + | InstanceNotSameType evk -> + spc () ++ str "(unable to find a well-typed instantiation for " ++ + quote (pr_existential_key evk) ++ str ")" + + +let explain_actual_type env sigma j t reason = let j = j_nf_betaiotaevar sigma j in - let pt = Reductionops.nf_betaiota sigma pt in + let t = Reductionops.nf_betaiota sigma t in let pe = pr_ne_context_of (str "In environment") env in let (pc,pct) = pr_ljudge_env env j in - let pt = pr_lconstr_env env pt in + let pt = pr_lconstr_env env t in + let ppreason = explain_unification_error env j.uj_type t reason in pe ++ + hov 0 ( str "The term" ++ brk(1,1) ++ pc ++ spc () ++ - str "has type" ++ brk(1,1) ++ pct ++ brk(1,1) ++ - str "while it is expected to have type" ++ brk(1,1) ++ pt ++ str "." + str "has type" ++ brk(1,1) ++ pct ++ spc () ++ + str "while it is expected to have type" ++ brk(1,1) ++ pt ++ + ppreason ++ str ".") let explain_cant_apply_bad_type env sigma (n,exptyp,actualtyp) rator randl = let randl = jv_nf_betaiotaevar sigma randl in @@ -420,13 +450,14 @@ let explain_wrong_case_info env ind ci = str "was given to a pattern-matching expression on the inductive type" ++ spc () ++ pc ++ str "." -let explain_cannot_unify env sigma m n = +let explain_cannot_unify env sigma m n e = let m = nf_evar sigma m in let n = nf_evar sigma n in let pm = pr_lconstr_env env m in let pn = pr_lconstr_env env n in + let ppreason = explain_unification_error env m n e in str "Impossible to unify" ++ brk(1,1) ++ pm ++ spc () ++ - str "with" ++ brk(1,1) ++ pn ++ str "." + str "with" ++ brk(1,1) ++ pn ++ ppreason ++ str "." let explain_cannot_unify_local env sigma m n subn = let pm = pr_lconstr_env env m in @@ -494,7 +525,7 @@ let explain_type_error env sigma err = | Generalization (nvar, c) -> explain_generalization env nvar c | ActualType (j, pt) -> - explain_actual_type env sigma j pt + explain_actual_type env sigma j pt None | CantApplyBadType (t, rator, randl) -> explain_cant_apply_bad_type env sigma t rator randl | CantApplyNonFunctional (rator, randl) -> @@ -511,13 +542,13 @@ let explain_pretype_error env sigma err = let env = make_all_name_different env in match err with | CantFindCaseType c -> explain_cant_find_case_type env sigma c - | OccurCheck (n,c) -> explain_occur_check env sigma n c - | NotClean (n,c,k) -> explain_not_clean env sigma n c k + | ActualTypeNotCoercible (j,t,e) -> explain_actual_type env sigma j t (Some e) + | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env evi k exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> explain_unexpected_type env sigma actual expect | NotProduct c -> explain_not_product env sigma c - | CannotUnify (m,n) -> explain_cannot_unify env sigma m n + | CannotUnify (m,n,e) -> explain_cannot_unify env sigma m n e | CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env sigma m n sn | CannotGeneralize ty -> explain_refiner_cannot_generalize env ty | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id |