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@16205 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 54 insertions, 11 deletions

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