diff options
| author | Hugo Herbelin | 2018-04-26 15:51:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-09-27 14:21:10 +0200 |
| commit | 8ef1be1aead0dbcc2d3cc46a7e5eaa02f9ad6069 (patch) | |
| tree | 60e562a2662a8a499c359c2454a37425d217b1c7 | |
| parent | cfefed1cb20b6abe33c222df49d346867bafbc7f (diff) | |
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.
| -rw-r--r-- | pretyping/evarconv.ml | 5 | ||||
| -rw-r--r-- | test-suite/output/unifconstraints.out | 8 | ||||
| -rw-r--r-- | test-suite/output/unifconstraints.v | 6 |
3 files changed, 18 insertions, 1 deletions
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). |