aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/coercion.ml19
-rw-r--r--pretyping/evarconv.ml248
-rw-r--r--pretyping/evarconv.mli8
-rw-r--r--pretyping/evarsolve.ml69
-rw-r--r--pretyping/evarsolve.mli22
-rw-r--r--pretyping/pretype_errors.ml57
-rw-r--r--pretyping/pretype_errors.mli29
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/unification.ml8
-rw-r--r--printing/printer.ml1
-rw-r--r--printing/printer.mli1
-rw-r--r--proofs/clenv.ml3
-rw-r--r--proofs/evar_refiner.ml21
-rw-r--r--proofs/logic.ml5
-rw-r--r--proofs/proofview.ml3
-rw-r--r--test-suite/output/names.out2
-rw-r--r--toplevel/himsg.ml65
17 files changed, 368 insertions, 199 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index f933bf1d3..aa172fc2a 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -30,6 +30,7 @@ open Termops
(* 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 =
@@ -122,7 +123,7 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
try
isevars := the_conv_x_leq env x y !isevars;
None
- with Reduction.NotConvertible -> coerce' env x y
+ with UnableToUnify _ -> 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 =
@@ -139,12 +140,12 @@ and coerce loc env isevars (x : Term.constr) (y : Term.constr)
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 UnableToUnify _ ->
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 UnableToUnify _ -> raise NoSubtacCoercion
in
(* Disallow equalities on arities *)
if Reduction.is_arity env eqT then raise NoSubtacCoercion;
@@ -416,11 +417,11 @@ let inh_coerce_to_fail env evd rigidonly v t c1 =
with Not_found -> raise NoCoercion
in
try (the_conv_x_leq env t' c1 evd, v')
- with Reduction.NotConvertible -> raise NoCoercion
+ with UnableToUnify _ -> 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 UnableToUnify (best_failed_evd,e) ->
try inh_coerce_to_fail env evd rigidonly v t c1
with NoCoercion ->
match
@@ -448,14 +449,14 @@ let rec inh_conv_coerce_to_fail loc env evd rigidonly v t c1 =
| 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 t =
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 _ ->
try
if Flags.is_program_mode () then
coerce_itf loc env evd (Some cj.uj_val) cj.uj_type t
@@ -464,8 +465,8 @@ let inh_conv_coerce_to_gen rigidonly loc env evd cj t =
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 (best_failed_evd,e) ->
+ 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 cb0bed51e..f65b5cc3e 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -20,6 +20,7 @@ open Evarutil
open Evarsolve
open Globnames
open Evd
+open Pretype_errors
type flex_kind_of_term =
| Rigid
@@ -128,16 +129,18 @@ 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
(* This function requires to get the outermost arguments first. It is
@@ -150,30 +153,32 @@ let ise_and evd l =
let generic_ise_list2 i f l1 l2 =
let rec aux i l1 l2 =
match l1,l2 with
- | [], [] -> (None,(i, true))
- | l, [] -> (Some (Inl (List.rev l)),(i, true))
- | [], l -> (Some (Inr (List.rev l)),(i, true))
+ | [], [] -> (None, Success i)
+ | l, [] -> (Some (Inl (List.rev l)), Success i)
+ | [], l -> (Some (Inr (List.rev l)), Success i)
| x::l1, y::l2 ->
- let (aa,(i',b)) = aux i l1 l2 in
- if b then (aa, f i' x y) else None, (i, false)
+ (match aux i l1 l2 with
+ | aa, Success i' -> (aa, f i' x y)
+ | _, (UnifFailure _ as x) -> None, x)
in aux i (List.rev l1) (List.rev l2)
(* Same but the 2 lists must have the same length *)
let ise_list2 evd f l1 l2 =
match generic_ise_list2 evd f l1 l2 with
| None, out -> out
- | _, _ -> (evd, false)
+ | _, (UnifFailure _ as out) -> out
+ | Some _, Success i -> UnifFailure (i,NotSameArgSize)
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 Int.equal lv1 (Array.length v2) then allrec evd (pred lv1)
- else (evd,false)
+ else UnifFailure (evd,NotSameArgSize)
(* This function tries to unify 2 stacks element by element. It works
from the end to the beginning. If it unifies a non empty suffix of
@@ -181,44 +186,47 @@ let ise_array2 evd f v1 v2 =
Some(the remaining prefixes to tackle)) *)
let ise_stack2 no_app env evd f sk1 sk2 =
let rec ise_stack2 deep i sk1 sk2 =
- let fal () = if deep then Some (List.rev sk1, List.rev sk2), (i,deep)
- else None, (evd, false) in
+ let fail x = if deep then Some (List.rev sk1, List.rev sk2), Success i
+ else None, x in
match sk1, sk2 with
- | [], [] -> None, (i,true)
+ | [], [] -> None, Success i
| Zcase (_,t1,c1,_)::q1, Zcase (_,t2,c2,_)::q2 ->
- let (i',b') = f env i CONV t1 t2 in
- if b' then
- let (i'',b'') = ise_array2 i' (fun ii -> f env ii CONV) c1 c2 in
- if b'' then ise_stack2 true i'' q1 q2 else fal ()
- else fal ()
+ (match f env i CONV t1 t2 with
+ | Success i' ->
+ (match ise_array2 i' (fun ii -> f env ii CONV) c1 c2 with
+ | Success i'' -> ise_stack2 true i'' q1 q2
+ | UnifFailure _ as x -> fail x)
+ | UnifFailure _ as x -> fail x)
| Zfix (((li1, i1),(_,tys1,bds1 as recdef1)),a1,_)::q1, Zfix (((li2, i2),(_,tys2,bds2)),a2,_)::q2 ->
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
- let (i',b') = ise_and i [
+ match ise_and i [
(fun i -> ise_array2 i (fun ii -> f env ii CONV) tys1 tys2);
(fun i -> ise_array2 i (fun ii -> f (push_rec_types recdef1 env) ii CONV) bds1 bds2);
- (fun i -> ise_list2 i (fun ii -> f env ii CONV) a1 a2)] in
- if b' then ise_stack2 true i' q1 q2 else fal ()
- else fal ()
+ (fun i -> ise_list2 i (fun ii -> f env ii CONV) a1 a2)] with
+ | Success i' -> ise_stack2 true i' q1 q2
+ | UnifFailure _ as x -> fail x
+ else fail (UnifFailure (i,NotSameHead))
| Zupdate _ :: _, _ | Zshift _ :: _, _
| _, Zupdate _ :: _ | _, Zshift _ :: _ -> assert false
- | Zapp l1 :: q1, Zapp l2 :: q2 -> if no_app&&deep then fal () else begin
+ | Zapp l1 :: q1, Zapp l2 :: q2 ->
+ if no_app&&deep then fail ((*dummy*)UnifFailure(i,NotSameHead)) else begin
(* Is requiring to match on all the shorter list a restriction
here ? we could imagine a generalization of
generic_ise_list2 that succeed when it matches only a strict
non empty suffix of both lists and returns in this case the 2
prefixes *)
match generic_ise_list2 i (fun ii -> f env ii CONV) l1 l2 with
- |_,(_, false) -> fal ()
- |None,(i', true) -> ise_stack2 true i' q1 q2
- |Some (Inl r),(i', true) -> ise_stack2 true i' (Zapp r :: q1) q2
- |Some (Inr r),(i', true) -> ise_stack2 true i' q1 (Zapp r :: q2)
+ |_,(UnifFailure _ as x) -> fail x
+ |None,Success i' -> ise_stack2 true i' q1 q2
+ |Some (Inl r),Success i' -> ise_stack2 true i' (Zapp r :: q1) q2
+ |Some (Inr r),Success i' -> ise_stack2 true i' q1 (Zapp r :: q2)
end
- |_, _ -> fal ()
+ |_, _ -> fail (UnifFailure (i,(* Maybe improve: *) NotSameHead))
in ise_stack2 false evd (List.rev sk1) (List.rev sk2)
(* Make sure that the matching suffix is the all stack *)
let exact_ise_stack2 env evd f sk1 sk2 =
- match ise_stack2 false env evd f sk1 sk2 with | None, out -> out | _ -> (evd, false)
+ match ise_stack2 false env evd f sk1 sk2 with | None, out -> out | _ -> UnifFailure (evd, NotSameArgSize)
let rec evar_conv_x ts env evd pbty term1 term2 =
let term1 = whd_head_evar evd term1 in
@@ -234,7 +242,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 *)
@@ -252,6 +261,8 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
and evar_eqappr_x ?(rhs_is_already_stuck = false)
ts env evd pbty (term1,sk1 as appr1) (term2,sk2 as appr2) =
+ let default_fail i = (* costly *)
+ UnifFailure (i,ConversionFailed (env, zip appr1, zip appr2)) in
let miller_pfenning on_left fallback ev (_,skF) apprM evd =
let tM = zip apprM in
Option.cata
@@ -264,29 +275,30 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
(position_problem on_left pbty,ev,t2)
) fallback
(is_unification_pattern_evar env evd ev lF tM)
- ) (evd, false) (list_of_app_stack skF) in
+ ) (default_fail evd) (list_of_app_stack skF) in
let flex_maybeflex on_left ev (termF,skF as apprF) (termM, skM as apprM) =
let switch f a b = if on_left then f a b else f b a in
let not_only_app = not_purely_applicative_stack skM in
let f1 i = miller_pfenning on_left
(if not_only_app then (* Postpone the use of an heuristic *)
- switch (fun x y -> add_conv_pb (pbty,env,zip x,zip y) i, true) apprF apprM
- else (i,false))
+ switch (fun x y -> Success (add_conv_pb (pbty,env,zip x,zip y) i)) apprF apprM
+ else default_fail i)
ev apprF apprM i
and f2 i =
match switch (ise_stack2 not_only_app env i (evar_conv_x ts)) skF skM with
- |Some (l,r), (i', true) when on_left && (not_only_app || l = []) ->
+ |Some (l,r), Success i' when on_left && (not_only_app || l = []) ->
switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
- |Some (r,l), (i', true) when not on_left && (not_only_app || l = []) ->
+ |Some (r,l), Success i' when not on_left && (not_only_app || l = []) ->
switch (evar_conv_x ts env i' pbty) (zip(termF,l)) (zip(termM,r))
- |None, (i', true) -> switch (evar_conv_x ts env i' pbty) termF termM
- |_ -> (i, false)
+ |None, Success i' -> switch (evar_conv_x ts env i' pbty) termF termM
+ |_, (UnifFailure _ as x) -> x
+ |Some _, _ -> UnifFailure (i,NotSameArgSize)
and f3 i =
match eval_flexible_term ts env termM with
| Some vM ->
switch (evar_eqappr_x ts env i pbty) apprF
(whd_betaiota_deltazeta_for_iota_state ts env i (vM, skM))
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2; f3] in
let eta env evd onleft sk term sk' term' =
@@ -306,19 +318,24 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| Flexible (sp1,al1 as ev1), Flexible (sp2,al2 as ev2) ->
let f1 i =
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
- |None, (i', true) -> solve_simple_eqn (evar_conv_x ts) env i'
+ |None, Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
(position_problem true pbty,ev1,term2)
- |Some (r,[]), (i', true) -> solve_simple_eqn (evar_conv_x ts) env i'
+ |Some (r,[]), Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
(position_problem false pbty,ev2,zip(term1,r))
- |Some ([],r), (i', true) -> solve_simple_eqn (evar_conv_x ts) env i'
+ |Some ([],r), Success i' -> solve_simple_eqn (evar_conv_x ts) env i'
(position_problem true pbty,ev1,zip(term2,r))
- |_, (_, _) -> (i, false)
+ |_, (UnifFailure _ as x) -> x
+ |Some _, _ -> UnifFailure (i,NotSameArgSize)
and f2 i =
if Int.equal sp1 sp2 then
match ise_stack2 false env i (evar_conv_x ts) sk1 sk2 with
- |None, (i', true) -> solve_refl (evar_conv_x ts) env i' sp1 al1 al2, true
- |_ -> i, false
- else (i,false)
+ |None, Success 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)
+ |_, (UnifFailure _ as x) -> x
+ |Some _, _ -> UnifFailure (i,NotSameArgSize)
+ else UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2]
@@ -349,12 +366,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
if eq_constr term1 term2 then
exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2
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
@@ -387,7 +404,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
match eval_flexible_term ts env term2 with
| Some v2 ->
evar_eqappr_x ts env i pbty appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2))
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
else
match eval_flexible_term ts env term2 with
| Some v2 ->
@@ -396,7 +413,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
match eval_flexible_term ts env term1 with
| Some v1 ->
evar_eqappr_x ts env i pbty (whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2
- | None -> (i,false)
+ | None -> UnifFailure (i,NotSameHead)
in
ise_try evd [f1; f2; f3]
end
@@ -414,31 +431,31 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| Flexible ev1, Rigid ->
let f1 evd =
miller_pfenning true
- ((* Postpone the use of an heuristic *)
- add_conv_pb (pbty,env,zip appr1,zip appr2) evd, true)
+ (Success ((* Postpone the use of an heuristic *)
+ add_conv_pb (pbty,env,zip appr1,zip appr2) evd))
ev1 appr1 appr2 evd
and f2 evd =
if isLambda term2 then
eta env evd false sk2 term2 sk1 term1
- else (evd,false)
+ else UnifFailure (evd,NotSameHead)
in ise_try evd [f1;f2]
| Rigid, Flexible ev2 ->
let f1 evd =
miller_pfenning false
- ((* Postpone the use of an heuristic *)
- add_conv_pb (pbty,env,zip appr1,zip appr2) evd, true)
+ (Success ((* Postpone the use of an heuristic *)
+ add_conv_pb (pbty,env,zip appr1,zip appr2) evd))
ev2 appr2 appr1 evd
and f2 evd =
if isLambda term1 then
eta env evd true sk1 term1 sk2 term2
- else (evd,false)
+ else UnifFailure (evd,NotSameHead)
in ise_try evd [f1;f2]
| MaybeFlexible, Rigid ->
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 ts env term1 with
| Some v1 ->
@@ -446,14 +463,14 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
(whd_betaiota_deltazeta_for_iota_state ts env i (v1,sk1)) appr2
| None ->
if isLambda term2 then eta env evd false sk2 term2 sk1 term1
- else (i,false)
+ else UnifFailure (i,NotSameHead)
in
ise_try evd [f3; f4]
| Rigid, MaybeFlexible ->
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 ts env term2 with
| Some v2 ->
@@ -461,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
appr1 (whd_betaiota_deltazeta_for_iota_state ts env i (v2,sk2))
| None ->
if isLambda term1 then eta env evd true sk1 term1 sk2 term2
- else (i,false)
+ else UnifFailure (i,NotSameHead)
in
ise_try evd [f3; f4]
@@ -481,9 +498,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
if pbty == CONV
then Evd.set_eq_sort evd s1 s2
else Evd.set_leq_sort evd s1 s2
- in (evd', true)
- with Univ.UniverseInconsistency _ -> (evd, false)
- | _ -> (evd, false))
+ in Success evd'
+ with Univ.UniverseInconsistency _ ->
+ UnifFailure (evd,UnifUnivInconsistency)
+ | _ -> UnifFailure (evd,NotSameHead))
| Prod (n,c1,c'1), Prod (_,c2,c'2) when app_empty ->
ise_and evd
@@ -495,12 +513,12 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
| Ind sp1, Ind sp2 ->
if eq_ind sp1 sp2 then
exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else (evd, false)
+ else UnifFailure (evd,NotSameHead)
| Construct sp1, Construct sp2 ->
if eq_constructor sp1 sp2 then
exact_ise_stack2 env evd (evar_conv_x ts) sk1 sk2
- else (evd, false)
+ else UnifFailure (evd,NotSameHead)
| Fix ((li1, i1),(_,tys1,bds1 as recdef1)), Fix ((li2, i2),(_,tys2,bds2)) -> (* Partially applied fixs *)
if Int.equal i1 i2 && Array.equal Int.equal li1 li2 then
@@ -508,7 +526,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
(fun i -> ise_array2 i (fun i' -> evar_conv_x ts env i' CONV) tys1 tys2);
(fun i -> ise_array2 i (fun i' -> evar_conv_x ts (push_rec_types recdef1 env) i' CONV) bds1 bds2);
(fun i -> exact_ise_stack2 env i (evar_conv_x ts) sk1 sk2)]
- else (evd, false)
+ else UnifFailure (evd, NotSameHead)
| CoFix (i1,(_,tys1,bds1 as recdef1)), CoFix (i2,(_,tys2,bds2)) ->
if Int.equal i1 i2 then
@@ -520,17 +538,17 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false)
bds1 bds2);
(fun i -> exact_ise_stack2 env i
(evar_conv_x ts) sk1 sk2)]
- else (evd,false)
+ else UnifFailure (evd,NotSameHead)
| (Meta _, _) | (_, Meta _) ->
begin match ise_stack2 true env evd (evar_conv_x ts) sk1 sk2 with
- |_, (_, false) -> (evd, false)
- |None, (i', true) -> evar_conv_x ts env i' CONV term1 term2
- |Some (sk1',sk2'), (i', true) -> evar_conv_x ts env i' CONV (zip (term1,sk1')) (zip (term2,sk2'))
+ |_, (UnifFailure _ as x) -> x
+ |None, Success i' -> evar_conv_x ts env i' CONV term1 term2
+ |Some (sk1',sk2'), Success i' -> evar_conv_x ts env i' CONV (zip (term1,sk1')) (zip (term2,sk2'))
end
- | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _), _ -> (evd,false)
- | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _) -> (evd,false)
+ | (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _), _ -> UnifFailure (evd,NotSameHead)
+ | _, (Ind _ | Construct _ | Sort _ | Prod _ | CoFix _ | Fix _) -> UnifFailure (evd,NotSameHead)
| (App _ | Cast _ | Case _), _ -> assert false
| (LetIn _ | Rel _ | Var _ | Const _ | Evar _), _ -> assert false
@@ -584,8 +602,8 @@ let choose_less_dependent_instance evk evd term args =
let subst = make_pure_subst evi args in
let subst' = List.filter (fun (id,c) -> eq_constr c term) subst in
match subst' with
- | [] -> evd, false
- | (id, _) :: _ -> Evd.define evk (mkVar id) evd, true
+ | [] -> None
+ | (id, _) :: _ -> Some (Evd.define evk (mkVar id) evd)
let apply_on_subterm f c t =
let rec applyrec (k,c as kc) t =
@@ -699,10 +717,12 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
(* and we use typing to propagate this instantiation *)
(* This is an arbitrary choice *)
let evd = Evd.define evk (mkVar id) evd in
- let evd,b = evar_conv_x ts env_evar evd CUMUL idty evty in
- if not b then error "Cannot find an instance";
- let evd,b = reconsider_conv_pbs (evar_conv_x ts) evd in
- if not b then error "Cannot find an instance";
+ match evar_conv_x ts env_evar evd CUMUL idty evty with
+ | UnifFailure _ -> error "Cannot find an instance"
+ | Success evd ->
+ match reconsider_conv_pbs (evar_conv_x ts) evd with
+ | UnifFailure _ -> error "Cannot find an instance"
+ | Success evd ->
evd
else
evd
@@ -722,9 +742,10 @@ let second_order_matching_with_args ts env evd ev l t =
(*
let evd,ev = evar_absorb_arguments env evd ev l in
let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in
- second_order_matching ts env evd ev argoccs t
+ let evd, b = second_order_matching ts env evd ev argoccs t in
+ if b then Success evd else
*)
- (evd,false)
+ UnifFailure (evd, ConversionFailed (env,applist(mkEvar ev,l),t))
let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in
@@ -737,18 +758,22 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
&& Array.for_all (fun a -> eq_constr a term2 || isEvar a) args1 ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
- choose_less_dependent_instance evk1 evd term2 args1
+ (match choose_less_dependent_instance evk1 evd term2 args1 with
+ | Some evd -> Success evd
+ | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- && Array.for_all (fun a -> eq_constr a term1 || isEvar a) args2 ->
+ & Array.for_all (fun a -> eq_constr 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
+ (match choose_less_dependent_instance evk2 evd term1 args2 with
+ | Some evd -> Success evd
+ | None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| Evar (evk1,args1), Evar (evk2,args2) when Int.equal evk1 evk2 ->
- let f env evd pbty x y = (evd,is_trans_fconv pbty ts env evd x y) in
- solve_refl ~can_drop:true f env evd evk1 args1 args2, true
+ let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in
+ Success (solve_refl ~can_drop:true f env evd evk1 args1 args2)
| Evar ev1, Evar ev2 ->
- solve_evar_evar ~force:true
- (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2, true
+ Success (solve_evar_evar ~force:true
+ (evar_define (evar_conv_x ts)) (evar_conv_x ts) env evd ev1 ev2)
| Evar ev1,_ when List.length l1 <= List.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
(* and otherwise second-order matching *)
@@ -806,9 +831,9 @@ let rec solve_unconstrained_evars_with_canditates evd =
let conv_algo = evar_conv_x full_transparent_state in
let evd = check_evar_instance evd evk a conv_algo in
let evd = Evd.define evk a evd in
- let evd,b = reconsider_conv_pbs conv_algo evd in
- if b then solve_unconstrained_evars_with_canditates evd
- else aux l
+ match reconsider_conv_pbs conv_algo evd with
+ | Success evd -> solve_unconstrained_evars_with_canditates evd
+ | UnifFailure _ -> aux l
with e when Pretype_errors.precatchable_exception e ->
aux l in
(* List.rev is there to favor most dependent solutions *)
@@ -827,15 +852,16 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
let rec aux evd pbs progress stuck =
match pbs with
| (pbty,env,t1,t2 as pb) :: pbs ->
- let evd', b = apply_conversion_problem_heuristic ts env evd pbty t1 t2 in
- if b then
- let (evd', rest) = extract_all_conv_pbs evd' in
- begin match rest with
- | [] -> aux evd' pbs true stuck
- | _ -> (* Unification got actually stuck, postpone *)
+ (match apply_conversion_problem_heuristic ts env evd pbty t1 t2 with
+ | Success evd' ->
+ let (evd', rest) = extract_all_conv_pbs evd' in
+ begin match rest with
+ | [] -> aux evd' pbs true stuck
+ | _ -> (* Unification got actually stuck, postpone *)
aux evd pbs progress (pb :: stuck)
- end
- else Pretype_errors.error_cannot_unify env evd (t1, t2)
+ end
+ | UnifFailure (evd,reason) ->
+ Pretype_errors.error_cannot_unify env evd ~reason (t1, t2))
| _ ->
if progress then aux evd stuck false []
else
@@ -852,22 +878,24 @@ let consider_remaining_unif_problems ?(ts=full_transparent_state) env evd =
(* Main entry points *)
+exception UnableToUnify 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 (UnableToUnify (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 (UnableToUnify (evd',e))
let e_conv ?(ts=full_transparent_state) env evdref t1 t2 =
match evar_conv_x ts env !evdref CONV t1 t2 with
- (evd',true) -> evdref := evd'; true
- | _ -> false
+ | Success evd' -> evdref := evd'; true
+ | _ -> false
let e_cumul ?(ts=full_transparent_state) env evdref t1 t2 =
match evar_conv_x ts env !evdref CUMUL t1 t2 with
- (evd',true) -> evdref := evd'; true
- | _ -> false
+ | Success evd' -> evdref := evd'; true
+ | _ -> false
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 285c509f1..d3f8b451a 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -15,7 +15,9 @@ open Reductionops
open Evd
open Locus
-(** returns exception Reduction.NotConvertible if not unifiable *)
+exception UnableToUnify 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
@@ -27,11 +29,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 -> Evarsolve.unification_result
val evar_eqappr_x : transparent_state ->
env -> evar_map ->
conv_pb -> constr * constr stack -> constr * constr stack ->
- evar_map * bool
+ Evarsolve.unification_result
(**/**)
val consider_remaining_unif_problems : ?ts:transparent_state -> env -> evar_map -> evar_map
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 1b8518098..a63f1b1c8 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -26,6 +26,19 @@ let normalize_evar evd ev =
| _ -> assert false
(************************)
+(* Unification results *)
+(************************)
+
+type unification_result =
+ | Success of evar_map
+ | UnifFailure of evar_map * unification_error
+
+let is_success = function Success _ -> true | UnifFailure _ -> false
+
+let test_success conv_algo env evd c c' rhs =
+ is_success (conv_algo env evd c c' rhs)
+
+(************************)
(* Manipulating filters *)
(************************)
@@ -504,6 +517,9 @@ let restrict_upon_filter evd evk p args =
let oldfullfilter = evar_filter (Evd.find_undefined evd evk) in
Some (apply_subfilter oldfullfilter newfilter)
+(***************)
+(* Unification *)
+
(* Inverting constructors in instances (common when inferring type of match) *)
let find_projectable_constructor env evd cstr k args cstr_subst =
@@ -883,8 +899,9 @@ let are_canonical_instances args1 args2 env =
let filter_compatible_candidates conv_algo env evd evi args rhs c =
let c' = instantiate_evar (evar_filtered_context evi) c args in
- let evd, b = conv_algo env evd Reduction.CONV rhs c' in
- if b then Some (c,evd) else None
+ match conv_algo env evd Reduction.CONV rhs c' with
+ | Success evd -> Some (c,evd)
+ | UnifFailure _ -> None
exception DoesNotPreserveCandidateRestriction
@@ -1012,7 +1029,10 @@ let solve_evar_evar ?(force=false) f g env evd (evk1,args1 as ev1) (evk2,args2 a
postpone_evar_evar f env evd filter1 ev1 filter2 ev2
type conv_fun =
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
+ env -> evar_map -> conv_pb -> constr -> constr -> unification_result
+
+type conv_fun_bool =
+ env -> evar_map -> conv_pb -> constr -> constr -> bool
let check_evar_instance evd evk1 body conv_algo =
let evi = Evd.find evd evk1 in
@@ -1022,9 +1042,11 @@ let check_evar_instance evd evk1 body conv_algo =
try Retyping.get_type_of evenv evd body
with _ -> error "Ill-typed evar instance"
in
- let evd,b = conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl in
- if b then evd else
- user_err_loc (fst (evar_source evk1 evd),"",
+ match conv_algo evenv evd Reduction.CUMUL ty evi.evar_concl with
+ | Success evd -> evd
+ | UnifFailure (evd,d) ->
+ (* TODO: use the error? *)
+ user_err_loc (fst (evar_source evk1 evd),"",
str "Unable to find a well-typed instantiation")
(* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
@@ -1037,7 +1059,7 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
(* Filter and restrict if needed *)
let untypedfilter =
restrict_upon_filter evd 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
let candidates = filter_candidates evd evk untypedfilter None in
let filter = match untypedfilter with
@@ -1105,6 +1127,8 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
exception NotInvertibleUsingOurAlgorithm of constr
exception NotEnoughInformationToProgress of (Id.t * evar_projection) list
exception OccurCheckIn of evar_map * constr
+exception MetaOccurInBodyInternal
+exception InstanceNotSameTypeInternal
let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
let aliases = make_alias_map env in
@@ -1254,7 +1278,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
match kind_of_term rhs with
| Evar (evk2,argsv2 as ev2) ->
if Int.equal evk evk2 then
- solve_refl ~can_drop:choose conv_algo env evd evk argsv argsv2
+ solve_refl ~can_drop:choose
+ (test_success conv_algo) env evd evk argsv argsv2
else
solve_evar_evar ~force:choose
(evar_define conv_algo) conv_algo env evd ev ev2
@@ -1263,7 +1288,7 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
with NoCandidates ->
try
let (evd',body) = invert_definition conv_algo 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));
@@ -1290,18 +1315,17 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
with
| NotEnoughInformationToProgress sols ->
postpone_non_unique_projection env evd ev sols 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 Int.equal 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))
(* This code (i.e. solve_pb, etc.) takes a unification
* problem, and tries to solve it. If it solves it, then it removes
@@ -1336,8 +1360,10 @@ let status_changed lev (pbty,_,t1,t2) =
let reconsider_conv_pbs conv_algo evd =
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
(* Tries to solve problem t1 = t2.
@@ -1358,6 +1384,13 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
| _ ->
evar_define conv_algo ~choose env evd ev1 t2 in
reconsider_conv_pbs conv_algo evd
- with e when precatchable_exception e ->
- (evd,false)
+ with
+ | NotInvertibleUsingOurAlgorithm t ->
+ UnifFailure (evd,NotClean (ev1,t))
+ | OccurCheckIn (evd,rhs) ->
+ UnifFailure (evd,OccurCheck (evk1,rhs))
+ | MetaOccurInBodyInternal ->
+ UnifFailure (evd,MetaOccurInBody evk1)
+ | InstanceNotSameTypeInternal ->
+ UnifFailure (evd,InstanceNotSameType evk1)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 6c7635449..e34332c9b 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -10,21 +10,31 @@ open Term
open Evd
open Environ
+type unification_result =
+ | Success of evar_map
+ | UnifFailure of evar_map * Pretype_errors.unification_error
+
+val is_success : unification_result -> bool
+
(** Replace the vars and rels that are aliases to other vars and rels by
their representative that is most ancient in the context *)
val expand_vars_in_term : env -> constr -> constr
-type conv_fun =
- env -> evar_map -> conv_pb -> constr -> constr -> evar_map * bool
-
(** [evar_define choose env ev c] try to instantiate [ev] with [c] (typed in [env]),
possibly solving related unification problems, possibly leaving open
some problems that cannot be solved in a unique way (except if choose is
true); fails if the instance is not valid for the given [ev] *)
+
+type conv_fun =
+ env -> evar_map -> conv_pb -> constr -> constr -> unification_result
+
+type conv_fun_bool =
+ env -> evar_map -> conv_pb -> constr -> constr -> bool
+
val evar_define : conv_fun -> ?choose:bool -> env -> evar_map ->
existential -> constr -> evar_map
-val solve_refl : ?can_drop:bool -> conv_fun -> env -> evar_map ->
+val solve_refl : ?can_drop:bool -> conv_fun_bool -> env -> evar_map ->
existential_key -> constr array -> constr array -> evar_map
val solve_evar_evar : ?force:bool ->
@@ -32,9 +42,9 @@ val solve_evar_evar : ?force:bool ->
env -> evar_map -> existential -> existential -> evar_map
val solve_simple_eqn : conv_fun -> ?choose:bool -> env -> evar_map ->
- bool option * existential * constr -> evar_map * bool
+ bool option * existential * constr -> unification_result
-val reconsider_conv_pbs : conv_fun -> evar_map -> evar_map * bool
+val reconsider_conv_pbs : conv_fun -> evar_map -> unification_result
val is_unification_pattern_evar : env -> evar_map -> existential -> constr list ->
constr -> constr list option
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 19ccb2375..f3235b9d1 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -14,15 +14,27 @@ open Namegen
open Environ
open Type_errors
+type unification_error =
+ | OccurCheck of existential_key * constr
+ | NotClean of existential * constr
+ | NotSameArgSize
+ | NotSameHead
+ | NoCanonicalStructure
+ | ConversionFailed of env * constr * constr
+ | MetaOccurInBody of existential_key
+ | InstanceNotSameType of existential_key
+ | UnifUnivInconsistency
+
type pretype_error =
(* Old Case *)
| CantFindCaseType of constr
- (* Unification *)
- | OccurCheck of existential_key * constr
- | NotClean of existential_key * constr * Evar_kinds.t
+ (* Type inference unification *)
+ | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ (* Tactic unification *)
+ | UnifOccurCheck of existential_key * constr
| UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
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
@@ -69,6 +81,25 @@ 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 contract4_vect env a b c d v =
+ match contract env ([a;b;c;d] @ Array.to_list v) with
+ | env, a::b::c::d::l -> (env,a,b,c),d,Array.of_list l
+ | _ -> 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,args),d) ->
+ let x,d,args = contract4_vect env a b c d args in x,NotClean((evk,args),d)
+ | ConversionFailed (env',t1,t2) ->
+ let (env',t1,t2) = contract2 env' t1 t2 in
+ contract3 env a b c, ConversionFailed (env',t1,t2)
+ | NotSameArgSize | NotSameHead | NoCanonicalStructure
+ | MetaOccurInBody _ | InstanceNotSameType _
+ | UnifUnivInconsistency as x -> contract3 env a b c, x
+
let raise_pretype_error (loc,env,sigma,te) =
Loc.raise loc (PretypeError(env,sigma,te))
@@ -76,10 +107,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
@@ -111,23 +143,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 3a4c6aad5..b57111bc6 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -16,15 +16,27 @@ open Inductiveops
(** {6 The type of errors raised by the pretyper } *)
+type unification_error =
+ | OccurCheck of existential_key * constr
+ | NotClean of existential * constr
+ | NotSameArgSize
+ | NotSameHead
+ | NoCanonicalStructure
+ | ConversionFailed of env * constr * constr
+ | MetaOccurInBody of existential_key
+ | InstanceNotSameType of existential_key
+ | UnifUnivInconsistency
+
type pretype_error =
(** Old Case *)
| CantFindCaseType of constr
- (** Unification *)
- | OccurCheck of existential_key * constr
- | NotClean of existential_key * constr * Evar_kinds.t
+ (** Type inference unification *)
+ | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+ (** Tactic Unification *)
+ | UnifOccurCheck of existential_key * constr
| UnsolvableImplicit of Evd.evar_info * Evar_kinds.t *
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
@@ -45,7 +57,8 @@ val precatchable_exception : exn -> bool
(** Raising errors *)
val error_actual_type_loc :
- Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr -> 'b
+ Loc.t -> env -> Evd.evar_map -> unsafe_judgment -> constr ->
+ unification_error -> 'b
val error_cant_apply_not_functional_loc :
Loc.t -> env -> Evd.evar_map ->
@@ -79,14 +92,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.t * Evar_kinds.t -> 'b
-
val error_unsolvable_implicit :
Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t ->
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 ed087fa25..0321707b0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -650,7 +650,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
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
else user_err_loc (loc,"",str "Cannot check cast with vm: " ++
str "unresolved arguments remain.")
@@ -662,7 +663,8 @@ let rec pretype (tycon : type_constraint) env evdref lvar = function
try
ignore (Nativeconv.native_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
else user_err_loc (loc,"",str "Cannot check cast with native compiler: " ++
str "unresolved arguments remain.")
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index d6f1fac88..4c0f12d3c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -831,9 +831,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/printing/printer.ml b/printing/printer.ml
index 7a9dcb03c..fa776d11e 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -127,6 +127,7 @@ let pr_global_env = pr_global_env
let pr_global = pr_global_env Id.Set.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/printing/printer.mli b/printing/printer.mli
index 2340b310f..2c6800a11 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -80,6 +80,7 @@ val pr_global_env : Id.Set.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/proofs/clenv.ml b/proofs/clenv.ml
index 158f8e94f..6177040cc 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -434,7 +434,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 71a07326f..92ee55e43 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -11,6 +11,7 @@ open Util
open Names
open Evd
open Evarutil
+open Evarsolve
(******************************************)
(* Instantiation of existential variables *)
@@ -23,15 +24,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 267e9d5bf..80a2e1d1a 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -50,8 +50,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 _|AbstractionOverMeta _)) -> true
| Typeclasses_errors.TypeClassError
(_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index c18c48744..7b384b13e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -342,7 +342,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/test-suite/output/names.out b/test-suite/output/names.out
index 90ad4ba09..1f13619cb 100644
--- a/test-suite/output/names.out
+++ b/test-suite/output/names.out
@@ -2,4 +2,4 @@ The command has indeed failed with message:
=> Error: In environment
y : nat
The term "a y" has type "{y0 : nat | y = y0}"
- while it is expected to have type "{x : nat | x = y}".
+ while it is expected to have type "{x : nat | x = y}".
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 93c3a3b1a..848bf5232 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -149,16 +149,58 @@ 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 sigma p1 p2 = function
+ | None -> mt()
+ | Some e ->
+ match e with
+ | OccurCheck (evk,rhs) ->
+ let rhs = Evarutil.nf_evar sigma rhs in
+ 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,args),c) ->
+ let c = Evarutil.nf_evar sigma c in
+ let args = Array.map (Evarutil.nf_evar sigma) args in
+ spc () ++ str "(cannot instantiate " ++ quote (pr_existential_key evk)
+ ++ strbrk " because " ++ pr_lconstr_env env c ++
+ strbrk " is not in its scope" ++
+ (if args = [||] then mt() else
+ strbrk ": available arguments are " ++
+ pr_sequence (pr_lconstr_env env) (List.rev (Array.to_list args))) ++
+ str ")"
+ | NotSameArgSize | NotSameHead | NoCanonicalStructure ->
+ (* Error speaks from itself *) mt ()
+ | ConversionFailed (env,t1,t2) ->
+ if eq_constr t1 p1 & eq_constr t2 p2 then mt () else
+ let env = make_all_name_different env in
+ let t1 = Evarutil.nf_evar sigma t1 in
+ let t2 = Evarutil.nf_evar sigma t2 in
+ 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 ")"
+ | UnifUnivInconsistency ->
+ spc () ++ str "(Universe inconsistency)"
+
+let explain_actual_type env sigma j t reason =
let j = Evarutil.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 sigma 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 = Evarutil.jv_nf_betaiotaevar sigma randl in
@@ -413,13 +455,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 = Evarutil.nf_evar sigma m in
let n = Evarutil.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 sigma 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 +537,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 +554,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
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-06 04:20:29 +0000