From cfefed1cb20b6abe33c222df49d346867bafbc7f Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Apr 2018 15:43:38 +0200
Subject: Preparing ability to select "best" unification failure to report
 among two.

---
 pretyping/evarconv.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 7d480b8d48..13676b674c 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -227,13 +227,20 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
+let join_failures evd1 evd2 e1 e2 = (evd2,e2)
+
 let rec ise_try evd = function
     [] -> assert false
   | [f] -> f evd
   | f1::l ->
       match f1 evd with
       | Success _ as x -> x
-      | UnifFailure _ -> ise_try evd l
+      | UnifFailure (evd1,e1) ->
+          match ise_try evd l with
+          | Success _ as x -> x
+          | UnifFailure (evd2,e2) ->
+              let evd,e = join_failures evd1 evd2 e1 e2 in
+              UnifFailure (evd,e)
 
 let ise_and evd l =
   let rec ise_and i = function
-- 
cgit v1.2.3


From 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 26 Apr 2018 15:51:03 +0200
Subject: Unification failure: don't give preference to a "beyond capabilities"
 error.

This is actually a bit ad hoc at this stage in the sense that this is
specifically to prefer an informative first-order unification failure
over the currently always uninformative failure coming from
second-order unification.

When second-order unification shall be able to give more information,
one may consider alternative strategies, even maybe reporting not just
one but the list of failures in all (interesting) branches.
---
 pretyping/evarconv.ml                 | 5 ++++-
 test-suite/output/unifconstraints.out | 8 ++++++++
 test-suite/output/unifconstraints.v   | 6 ++++++
 3 files changed, 18 insertions(+), 1 deletion(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 13676b674c..e978adf761 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -227,7 +227,10 @@ let check_conv_record env sigma (t1,sk1) (t2,sk2) =
 (* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
-let join_failures evd1 evd2 e1 e2 = (evd2,e2)
+let join_failures evd1 evd2 e1 e2 =
+  match e1, e2 with
+  | _, CannotSolveConstraint (_,ProblemBeyondCapabilities) -> (evd1,e1)
+  | _ -> (evd2,e2)
 
 let rec ise_try evd = function
     [] -> assert false
diff --git a/test-suite/output/unifconstraints.out b/test-suite/output/unifconstraints.out
index ae84603622..2fadd747b7 100644
--- a/test-suite/output/unifconstraints.out
+++ b/test-suite/output/unifconstraints.out
@@ -63,3 +63,11 @@ unification constraint:
    True /\ True /\ True \/
    veeryyyyyyyyyyyyloooooooooooooonggidentifier =
    veeryyyyyyyyyyyyloooooooooooooonggidentifier
+The command has indeed failed with message:
+In environment
+P : nat -> Type
+x : nat
+h : P x
+Unable to unify "P x" with "?P x"
+(unable to find a well-typed instantiation for "?P": cannot ensure that
+"nat -> Type" is a subtype of "nat -> Prop").
diff --git a/test-suite/output/unifconstraints.v b/test-suite/output/unifconstraints.v
index b9413a4ac2..179dec3fb0 100644
--- a/test-suite/output/unifconstraints.v
+++ b/test-suite/output/unifconstraints.v
@@ -20,3 +20,9 @@ Goal forall n m : nat, True /\ True /\ True \/
   3:clear m.
   Show.
 Admitted.
+Unset Printing Existential Instances.
+
+(* Check non regression of error message (the example can eventually
+   improve though and succeed) *)
+
+Fail Check fun P (x:nat) (h:P x) => exist _ x (h : P x).
-- 
cgit v1.2.3