Added propagation of evars unification failure reasons for better

error messages. The architecture of unification error handling
changed, not helped by ocaml for checking that every exceptions is
correctly caught. Report or fix if you find a regression.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13893 85f007b7-540e-0410-9357-904b9bb8a0f7

9 files changed, 185 insertions, 110 deletions

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]