Repairing r16205: errors raised by check_evar_instance were no longer

trapped by solve_simple_eqn.

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

6 files changed, 22 insertions, 17 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 1258e4a09..6d6aa6d5d 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -854,8 +854,9 @@ let rec solve_unconstrained_evars_with_canditates evd =
             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
+          with
+          | IllTypedInstance _ as e
+          | e when Pretype_errors.precatchable_exception e -> aux l in
       (* List.rev is there to favor most dependent solutions *)
       (* and favor progress when used with the refine tactics *)
       let evd = aux (List.rev l) in
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index f29d982c2..01878024b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1034,6 +1034,8 @@ type conv_fun =
 type conv_fun_bool =
   env ->  evar_map -> conv_pb -> constr -> constr -> bool
 
+exception IllTypedInstance of env * types * types
+
 let check_evar_instance evd evk1 body conv_algo =
   let evi = Evd.find evd evk1 in
   let evenv = evar_env evi in
@@ -1044,10 +1046,7 @@ let check_evar_instance evd evk1 body conv_algo =
   in
   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")
+  | UnifFailure _ -> raise (IllTypedInstance (evenv,ty,evi.evar_concl))
 
 (* Solve pbs ?e[t1..tn] = ?e[u1..un] which arise often in fixpoint
  * definitions. We try to unify the ti with the ui pairwise. The pairs
@@ -1128,7 +1127,6 @@ 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
@@ -1310,8 +1308,8 @@ and evar_define conv_algo ?(choose=false) env evd (evk,argsv as ev) rhs =
            str "----> " ++ int ev ++ str " := " ++
            print_constr body);
         raise e in*)
-    let evd' = Evd.define evk body evd' in
-    check_evar_instance evd' evk body conv_algo
+    let evd' = check_evar_instance evd' evk body conv_algo in
+    Evd.define evk body evd'
   with
     | NotEnoughInformationToProgress sols ->
         postpone_non_unique_projection env evd ev sols rhs
@@ -1391,6 +1389,6 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
         UnifFailure (evd,OccurCheck (evk1,rhs))
     | MetaOccurInBodyInternal ->
         UnifFailure (evd,MetaOccurInBody evk1)
-    | InstanceNotSameTypeInternal ->
-        UnifFailure (evd,InstanceNotSameType evk1)
+    | IllTypedInstance (env,t,u) ->
+        UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
 
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index e34332c9b..3e769e02d 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -54,5 +54,8 @@ val is_unification_pattern : env * int -> evar_map -> constr -> constr list ->
 
 val solve_pattern_eqn : env -> constr list -> constr -> constr
 
-val check_evar_instance : evar_map -> existential_key -> constr -> conv_fun ->
-  evar_map
+exception IllTypedInstance of env * types * types
+
+(* May raise IllTypedInstance if types are not convertible *)
+val check_evar_instance :
+  evar_map -> existential_key -> constr -> conv_fun -> evar_map
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 91d24ec69..72cc6502a 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -22,7 +22,7 @@ type unification_error =
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency
 
 type pretype_error =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index ee7965131..69994531d 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -25,7 +25,7 @@ type unification_error =
   | NoCanonicalStructure
   | ConversionFailed of env * constr * constr
   | MetaOccurInBody of existential_key
-  | InstanceNotSameType of existential_key
+  | InstanceNotSameType of existential_key * env * types * types
   | UnifUnivInconsistency
 
 type pretype_error =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 61830603b..9680a0046 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -183,9 +183,12 @@ let explain_unification_error env sigma p1 p2 = function
     | MetaOccurInBody evk ->
         spc () ++ str "(instance for " ++ quote (pr_existential_key evk) ++
 	strbrk " refers to a metavariable - please report your example)"
-    | InstanceNotSameType evk ->
+    | InstanceNotSameType (evk,env,t,u) ->
         spc () ++ str "(unable to find a well-typed instantiation for " ++
-	quote (pr_existential_key evk) ++ str ")"
+	quote (pr_existential_key evk) ++ str ":" ++ spc () ++
+          str "cannot unify" ++
+          pr_lconstr_env env t ++ spc () ++ str "and" ++ spc () ++
+          pr_lconstr_env env u ++ str ")"
     | UnifUnivInconsistency ->
         spc () ++ str "(Universe inconsistency)"