Merge PR #7062: Slightly refining some error messages about unresolvable evars.

9 files changed, 42 insertions, 13 deletions

diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 9cf81ecce..45760c6b4 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -807,11 +807,11 @@ let judge_of_new_Type evd =
   let (evd', s) = new_univ_variable univ_rigid evd in
   (evd', { uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) })
 
-let subterm_source evk (loc,k) =
+let subterm_source evk ?where (loc,k) =
   let evk = match k with
-    | Evar_kinds.SubEvar (evk) -> evk
+    | Evar_kinds.SubEvar (None,evk) when where = None -> evk
     | _ -> evk in
-  (loc,Evar_kinds.SubEvar evk)
+  (loc,Evar_kinds.SubEvar (where,evk))
 
 (* Add equality constraints for covariant/invariant positions. For
    irrelevant positions, unify universes when flexible. *)
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index e289ca169..972b0b9e1 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -254,7 +254,7 @@ val evd_comb0 : (evar_map -> evar_map * 'a) -> evar_map ref -> 'a
 val evd_comb1 : (evar_map -> 'b -> evar_map * 'a) -> evar_map ref -> 'b -> 'a
 val evd_comb2 : (evar_map -> 'b -> 'c -> evar_map * 'a) -> evar_map ref -> 'b -> 'c -> 'a
 
-val subterm_source : Evar.t -> Evar_kinds.t Loc.located ->
+val subterm_source : Evar.t -> ?where:Evar_kinds.subevar_kind -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
 val meta_counter_summary_tag : int Summary.Dyn.tag
diff --git a/engine/termops.ml b/engine/termops.ml
index 3dfb0c34f..b7531f6fc 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -206,8 +206,12 @@ let pr_evar_source = function
   | Evar_kinds.ImpossibleCase -> str "type of impossible pattern-matching clause"
   | Evar_kinds.MatchingVar _ -> str "matching variable"
   | Evar_kinds.VarInstance id -> str "instance of " ++ Id.print id
-  | Evar_kinds.SubEvar evk ->
-    str "subterm of " ++ Evar.print evk
+  | Evar_kinds.SubEvar (where,evk) ->
+     (match where with
+     | None -> str "subterm of "
+     | Some Evar_kinds.Body -> str "body of "
+     | Some Evar_kinds.Domain -> str "domain of "
+     | Some Evar_kinds.Codomain -> str "codomain of ") ++ Evar.print evk
 
 let pr_evar_info evi =
   let open Evd in
diff --git a/intf/evar_kinds.ml b/intf/evar_kinds.ml
index c5de383b2..c964ecf1f 100644
--- a/intf/evar_kinds.ml
+++ b/intf/evar_kinds.ml
@@ -21,6 +21,8 @@ type obligation_definition_status = Define of bool | Expand
 
 type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
 
+type subevar_kind = Domain | Codomain | Body
+
 type t =
   | ImplicitArg of global_reference * (int * Id.t option)
      * bool (** Force inference *)
@@ -34,4 +36,4 @@ type t =
   | ImpossibleCase
   | MatchingVar of matching_var_kind
   | VarInstance of Id.t
-  | SubEvar of Evar.t
+  | SubEvar of subevar_kind option * Evar.t
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a5b7a9e6f..73be9d6b7 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1662,7 +1662,7 @@ let rec list_assoc_in_triple x = function
 let abstract_tycon ?loc env evdref subst tycon extenv t =
   let t = nf_betaiota env !evdref t in (* it helps in some cases to remove K-redex*)
   let src = match EConstr.kind !evdref t with
-    | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar evk)
+    | Evar (evk,_) -> (Loc.tag ?loc @@ Evar_kinds.SubEvar (None,evk))
     | _ -> (Loc.tag ?loc @@ Evar_kinds.CasesType true) in
   let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv !evdref subst t in
   (* We traverse the type T of the original problem Xi looking for subterms
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
index 03f40ad92..4cffbbb83 100644
--- a/pretyping/evardefine.ml
+++ b/pretyping/evardefine.ml
@@ -19,6 +19,7 @@ open Vars
 open Namegen
 open Evd
 open Evarutil
+open Evar_kinds
 open Pretype_errors
 
 module RelDecl = Context.Rel.Declaration
@@ -78,12 +79,14 @@ let define_pure_evar_as_product evd evk =
   let id = next_ident_away idx (Environ.ids_of_named_context_val evi.evar_hyps) in
   let concl = Reductionops.whd_all evenv evd (EConstr.of_constr evi.evar_concl) in
   let s = destSort evd concl in
+  let evksrc = evar_source evk evd in
+  let src = subterm_source evk ~where:Domain evksrc in
   let evd1,(dom,u1) =
-    new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi)
+    new_type_evar evenv evd univ_flexible_alg ~src ~filter:(evar_filter evi)
   in
   let evd2,rng =
     let newenv = push_named (LocalAssum (id, dom)) evenv in
-    let src = evar_source evk evd1 in
+    let src = subterm_source evk ~where:Codomain evksrc in
     let filter = Filter.extend 1 (evar_filter evi) in
       if Sorts.is_prop (ESorts.kind evd1 s) then
        (* Impredicative product, conclusion must fall in [Prop]. *)
@@ -135,7 +138,7 @@ let define_pure_evar_as_lambda env evd evk =
     next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
   let newenv = push_named (LocalAssum (id, dom)) evenv in
   let filter = Filter.extend 1 (evar_filter evi) in
-  let src = evar_source evk evd1 in
+  let src = subterm_source evk ~where:Body (evar_source evk evd1) in
   let evd2,body = new_evar newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
   let lam = mkLambda (Name id, dom, subst_var id body) in
   Evd.define evk (EConstr.Unsafe.to_constr lam) evd2, lam
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index 38d055b28..24180c455 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -8,3 +8,11 @@ Unable to unify "nat" with "True".
 The command has indeed failed with message:
 Ltac call to "instantiate ( (ident) := (lglob) )" failed.
 Instance is not well-typed in the environment of ?x.
+The command has indeed failed with message:
+Cannot infer the domain of the type of f.
+The command has indeed failed with message:
+Cannot infer the domain of the implicit parameter A of id whose type is
+"Type".
+The command has indeed failed with message:
+Cannot infer the codomain of the type of f in environment:
+x : nat
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 424d24801..c9b509134 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -25,3 +25,9 @@ eexists ?[x].
 destruct H1 as [x1 H1].
 Fail instantiate (x:=projT1 x1).
 Abort.
+
+(* Test some messages for non solvable evars *)
+
+Fail Goal forall a f, f a = 0.
+Fail Goal forall f x, id f x = 0.
+Fail Goal forall f P,  P (f 0).
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index 249e7893c..698ee4703 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -559,15 +559,21 @@ let rec explain_evar_kind env sigma evk ty = function
   | Evar_kinds.VarInstance id ->
       strbrk "an instance of type " ++ ty ++
       str " for the variable " ++ Id.print id
-  | Evar_kinds.SubEvar evk' ->
+  | Evar_kinds.SubEvar (where,evk') ->
       let evi = Evd.find sigma evk' in
       let pc = match evi.evar_body with
       | Evar_defined c -> pr_leconstr_env env sigma (EConstr.of_constr c)
       | Evar_empty -> assert false in
       let ty' = EConstr.of_constr evi.evar_concl in
+      (match where with
+      | Some Evar_kinds.Body -> str "the body of "
+      | Some Evar_kinds.Domain -> str "the domain of "
+      | Some Evar_kinds.Codomain -> str "the codomain of "
+      | None ->
       pr_existential_key sigma evk ++ str " of type " ++ ty ++
       str " in the partial instance " ++ pc ++
-      str " found for " ++ explain_evar_kind env sigma evk'
+      str " found for ") ++
+      explain_evar_kind env sigma evk'
       (pr_leconstr_env env sigma ty') (snd evi.evar_source)
 
 let explain_typeclass_resolution env sigma evi k =