Merge PR #19002: Phrasing and formatting of the unsatisfiable constra…

…ints error message

Reviewed-by: SkySkimmer
Co-authored-by: SkySkimmer <SkySkimmer@users.noreply.github.com>

engine/termops.ml

@@ -337,12 +337,12 @@ let pr_evar_constraints sigma pbs =
          naming/renaming. *)
       Namegen.make_all_name_different env sigma
     in
-    print_env_short env sigma ++ spc () ++ str "|-" ++ spc () ++
+    hov 2 (hov 2 (print_env_short env sigma) ++ spc () ++ str "|-" ++ spc () ++
       Internal.print_kconstr env sigma t1 ++ spc () ++
       str (match pbty with
             | Conversion.CONV -> "=="
             | Conversion.CUMUL -> "<=") ++
-      spc () ++ Internal.print_kconstr env sigma t2
+      spc () ++ Internal.print_kconstr env sigma t2)
   in
   prlist_with_sep fnl pr_evconstr pbs
 

test-suite/output/ClassMissingInstance.out

@@ -1,8 +1,6 @@
 File "./output/ClassMissingInstance.v", line 7, characters 0-28:
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
-
-?arg_2 : "Foo 1"
-
-?arg_20 : "Foo 2"
+Could not find an instance for the following existential variables:
+?arg_2 : Foo 1
 
+?arg_20 : Foo 2

test-suite/output/bug_13942.out

@@ -108,7 +108,6 @@ More precisely:
   i : Union (M A)
 File "./output/bug_13942.v", line 140, characters 2-20:
 The command has indeed failed with message:
-Unable to satisfy the following constraints:
 In environment:
 K : Type
 M : Type -> Type
@@ -119,14 +118,12 @@ ifalse : Choose false -> Union (M B)
 itrue : Choose true -> Union (M B)
 ib : Insert K B (M B)
 i : Choose false -> Union (M A)
+Could not find an instance for the following existential variables:
+?hi : Insert K ?A (M ?A)
 
-?hi : "Insert K ?A (M ?A)"
-
-?hu : "Union (M ?A)"
-
+?hu : Union (M ?A)
 File "./output/bug_13942.v", line 145, characters 16-18:
 The command has indeed failed with message:
-
 Could not find an instance for "Union (M B)" in
 environment:
 K : Type
@@ -143,7 +140,6 @@ fi fu : B
      : B
 File "./output/bug_13942.v", line 307, characters 20-31:
 The command has indeed failed with message:
-
 Could not find an instance for "Insert K K (M A)" in
 environment:
 K : Type

vernac/himsg.ml

@@ -682,7 +682,7 @@ let explain_typeclass_resolution env sigma evi k =
   match Typeclasses.class_of_constr env sigma (Evd.evar_concl evi) with
   | Some _ ->
     let env = Evd.evar_filtered_env env evi in
-      fnl () ++ str "Could not find an instance for " ++
+      str "Could not find an instance for " ++
       pr_leconstr_env env sigma (Evd.evar_concl evi) ++
       pr_trailing_ne_context_of env sigma
   | _ -> mt()
@@ -963,7 +963,7 @@ let explain_cannot_unify_occurrences env sigma nested ((cl2,pos2),t2) ((cl1,pos1
     pr_leconstr_env env sigma t1 ++ strbrk " at position " ++
     pr_position (cl1,pos1) ++ str "."
 
-let pr_constraints printenv env sigma evars cstrs =
+let pr_constraints printenv msg env sigma evars cstrs =
   let (ev, evi) = Evar.Map.choose evars in
     if Evar.Map.for_all (fun ev' evi' ->
       eq_named_context_val (Evd.evar_hyps evi) (Evd.evar_hyps evi')) evars
@@ -975,12 +975,13 @@ let pr_constraints printenv env sigma evars cstrs =
           pr_ne_context_of (str "In environment:") env' sigma
         else mt ()
       in
+      let env = Global.env () in
       let evs =
-        prlist
-        (fun (ev, evi) -> fnl () ++ pr_existential_key (Global.env ()) sigma ev ++
-            str " : " ++ pr_leconstr_env env' sigma (Evd.evar_concl evi) ++ fnl ()) l
+        prlist_with_sep (fun () -> fnl () ++ fnl ())
+        (fun (ev, evi) -> hov 2 (pr_existential_key env sigma ev ++
+            str " :" ++ spc () ++ Printer.pr_leconstr_env env' sigma (Evd.evar_concl evi))) l
       in
-      h (pe ++ evs ++ pr_evar_constraints sigma cstrs)
+      h (pe ++ str msg ++ fnl () ++ evs ++ pr_evar_constraints sigma cstrs)
     else
       let filter evk _ = Evar.Map.mem evk evars in
       pr_evar_map_filter ~with_univs:false filter env sigma
@@ -999,14 +1000,18 @@ let explain_unsatisfiable_constraints env sigma constr comp =
   in
   match constr with
   | None ->
-    str "Unable to satisfy the following constraints:" ++ fnl () ++
-    pr_constraints true env sigma undef constraints
+    if List.is_empty constraints then
+      let msg = "Could not find an instance for the following existential variables:" in
+      pr_constraints true msg env sigma undef constraints
+    else
+      let msg = "Unable to satisfy the following constraints:" in
+      pr_constraints true msg env sigma undef constraints
   | Some (ev, k) ->
     let cstr =
       let remaining = Evar.Map.remove ev undef in
       if not (Evar.Map.is_empty remaining) then
-        str "With the following constraints:" ++ fnl () ++
-          pr_constraints false env sigma remaining constraints
+        let msg = "With the following constraints:" in
+        pr_constraints false msg env sigma remaining constraints
       else mt ()
     in
     let info = Evar.Map.find ev undef in