From 47c05b2531cb0de6da91968e2d17c68033ae7835 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 21 Aug 2020 20:53:45 +0200
Subject: Fixing a (known) "bugged" part of imitation in unification.

We ensure that when imitation stops to be possible, we postpone an
equation of the type of the subterm (and not of the arbitrary type of
an evar possibly depending on this subterm).
---
 pretyping/evarsolve.ml | 15 ++++-----------
 1 file changed, 4 insertions(+), 11 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 715b80f428..994ba9e0e7 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -935,13 +935,6 @@ let project_with_effects aliases sigma t subst =
   in
   filter_solution (Int.Map.fold is_projectable subst [])
 
-open Context.Named.Declaration
-let rec find_solution_type evarenv = function
-  | (id,ProjectVar)::l -> get_type (lookup_named id evarenv)
-  | [id,ProjectEvar _] -> (* bugged *) get_type (lookup_named id evarenv)
-  | (id,ProjectEvar _)::l -> find_solution_type evarenv l
-  | [] -> assert false
-
 (* In case the solution to a projection problem requires the instantiation of
  * subsidiary evars, [do_projection_effects] performs them; it
  * also try to instantiate the type of those subsidiary evars if their
@@ -1552,10 +1545,10 @@ let rec invert_definition unify flags choose imitate_defs
             raise (NotEnoughInformationToProgress sols);
           (* No unique projection but still restrict to where it is possible *)
           (* materializing is necessary, but is restricting useful? *)
-          let ty = find_solution_type (evar_filtered_env env evi) sols in
-          let ty' = instantiate_evar_array evi ty argsv in
+          let t' = of_alias t in
+          let ty = Retyping.get_type_of env !evdref t' in
           let (evd,evar,(evk',argsv' as ev')) =
-            materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
+            materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty in
           let ts = expansions_of_var evd aliases t in
           let test c = isEvar evd c || List.exists (is_alias evd c) ts in
           let filter = restrict_upon_filter evd evk test argsv' in
@@ -1564,7 +1557,7 @@ let rec invert_definition unify flags choose imitate_defs
           let evd = match candidates with
           | NoUpdate ->
             let evd, ev'' = restrict_applied_evar evd ev' filter NoUpdate in
-            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',of_alias t) evd
+            add_conv_oriented_pb ~tail:false (None,env,mkEvar ev'',t') evd
           | UpdateWith _ ->
             restrict_evar evd evk' filter candidates
           in
-- 
cgit v1.2.3


From a8b25255a5e918ed0d8dfcc8529dcd2ec27f721b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 21 Aug 2020 21:00:06 +0200
Subject: Checking type in unification imitation: avoid raising a non-located
 error.

---
 pretyping/evarsolve.ml | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 994ba9e0e7..5548f3205b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -227,8 +227,7 @@ let recheck_applications unify flags env evdref t =
             (match unify flags TypeUnification env !evdref Reduction.CUMUL argsty.(i) dom with
              | Success evd -> evdref := evd;
                              aux (succ i) (subst1 args.(i) codom)
-             | UnifFailure (evd, reason) ->
-                Pretype_errors.error_cannot_unify env evd ~reason (argsty.(i), dom))
+             | UnifFailure (evd, reason) -> raise (IllTypedInstance (env, ty, argsty.(i))))
          | _ -> raise (IllTypedInstance (env, ty, argsty.(i)))
        else ()
      in aux 0 fty
-- 
cgit v1.2.3


From 6f31beeaaaf99306d206964e1bd3e966b0475023 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 22 Aug 2020 00:43:28 +0200
Subject: Overlay for Coq-Equations.

---
 ...ster+minifix-unification-error-reporting-recheck-applications.sh | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh

diff --git a/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
new file mode 100644
index 0000000000..7680e8da78
--- /dev/null
+++ b/dev/ci/user-overlays/12873-master+minifix-unification-error-reporting-recheck-applications.sh
@@ -0,0 +1,6 @@
+if [ "$CI_PULL_REQUEST" = "12873" ] || [ "$CI_BRANCH" = "master+minifix-unification-error-reporting-recheck-applications" ]; then
+
+    equations_CI_REF=master+fix12873-better-unification
+    equations_CI_GITURL=https://github.com/herbelin/Coq-Equations
+
+fi
-- 
cgit v1.2.3