aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--engine/evarutil.ml6
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/termops.ml8
-rw-r--r--intf/evar_kinds.ml4
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/evardefine.ml9
-rw-r--r--test-suite/output/Errors.out8
-rw-r--r--test-suite/output/Errors.v6
-rw-r--r--vernac/himsg.ml10
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 =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 18:24:02 +0000