aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evd.ml5
-rw-r--r--pretyping/pretype_errors.ml10
-rw-r--r--pretyping/pretype_errors.mli8
-rw-r--r--pretyping/reductionops.ml4
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/unification.ml9
-rw-r--r--tactics/inv.ml5
-rw-r--r--test-suite/bugs/closed/shouldsucceed/2135.v9
-rw-r--r--toplevel/himsg.ml13
9 files changed, 51 insertions, 14 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index ed18f5e97..cf788f36d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -694,10 +694,7 @@ let meta_reassign mv (v,pb) evd =
(* If the meta is defined then forget its name *)
let meta_name evd mv =
- try
- let (na,def) = clb_name (Metamap.find mv evd.metas) in
- if def then Anonymous else na
- with Not_found -> Anonymous
+ try fst (clb_name (Metamap.find mv evd.metas)) with Not_found -> Anonymous
let meta_with_name evd id =
let na = Name id in
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 5b829e5bf..e92ab3206 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -32,6 +32,8 @@ type pretype_error =
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
| CannotFindWellTypedAbstraction of constr * constr list
+ | AbstractionOverMeta of name * name
+ | NonLinearUnification of name * constr
(* Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
@@ -174,6 +176,14 @@ let error_cannot_coerce env sigma (m,n) =
let error_cannot_find_well_typed_abstraction env sigma p l =
raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+let error_abstraction_over_meta env sigma hdmeta metaarg =
+ let m = Evd.meta_name sigma hdmeta and n = Evd.meta_name sigma metaarg in
+ raise (PretypeError (env_ise sigma env,AbstractionOverMeta (m,n)))
+
+let error_non_linear_unification env sigma hdmeta t =
+ let m = Evd.meta_name sigma hdmeta in
+ raise (PretypeError (env_ise sigma env,NonLinearUnification (m,t)))
+
(*s Ml Case errors *)
let error_cant_find_case_type_loc loc env sigma expr =
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e6e01fc44..f55e70bef 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -31,6 +31,8 @@ type pretype_error =
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
| CannotFindWellTypedAbstraction of constr * constr list
+ | AbstractionOverMeta of name * name
+ | NonLinearUnification of name * constr
(** Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
@@ -101,6 +103,12 @@ val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -
val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
constr -> constr list -> 'b
+val error_abstraction_over_meta : env -> Evd.evar_map ->
+ metavariable -> metavariable -> 'b
+
+val error_non_linear_unification : env -> Evd.evar_map ->
+ metavariable -> constr -> 'b
+
(** {6 Ml Case errors } *)
val error_cant_find_case_type_loc :
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index dae668243..bb0ce44ea 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -635,8 +635,8 @@ let is_trans_fconv = function | CONV -> is_trans_conv | CUMUL -> is_trans_conv_l
(* Special-Purpose Reduction *)
(********************************************************************)
-let whd_meta metasubst c = match kind_of_term c with
- | Meta p -> (try List.assoc p metasubst with Not_found -> c)
+let whd_meta sigma c = match kind_of_term c with
+ | Meta p -> (try meta_value sigma p with Not_found -> c)
| _ -> c
(* Try to replace all metas. Does not replace metas in the metas' values
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index f3bfa1e5f..4518c693d 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -206,7 +206,7 @@ val is_trans_fconv : conv_pb -> transparent_state -> env -> evar_map -> constr
(** {6 Special-Purpose Reduction Functions } *)
-val whd_meta : (metavariable * constr) list -> constr -> constr
+val whd_meta : evar_map -> constr -> constr
val plain_instance : (metavariable * constr) list -> constr -> constr
val instance :evar_map -> (metavariable * constr) list -> constr -> constr
val head_unfold_under_prod : transparent_state -> reduction_function
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b1b925f78..01109d8af 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -880,12 +880,13 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
else
res
-let w_unify_to_subterm_list env flags allow_K oplist t evd =
+let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
List.fold_right
(fun op (evd,l) ->
+ let op = whd_meta evd op in
if isMeta op then
if allow_K then (evd,op::l)
- else error "Unify_to_subterm_list"
+ else error_abstraction_over_meta env evd hdmeta (destMeta op)
else if occur_meta_or_existential op then
let (evd',cl) =
try
@@ -895,7 +896,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
in
if not allow_K && (* ensure we found a different instance *)
List.exists (fun op -> eq_constr op cl) l
- then error "Unify_to_subterm_list"
+ then error_non_linear_unification env evd hdmeta cl
else (evd',cl::l)
else if allow_K or dependent op t then
(evd,op::l)
@@ -909,7 +910,7 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
(* Remove delta when looking for a subterm *)
let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
let (evd',cllist) =
- w_unify_to_subterm_list env flags allow_K oplist typ evd in
+ w_unify_to_subterm_list env flags allow_K p oplist typ evd in
let typp = Typing.meta_type evd' p in
let pred = abstract_list_all env evd' typp typ cllist in
w_merge env false flags (evd',[p,pred,(ConvUpToEta 0,TypeProcessed)],[])
diff --git a/tactics/inv.ml b/tactics/inv.ml
index e732a31c4..140ddf8f4 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -45,8 +45,9 @@ let collect_meta_variables c =
let check_no_metas clenv ccl =
if occur_meta ccl then
- let metas = List.filter (fun na -> na<>Anonymous)
- (List.map (Evd.meta_name clenv.evd) (collect_meta_variables ccl)) in
+ let metas = List.filter (fun m -> not (Evd.meta_defined clenv.evd m))
+ (collect_meta_variables ccl) in
+ let metas = List.map (Evd.meta_name clenv.evd) metas in
errorlabstrm "inversion"
(str ("Cannot find an instantiation for variable"^
(if List.length metas = 1 then " " else "s ")) ++
diff --git a/test-suite/bugs/closed/shouldsucceed/2135.v b/test-suite/bugs/closed/shouldsucceed/2135.v
new file mode 100644
index 000000000..61882176a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2135.v
@@ -0,0 +1,9 @@
+(* Check that metas are whd-normalized before trying 2nd-order unification *)
+Lemma test :
+ forall (D:Type) (T : forall C, option C) (Q:forall D, option D -> Prop),
+ (forall (A : Type) (P : forall B:Type, option B -> Prop), P A (T A))
+ -> Q D (T D).
+Proof.
+ intros D T Q H.
+ pattern (T D). apply H.
+Qed.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index bccde6cbd..e01686750 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -436,6 +436,16 @@ let explain_cannot_find_well_typed_abstraction env p l =
str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
str "which is ill-typed."
+let explain_abstraction_over_meta _ m n =
+ strbrk "Too complex unification problem: cannot find a solution for both " ++
+ pr_name m ++ spc () ++ str "and " ++ pr_name n ++ str "."
+
+let explain_non_linear_unification env m t =
+ strbrk "Cannot unambiguously instantiate " ++
+ pr_name m ++ str ":" ++
+ strbrk " which would require to abstract twice on " ++
+ pr_lconstr_env env t ++ str "."
+
let explain_type_error env err =
let env = make_all_name_different env in
match err with
@@ -489,7 +499,8 @@ let explain_pretype_error env err =
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
| CannotFindWellTypedAbstraction (p,l) ->
explain_cannot_find_well_typed_abstraction env p l
-
+ | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n
+ | NonLinearUnification (m,c) -> explain_non_linear_unification env m c
(* Typeclass errors *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 10:13:38 +0000