diff options
| -rw-r--r-- | pretyping/pretype_errors.ml | 4 | ||||
| -rw-r--r-- | pretyping/pretype_errors.mli | 4 | ||||
| -rw-r--r-- | pretyping/unification.ml | 17 | ||||
| -rw-r--r-- | pretyping/unification.mli | 2 | ||||
| -rw-r--r-- | tactics/inv.ml | 5 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 8 |
6 files changed, 31 insertions, 9 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d91273037..0cd5743cd 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -28,6 +28,7 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * identifier option | CannotFindWellTypedAbstraction of constr * constr list + | WrongAbstractionType of name * constr * types * types | AbstractionOverMeta of name * name | NonLinearUnification of name * constr (* Pretyping *) @@ -154,6 +155,9 @@ let error_cannot_coerce env sigma (m,n) = let error_cannot_find_well_typed_abstraction env sigma p l = raise (PretypeError (env, sigma,CannotFindWellTypedAbstraction (p,l))) +let error_wrong_abstraction_type env sigma na a p l = + raise (PretypeError (env, sigma,WrongAbstractionType (na,a,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, sigma,AbstractionOverMeta (m,n))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index ef4d2cc68..e2e66e80f 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -30,6 +30,7 @@ type pretype_error = | CannotGeneralize of constr | NoOccurrenceFound of constr * identifier option | CannotFindWellTypedAbstraction of constr * constr list + | WrongAbstractionType of name * constr * types * types | AbstractionOverMeta of name * name | NonLinearUnification of name * constr (** Pretyping *) @@ -106,6 +107,9 @@ 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_wrong_abstraction_type : env -> Evd.evar_map -> + name -> constr -> types -> types -> 'b + val error_abstraction_over_meta : env -> Evd.evar_map -> metavariable -> metavariable -> 'b diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 886c4a3aa..e25a880f8 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -60,15 +60,17 @@ let abstract_scheme env c l lname_typ = (List.rev l) lname_typ +(* Precondition: resulting abstraction is expected to be of type [typ] *) + let abstract_list_all env evd typ c l = let ctxt,_ = splay_prod_n env evd (List.length l) typ in let l_with_all_occs = List.map (function a -> (AllOccurrences,a)) l in let p = abstract_scheme env c l_with_all_occs ctxt in - try - if is_conv_leq env evd (Typing.type_of env evd p) typ then p - else error "abstract_list_all" - with UserError _ | Type_errors.TypeError _ -> - error_cannot_find_well_typed_abstraction env evd p l + let typp = + try Typing.type_of env evd p + with UserError _ | Type_errors.TypeError _ -> + error_cannot_find_well_typed_abstraction env evd p l in + (p,typp) let set_occurrences_of_last_arg args = Some AllOccurrences :: List.tl (Array.map_to_list (fun _ -> None) args) @@ -1176,7 +1178,10 @@ let secondOrderAbstraction env evd flags typ (p, oplist) = let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in let typp = Typing.meta_type evd' p in - let pred = abstract_list_all env evd' typp typ cllist in + let pred,predtyp = abstract_list_all env evd' typp typ cllist in + if not (is_conv_leq env evd predtyp typp) then + error_wrong_abstraction_type env evd + (Evd.meta_name evd p) pred typp predtyp; w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[]) let secondOrderDependentAbstraction env evd flags typ (p, oplist) = diff --git a/pretyping/unification.mli b/pretyping/unification.mli index e3fd46afe..df87283f9 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -58,7 +58,7 @@ val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> abstracts the terms in l over c to get a term of type t (exported for inv.ml) *) val abstract_list_all : - env -> evar_map -> constr -> constr -> constr list -> constr + env -> evar_map -> constr -> constr -> constr list -> constr * types (* For tracing *) diff --git a/tactics/inv.ml b/tactics/inv.ml index d598a97e6..81c630884 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -102,8 +102,9 @@ let make_inv_predicate env sigma indf realargs id status concl = | None -> let sort = get_sort_family_of env sigma concl in let p = make_arity env true indf (new_sort_in_family sort) in - Unification.abstract_list_all env (Evd.create_evar_defs sigma) - p concl (realargs@[mkVar id]) in + fst (Unification.abstract_list_all env + (Evd.create_evar_defs sigma) + p concl (realargs@[mkVar id])) in let hyps,bodypred = decompose_lam_n_assum (nrealargs+1) pred in (* We lift to make room for the equations *) (hyps,lift nrealargs bodypred) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 53c4325e1..141acb3db 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -453,6 +453,13 @@ 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_wrong_abstraction_type env na abs expected result = + let ppname = match na with Anonymous -> mt() | Name id -> pr_id id ++ spc() in + str "Cannot instantiate metavariable " ++ ppname ++ strbrk "of type " ++ + pr_lconstr_env env expected ++ strbrk " with abstraction " ++ + pr_lconstr_env env abs ++ strbrk " of incompatible type " ++ + pr_lconstr_env env result ++ str "." + 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 "." @@ -517,6 +524,7 @@ let explain_pretype_error env sigma err = | CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n | CannotFindWellTypedAbstraction (p,l) -> explain_cannot_find_well_typed_abstraction env p l + | WrongAbstractionType (n,a,t,u) -> explain_wrong_abstraction_type env n a t u | AbstractionOverMeta (m,n) -> explain_abstraction_over_meta env m n | NonLinearUnification (m,c) -> explain_non_linear_unification env m c | TypingError t -> explain_type_error env sigma t |