From 6cbd65aa4e5fe82259b44b89e5e624ed2299249c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 7 Mar 2011 20:11:32 +0000
Subject: 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
---
 pretyping/pretype_errors.ml | 46 +++++++++++++++++++++++++++++++--------------
 1 file changed, 32 insertions(+), 14 deletions(-)

(limited to 'pretyping/pretype_errors.ml')

diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 6d1c54e63d..f663496dfb 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -18,15 +18,26 @@ open Type_errors
 open Glob_term
 open Inductiveops
 
+type unification_error =
+  | OccurCheck of existential_key * constr
+  | NotClean of existential_key * constr
+  | NotSameArgSize
+  | NotSameHead
+  | NoCanonicalStructure
+  | ConversionFailed of env * constr * constr
+  | MetaOccurInBody of existential_key
+  | InstanceNotSameType of existential_key
+
 type pretype_error =
   (* Old Case *)
   | CantFindCaseType of constr
-  (* Unification *)
-  | OccurCheck of existential_key * constr
-  | NotClean of existential_key * constr * Evd.hole_kind
+  (* Type inference unification *)
+  | ActualTypeNotCoercible of unsafe_judgment * types * unification_error
+  (* Tactic unification *)
+  | UnifOccurCheck of existential_key * constr
   | UnsolvableImplicit of Evd.evar_info * Evd.hole_kind *
       Evd.unsolvability_explanation option
-  | CannotUnify of constr * constr
+  | CannotUnify of constr * constr * unification_error option
   | CannotUnifyLocal of constr * constr * constr
   | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
@@ -95,6 +106,15 @@ let contract2 env a b = match contract env [a;b] with
 let contract3 env a b c = match contract env [a;b;c] with
   | env, [a;b;c] -> env,a,b,c | _ -> assert false
 
+let contract4 env a b c d = match contract env [a;b;c;d] with
+  | env, [a;b;c;d] -> (env,a,b,c),d | _ -> assert false
+
+let contract3' env a b c = function
+  | OccurCheck (evk,d) -> let x,d = contract4 env a b c d in x,OccurCheck(evk,d)
+  | NotClean (evk,d) -> let x,d = contract4 env a b c d in x,NotClean(evk,d)
+  | NotSameArgSize | NotSameHead | NoCanonicalStructure  | ConversionFailed _
+  | MetaOccurInBody _ | InstanceNotSameType _ as x -> contract3 env a b c, x
+
 let raise_pretype_error (loc,env,sigma,te) =
   Loc.raise loc (PretypeError(env,sigma,te))
 
@@ -102,10 +122,11 @@ let raise_located_type_error (loc,env,sigma,te) =
   Loc.raise loc (PretypeError(env,sigma,TypingError te))
 
 
-let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty =
-  let env, c, actty, expty = contract3 env c actty expty in
+let error_actual_type_loc loc env sigma {uj_val=c;uj_type=actty} expty reason =
+  let (env, c, actty, expty), reason = contract3' env c actty expty reason in
   let j = {uj_val=c;uj_type=actty} in
-  raise_located_type_error (loc, env, sigma, ActualType (j, expty))
+  raise_pretype_error
+    (loc, env, sigma, ActualTypeNotCoercible (j, expty, reason))
 
 let error_cant_apply_not_functional_loc loc env sigma rator randl =
   raise_located_type_error
@@ -137,23 +158,20 @@ let error_not_a_type_loc loc env sigma j =
     a precise location. *)
 
 let error_occur_check env sigma ev c =
-  raise (PretypeError (env, sigma, OccurCheck (ev,c)))
-
-let error_not_clean env sigma ev c (loc,k) =
-  Loc.raise loc (PretypeError (env, sigma, NotClean (ev,c,k)))
+  raise (PretypeError (env, sigma, UnifOccurCheck (ev,c)))
 
 let error_unsolvable_implicit loc env sigma evi e explain =
   Loc.raise loc
     (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain)))
 
-let error_cannot_unify env sigma (m,n) =
-  raise (PretypeError (env, sigma,CannotUnify (m,n)))
+let error_cannot_unify env sigma ?reason (m,n) =
+  raise (PretypeError (env, sigma,CannotUnify (m,n,reason)))
 
 let error_cannot_unify_local env sigma (m,n,sn) =
   raise (PretypeError (env, sigma,CannotUnifyLocal (m,n,sn)))
 
 let error_cannot_coerce env sigma (m,n) =
-  raise (PretypeError (env, sigma,CannotUnify (m,n)))
+  raise (PretypeError (env, sigma,CannotUnify (m,n,None)))
 
 let error_cannot_find_well_typed_abstraction env sigma p l =
   raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l)))
-- 
cgit v1.2.3