aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evd.mli2
-rw-r--r--pretyping/pretype_errors.ml4
-rw-r--r--pretyping/pretype_errors.mli4
-rw-r--r--pretyping/unification.ml44
-rw-r--r--test-suite/success/apply.v12
-rw-r--r--toplevel/himsg.ml16
6 files changed, 60 insertions, 22 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli
index 71c6bb0dc3..605f2fcd03 100644
--- a/pretyping/evd.mli
+++ b/pretyping/evd.mli
@@ -112,7 +112,7 @@ val metavars_of : constr -> Metaset.t
val mk_freelisted : constr -> constr freelisted
val map_fl : ('a -> 'b) -> 'a freelisted -> 'b freelisted
-(* Possible constraints over the instance of a metavariable:
+(* Status of an instance found by unification wrt to the meta it solves:
- a supertype of the meta (e.g. the solution to ?X <= T is a supertype of ?X)
- a subtype of the meta (e.g. the solution to T <= ?X is a supertype of ?X)
- a term that can be eta-expanded n times while still being a solution
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index cd32ac450a..06d1aa533b 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -32,6 +32,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
+ | CannotFindWellTypedAbstraction of constr * constr list
(* Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
@@ -166,6 +167,9 @@ let error_cannot_unify_local env sigma (m,n,sn) =
let error_cannot_coerce env sigma (m,n) =
raise (PretypeError (env_ise sigma env,CannotUnify (m,n)))
+let error_cannot_find_well_typed_abstraction env sigma p l =
+ raise (PretypeError (env_ise sigma env,CannotFindWellTypedAbstraction (p,l)))
+
(*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 c6527f337e..a276b4ed51 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -34,6 +34,7 @@ type pretype_error =
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
| NoOccurrenceFound of constr * identifier option
+ | CannotFindWellTypedAbstraction of constr * constr list
(* Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
@@ -101,6 +102,9 @@ val error_cannot_unify : env -> Evd.evar_map -> constr * constr -> 'b
val error_cannot_unify_local : env -> Evd.evar_map -> constr * constr * constr -> 'b
+val error_cannot_find_well_typed_abstraction : env -> Evd.evar_map ->
+ constr -> constr list -> 'b
+
(*s Ml Case errors *)
val error_cant_find_case_type_loc :
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 84f9330d3b..578afdb75c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -48,8 +48,8 @@ let abstract_list_all env evd typ c l =
try
if is_conv_leq env (evars_of evd) (Typing.mtype_of env evd p) typ then p
else error "abstract_list_all"
- with UserError _ ->
- raise (PretypeError (env,CannotGeneralize typ))
+ with UserError _ | Type_errors.TypeError _ ->
+ error_cannot_find_well_typed_abstraction env (evars_of evd) p l
(**)
@@ -142,7 +142,7 @@ let expand_constant env flags c =
| Var id when Idpred.mem id ids && Idpred.mem id (fst flags.modulo_delta) -> named_body id env
| _ -> None
-let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
+let unify_0_with_initial_metas subst conv_at_top env sigma cv_pb flags m n =
let nb = nb_rel env in
let trivial_unify pb (metasubst,_) m n =
match subst_defined_metas metasubst m with
@@ -243,11 +243,11 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
is_trans_fconv (conv_pb_of cv_pb) flags env sigma m n
| None -> eq_constr m n)
then
- (metas,[])
+ subst
else
- unirec_rec env cv_pb conv_at_top (metas,[]) m n
+ unirec_rec env cv_pb conv_at_top subst m n
-let unify_0 = unify_0_with_initial_metas [] true
+let unify_0 = unify_0_with_initial_metas ([],[]) true
let left = true
let right = false
@@ -451,7 +451,7 @@ let solve_simple_evar_eqn env evd ev rhs =
or in evars, possibly generating new unification problems; if [b]
is true, unification of types of metas is required *)
-let w_merge env with_types flags metas evars evd =
+let w_merge env with_types flags (metas,evars) evd =
let rec w_merge_rec evd metas evars eqns =
(* Process evars *)
@@ -528,7 +528,7 @@ let w_merge env with_types flags metas evars evd =
let w_unify_meta_types env ?(flags=default_unify_flags) evd =
let metas,evd = retract_coercible_metas evd in
- w_merge env true flags metas [] evd
+ w_merge env true flags (metas,[]) evd
(* [w_unify env evd M N]
performs a unification of M and N, generating a bunch of
@@ -540,12 +540,22 @@ let w_unify_meta_types env ?(flags=default_unify_flags) evd =
[clenv_typed_unify M N clenv] expects in addition that expected
types of metavars are unifiable with the types of their instances *)
+let check_types env evd subst m n =
+ if isEvar (fst (whd_stack m)) or isEvar (fst (whd_stack n)) then
+ unify_0_with_initial_metas subst true env (evars_of evd) topconv
+ default_unify_flags
+ (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) m)
+ (Retyping.get_type_of_with_meta env (evars_of evd) (metas_of evd) n)
+ else
+ subst
+
let w_unify_core_0 env with_types cv_pb flags m n evd =
let (mc1,evd') = retract_coercible_metas evd in
- let (mc2,ec) =
- unify_0_with_initial_metas mc1 true env (evars_of evd') cv_pb flags m n
+ let subst1 = check_types env evd (mc1,[]) m n in
+ let subst2 =
+ unify_0_with_initial_metas subst1 true env (evars_of evd') cv_pb flags m n
in
- w_merge env with_types flags mc2 ec evd'
+ w_merge env with_types flags subst2 evd'
let w_unify_0 env = w_unify_core_0 env false
let w_typed_unify env = w_unify_core_0 env true
@@ -653,7 +663,7 @@ let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
w_unify_to_subterm_list env flags allow_K oplist typ evd in
let typp = Typing.meta_type evd' p in
let pred = abstract_list_all env evd' typp typ cllist in
- w_unify_0 env topconv flags (mkMeta p) pred evd'
+ w_merge env false flags ([p,pred,(ConvUpToEta 0,TypeProcessed)],[]) evd'
let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
let c1, oplist1 = whd_stack ty1 in
@@ -673,7 +683,6 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
| _ -> error "w_unify2"
-
(* The unique unification algorithm works like this: If the pattern is
flexible, and the goal has a lambda-abstraction at the head, then
we do a first-order unification.
@@ -707,9 +716,7 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
with ex when precatchable_exception ex ->
try
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound _) as e -> raise e
- | ex when precatchable_exception ex ->
- error "Cannot solve a second-order unification problem")
+ with PretypeError (env,NoOccurrenceFound _) as e -> raise e)
(* Second order case *)
| (Meta _, true, _, _ | _, _, Meta _, true) ->
@@ -719,9 +726,8 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
| ex when precatchable_exception ex ->
try
w_typed_unify env cv_pb flags ty1 ty2 evd
- with ex when precatchable_exception ex ->
- error "Cannot solve a second-order unification problem")
+ with ex' when precatchable_exception ex' ->
+ raise ex)
(* General case: try first order *)
| _ -> w_typed_unify env cv_pb flags ty1 ty2 evd
-
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index 3b4e8af21f..e3fed09e7d 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -174,3 +174,15 @@ Axiom ax : forall (A : Set) (R : A -> A -> Prop) (x y : A), R x y.
Theorem t : r true false.
apply ax with (R := r).
Qed.
+
+
+(* Check verification of type at unification (Submitted by Stéphane Lengrand)
+ (without verification, the first "apply" works which leads to wrongly
+ instantiate x by Prop) *)
+
+Theorem t: ~(forall x:Prop, ~x).
+unfold not.
+intro.
+eapply H.
+apply (forall B:Prop,B->B) || (instantiate (1:=True); exact I).
+Defined.
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 4950f4064d..70450295be 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -403,7 +403,7 @@ let explain_cannot_unify_local env m n subn =
psubn ++ str " contains local variables"
let explain_refiner_cannot_generalize env ty =
- str "Cannot find a well-typed generalisation of the goal with type : " ++
+ str "Cannot find a well-typed generalisation of the goal with type: " ++
pr_lconstr_env env ty
let explain_no_occurrence_found env c id =
@@ -419,6 +419,16 @@ let explain_cannot_unify_binding_type env m n =
str "This binding has type" ++ brk(1,1) ++ pm ++ spc () ++
str "which should be unifiable with" ++ brk(1,1) ++ pn
+let explain_cannot_find_well_typed_abstraction env p l =
+ let la,lc = list_chop (List.length l - 1) l in
+ str "Abstracting over the " ++
+ str (plural (List.length l) "term") ++ spc () ++
+ hov 0 (prlist_with_sep pr_coma (pr_lconstr_env env) la ++
+ (if la<>[] then str " and" ++ spc () else mt()) ++
+ pr_lconstr_env env (List.hd lc)) ++ spc () ++
+ str "leads to a term" ++ spc () ++ pr_lconstr_env env p ++ spc () ++
+ str "which is ill-typed"
+
let explain_type_error env err =
let env = make_all_name_different env in
match err with
@@ -470,6 +480,8 @@ let explain_pretype_error env err =
| CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
| NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
+ | CannotFindWellTypedAbstraction (p,l) ->
+ explain_cannot_find_well_typed_abstraction env p l
(* Typeclass errors *)
@@ -716,7 +728,7 @@ let explain_cannot_infer_predicate env typs =
let env = make_all_name_different env in
let pr_branch (cstr,typ) =
let cstr,_ = decompose_app cstr in
- str "For " ++ pr_lconstr_env env cstr ++ str " : " ++ pr_lconstr_env env typ
+ str "For " ++ pr_lconstr_env env cstr ++ str ": " ++ pr_lconstr_env env typ
in
str "Unable to unify the types found in the branches:" ++
spc () ++ hov 0 (prlist_with_sep pr_fnl pr_branch (Array.to_list typs))
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 19:19:53 +0000