Fix a bug in error printing of unif constraints

Conversion problems are in a de Bruijn environment that may
include references to unbound rels (because of the way evars
are created), we patch the env to named all de Bruijn variables
so that error printing does not raise an anomaly. Also fix a minor
printing bug in unsatisfiable constraints error reporting.

HoTT_coq_117.v tests all of this.

3 files changed, 21 insertions, 7 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d82d555f84..c538a137f2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1158,9 +1158,14 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
       (* Some head evar have been instantiated, or unknown kind of problem *)
       evar_conv_x ts env evd pbty t1 t2
 
+let error_cannot_unify env evd pb ?reason t1 t2 =
+  Pretype_errors.error_cannot_unify_loc
+    (loc_of_conv_pb evd pb) env
+    evd ?reason (t1, t2)
+
 let check_problems_are_solved env evd =
   match snd (extract_all_conv_pbs evd) with
-  | (pbty,env,t1,t2)::_ -> Pretype_errors.error_cannot_unify env evd (t1, t2)
+  | (pbty,env,t1,t2) as pb::_ -> error_cannot_unify env evd pb t1 t2
   | _ -> ()
 
 let max_undefined_with_candidates evd =
@@ -1229,17 +1234,15 @@ let consider_remaining_unif_problems env
 	      aux evd pbs progress (pb :: stuck)
             end
         | UnifFailure (evd,reason) ->
-	    Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
-              env evd ~reason (t1, t2))
+           error_cannot_unify env evd pb ~reason t1 t2)
     | _ -> 
 	if progress then aux evd stuck false []
 	else 
 	  match stuck with
 	  | [] -> (* We're finished *) evd
 	  | (pbty,env,t1,t2 as pb) :: _ ->
-	      (* There remains stuck problems *)
-	      Pretype_errors.error_cannot_unify_loc (loc_of_conv_pb evd pb)
-                env evd (t1, t2)
+	     (* There remains stuck problems *)
+             error_cannot_unify env evd pb t1 t2
   in
   let (evd,pbs) = extract_all_conv_pbs evd in
   let heuristic_solved_evd = aux evd pbs false [] in
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 0bc688aacf..2f4b8fc12f 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -840,6 +840,7 @@ let set_universe_context evd uctx' =
   { evd with universes = uctx' }
 
 let add_conv_pb ?(tail=false) pb d =
+  (** MS: we have duplicates here, why? *)
   if tail then {d with conv_pbs = d.conv_pbs @ [pb]}
   else {d with conv_pbs = pb::d.conv_pbs}
 
@@ -1888,6 +1889,16 @@ let print_env_short env =
 
 let pr_evar_constraints pbs =
   let pr_evconstr (pbty, env, t1, t2) =
+    let env =
+      (** We currently allow evar instances to refer to anonymous de
+          Bruijn indices, so we protect the error printing code in this
+          case by giving names to every de Bruijn variable in the
+          rel_context of the conversion problem. MS: we should rather
+          stop depending on anonymous variables, they can be used to
+          indicate independency. Also, this depends on a strategy for
+          naming/renaming. *)
+      Namegen.make_all_name_different env
+    in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
       print_constr_env env t1 ++ spc () ++
       str (match pbty with
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index ae6c86c8cc..fe9b6d4e19 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -741,7 +741,7 @@ let pr_constraints printenv env sigma evars cstrs =
       let evs =
         prlist
         (fun (ev, evi) -> fnl () ++ pr_existential_key sigma ev ++
-            str " : " ++ pr_lconstr_env env' sigma evi.evar_concl) l
+            str " : " ++ pr_lconstr_env env' sigma evi.evar_concl ++ fnl ()) l
       in
       h 0 (pe ++ evs ++ pr_evar_constraints cstrs)
     else