Fixing a regression in unification introduced in r16205 (error raised

by solve_candidates was not anymore handled at the expected time).

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

2 files changed, 40 insertions, 2 deletions

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 1d5dda69f7..52088af389 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1082,8 +1082,9 @@ let solve_refl ?(can_drop=false) conv_algo env evd evk argsv1 argsv2 =
    in advance, we check which of them apply *)
 
 exception NoCandidates
+exception IncompatibleCandidates
 
-let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
+let solve_candidates conv_algo env evd (evk,argsv) rhs =
   let evi = Evd.find evd evk in
   let args = Array.to_list argsv in
   match evi.evar_candidates with
@@ -1093,7 +1094,7 @@ let solve_candidates conv_algo env evd (evk,argsv as ev) rhs =
         List.map_filter
           (filter_compatible_candidates conv_algo env evd evi args rhs) l in
       match l' with
-      | [] -> error_cannot_unify env evd (mkEvar ev, rhs)
+      | [] -> raise IncompatibleCandidates
       | [c,evd] ->
           (* solve_candidates might have been called recursively in the mean *)
           (* time and the evar been solved by the filtering process *)
@@ -1393,4 +1394,6 @@ let solve_simple_eqn conv_algo ?(choose=false) env evd (pbty,(evk1,args1 as ev1)
         UnifFailure (evd,MetaOccurInBody evk1)
     | IllTypedInstance (env,t,u) ->
         UnifFailure (evd,InstanceNotSameType (evk1,env,t,u))
+    | IncompatibleCandidates ->
+        UnifFailure (evd,ConversionFailed (env,mkEvar ev1,t2))
 
diff --git a/test-suite/success/Case20.v b/test-suite/success/Case20.v
new file mode 100644
index 0000000000..67eebf7238
--- /dev/null
+++ b/test-suite/success/Case20.v
@@ -0,0 +1,35 @@
+(* Example taken from RelationAlgebra *)
+(* Was failing from r16205 up to now *)
+
+Require Import BinNums.
+
+Section A.
+
+Context (A:Type) {X: A} (tst:A->Type) (top:forall X, X).
+
+Inductive v: (positive -> A) -> Type :=
+| v_L: forall f', v f'
+| v_N: forall f', 
+  v (fun n => f' (xO n)) -> 
+  (positive -> tst (f' xH)) -> 
+  v (fun n => f' (xI n)) -> v f'.
+
+Fixpoint v_add f' (t: v f') n: (positive -> tst (f' n)) -> v f' :=
+  match t in (v o) return ((positive -> (tst (o n))) -> v o) with
+    | v_L f' => 
+        match n return ((positive ->  (tst (f' n))) -> v f') with
+        | xH => fun x => v_N _ (v_L _) x (v_L _)
+        | xO n => fun x => v_N _ 
+          (v_add (fun n => f' (xO n)) (v_L _) n x) (fun _ => top _) (v_L _)
+        | xI n => fun x => v_N _ 
+          (v_L _) (fun _ => top _) (v_add (fun n => f' (xI n)) (v_L _) n x)
+        end
+    | v_N f' l y r => 
+        match n with
+        | xH => fun x => v_N _ l x r
+        | xO n => fun x => v_N _ (v_add (fun n => f' (xO n)) l n x) y r
+        | xI n => fun x => v_N _ l y (v_add (fun n => f' (xI n)) r n x)
+        end
+    end.
+
+End A.