check candidates in miller_pfenning

Author: Tragicus

pretyping/evarconv.ml

@@ -737,13 +737,19 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
     UnifFailure (i, NotSameHead)
   in
   let miller_pfenning l2r fallback ev lF tM evd =
-    match is_unification_pattern_evar env evd ev lF tM with
-      | None -> fallback ()
-      | Some l1' -> (* Miller-Pfenning's patterns unification *)
-        let t2 = tM in
-        let t2 = solve_pattern_eqn env evd l1' t2 in
-          solve_simple_eqn (conv_fun evar_conv_x) flags env evd
-            (position_problem l2r pbty,ev,t2)
+    try
+      if lF = [] then Success (Evarsolve.solve_candidates (conv_fun evar_conv_x) flags env evd ev tM)
+      else raise NoCandidates
+    with NoCandidates ->
+      (match is_unification_pattern_evar env evd ev lF tM with
+        | None -> fallback ()
+        | Some l1' -> (* Miller-Pfenning's patterns unification *)
+          let t2 = tM in
+          let t2 = solve_pattern_eqn env evd l1' t2 in
+            solve_simple_eqn (conv_fun evar_conv_x) flags env evd
+              (position_problem l2r pbty,ev,t2))
+    | IncompatibleCandidates t ->
+        UnifFailure (evd,IncompatibleInstances (env,ev,t,tM))
   in
   let consume_stack l2r (termF,skF) (termO,skO) evd =
     let switch f a b = if l2r then f a b else f b a in

pretyping/evarsolve.mli

@@ -123,6 +123,11 @@ val refresh_universes :
   bool option (* direction: true for levels lower than the existing levels *) ->
   env -> evar_map -> types -> evar_map * types
 
+exception NoCandidates
+exception IncompatibleCandidates of constr
+
+val solve_candidates : unifier -> unify_flags -> env -> evar_map -> existential -> constr -> evar_map
+
 val solve_refl : ?can_drop:bool -> conversion_check -> unify_flags -> env ->  evar_map ->
   bool option -> Evar.t -> constr SList.t -> constr SList.t -> evar_map