From 34cb1f6491017e4ed1a509f6b83b88a812ac425f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 9 Dec 2014 12:09:44 +0100 Subject: Tentatively more informative report of failure when inferring pattern-matching predicate. --- interp/constrintern.ml | 2 +- intf/evar_kinds.mli | 4 ++-- pretyping/cases.ml | 18 ++++++++--------- pretyping/evarsolve.ml | 2 +- pretyping/evarutil.ml | 10 ++++++--- pretyping/evarutil.mli | 3 +++ pretyping/evd.ml | 7 +++++-- pretyping/pretype_errors.ml | 7 +++---- pretyping/pretype_errors.mli | 5 ++--- pretyping/pretyping.ml | 3 +-- tactics/tacticals.ml | 9 ++++----- toplevel/himsg.ml | 48 ++++++++++++++++++++++++++++---------------- toplevel/obligations.ml | 3 +-- 13 files changed, 70 insertions(+), 51 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index a0654220e..0fbd3cff9 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1514,7 +1514,7 @@ let internalize globalenv env allow_patvar lvar c = GCases(Loc.ghost,Term.RegularStyle,(* Some (GSort (Loc.ghost,GType None)) *)None, (* "return Type" *) List.map (fun id -> GVar (Loc.ghost,id),(Name id,None)) thevars, (* "match v1,..,vn" *) [Loc.ghost,[],thepats, (* "|p1,..,pn" *) - Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) + Option.cata (intern_type env') (GHole(Loc.ghost,Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None)) rtnpo; (* "=> P" is there were a P "=> _" else *) Loc.ghost,[],List.make (List.length thepats) (PatVar(Loc.ghost,Anonymous)), (* "|_,..,_" *) GHole(Loc.ghost,Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None) (* "=> _" *)])) in diff --git a/intf/evar_kinds.mli b/intf/evar_kinds.mli index f77fc5a6a..aae6e95aa 100644 --- a/intf/evar_kinds.mli +++ b/intf/evar_kinds.mli @@ -21,11 +21,11 @@ type t = * bool (** Force inference *) | BinderType of Name.t | QuestionMark of obligation_definition_status - | CasesType + | CasesType of bool (* true = a subterm of the type *) | InternalHole | TomatchTypeParameter of inductive * int | GoalEvar | ImpossibleCase | MatchingVar of bool * Id.t | VarInstance of Id.t - | SubEvar of t + | SubEvar of Constr.existential_key diff --git a/pretyping/cases.ml b/pretyping/cases.ml index eeb367a43..cd3c6276a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1586,8 +1586,11 @@ let rec list_assoc_in_triple x = function * similarly for each ti. *) -let abstract_tycon loc env evdref subst _tycon extenv t = - let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex *) +let abstract_tycon loc env evdref subst tycon extenv t = + let t = nf_betaiota !evdref t in (* it helps in some cases to remove K-redex*) + let src = match kind_of_term t with + | Evar (evk,_) -> (loc,Evar_kinds.SubEvar evk) + | _ -> (loc,Evar_kinds.CasesType true) in let subst0,t0 = adjust_to_extended_env_and_remove_deps env extenv subst t in (* We traverse the type T of the original problem Xi looking for subterms that match the non-constructor part of the constraints (this part @@ -1596,8 +1599,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = convertible subterms of the substitution *) let rec aux (k,env,subst as x) t = let t = whd_evar !evdref t in match kind_of_term t with - | Rel n when pi2 (lookup_rel n env) != None -> - map_constr_with_full_binders push_binder aux x t + | Rel n when pi2 (lookup_rel n env) != None -> t | Evar ev -> let ty = get_type_of env !evdref t in let ty = Evarutil.evd_comb1 (refresh_universes (Some false) env) evdref ty in @@ -1606,7 +1608,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev' = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in + let ev' = e_new_evar env evdref ~src ty in begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with | Success evd -> evdref := evd | UnifFailure _ -> assert false @@ -1637,9 +1639,7 @@ let abstract_tycon loc env evdref subst _tycon extenv t = (named_context extenv) in let filter = Filter.make (rel_filter @ named_filter) in let candidates = u :: List.map mkRel vl in - let ev = - e_new_evar extenv evdref ~src:(loc, Evar_kinds.CasesType) - ~filter ~candidates ty in + let ev = e_new_evar extenv evdref ~src ~filter ~candidates ty in lift k ev in aux (0,extenv,subst0) t0 @@ -1913,7 +1913,7 @@ let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred = | Some t -> sigma,t | None -> let sigma, (t, _) = - new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType) in + new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in sigma, t in (* First strategy: we build an "inversion" predicate *) diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index cb5673c2e..0e1ecda5c 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -552,7 +552,7 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env = let env1,rel_sign = env_rel_context_chop k env in let sign1 = evar_hyps evi1 in let filter1 = evar_filter evi1 in - let src = let (loc,k) = evi1.evar_source in (loc,Evar_kinds.SubEvar k) in + let src = subterm_source evk1 evi1.evar_source in let ids1 = List.map pi1 (named_context_of_val sign1) in let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) = diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 0fcff3d49..19a325df9 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -650,9 +650,7 @@ let check_evars env initial_sigma sigma c = let (loc,k) = evar_source evk sigma in match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () - | _ -> - let evi = nf_evar_info sigma (Evd.find_undefined sigma evk) in - error_unsolvable_implicit loc env sigma evi k None) + | _ -> error_unsolvable_implicit loc env sigma evk None) | _ -> iter_constr proc_rec c in proc_rec c @@ -834,3 +832,9 @@ let lift_tycon n = Option.map (lift n) let pr_tycon env = function None -> str "None" | Some t -> Termops.print_constr_env env t + +let subterm_source evk (loc,k) = + let evk = match k with + | Evar_kinds.SubEvar (evk) -> evk + | _ -> evk in + (loc,Evar_kinds.SubEvar evk) diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 8e8bbf367..abb895e62 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -233,3 +233,6 @@ val generalize_evar_over_rels : evar_map -> existential -> types * constr list 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 : existential_key -> Evar_kinds.t Loc.located -> + Evar_kinds.t Loc.located diff --git a/pretyping/evd.ml b/pretyping/evd.ml index c9435b54c..0fe16f0ed 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -1601,7 +1601,9 @@ let pr_decl ((id,b,_),ok) = let rec pr_evar_source = function | Evar_kinds.QuestionMark _ -> str "underscore" - | Evar_kinds.CasesType -> str "pattern-matching return predicate" + | Evar_kinds.CasesType false -> str "pattern-matching return predicate" + | Evar_kinds.CasesType true -> + str "subterm of pattern-matching return predicate" | Evar_kinds.BinderType (Name id) -> str "type of " ++ Nameops.pr_id id | Evar_kinds.BinderType Anonymous -> str "type of anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> @@ -1615,7 +1617,8 @@ let rec 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 " ++ pr_id id - | Evar_kinds.SubEvar k -> str "subterm of " ++ pr_evar_source k + | Evar_kinds.SubEvar evk -> + str "subterm of " ++ str (string_of_existential evk) let pr_evar_info evi = let phyps = diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 99b5a51f9..9b5b79284 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -36,8 +36,7 @@ type pretype_error = | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (* Tactic unification *) | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t * - Evd.unsolvability_explanation option + | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -107,9 +106,9 @@ let error_not_a_type_loc loc env sigma j = let error_occur_check env sigma ev c = raise (PretypeError (env, sigma, UnifOccurCheck (ev,c))) -let error_unsolvable_implicit loc env sigma evi e explain = +let error_unsolvable_implicit loc env sigma evk explain = Loc.raise loc - (PretypeError (env, sigma, UnsolvableImplicit (evi, e, explain))) + (PretypeError (env, sigma, UnsolvableImplicit (evk, explain))) let error_cannot_unify_loc loc env sigma ?reason (m,n) = Loc.raise loc (PretypeError (env, sigma,CannotUnify (m,n,reason))) diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 5882d8b9c..122240621 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -37,8 +37,7 @@ type pretype_error = | ActualTypeNotCoercible of unsafe_judgment * types * unification_error (** Tactic Unification *) | UnifOccurCheck of existential_key * constr - | UnsolvableImplicit of Evd.evar_info * Evar_kinds.t * - Evd.unsolvability_explanation option + | UnsolvableImplicit of existential_key * Evd.unsolvability_explanation option | CannotUnify of constr * constr * unification_error option | CannotUnifyLocal of constr * constr * constr | CannotUnifyBindingType of constr * constr @@ -100,7 +99,7 @@ val error_cannot_coerce : env -> Evd.evar_map -> constr * constr -> 'b val error_occur_check : env -> Evd.evar_map -> existential_key -> constr -> 'b val error_unsolvable_implicit : - Loc.t -> env -> Evd.evar_map -> Evd.evar_info -> Evar_kinds.t -> + Loc.t -> env -> Evd.evar_map -> existential_key -> Evd.unsolvability_explanation option -> 'b val error_cannot_unify_loc : Loc.t -> env -> Evd.evar_map -> diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f5aea567f..dfe018c33 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -190,8 +190,7 @@ let check_extra_evars_are_solved env current_sigma pending = match k with | Evar_kinds.ImplicitArg (gr, (i, id), false) -> () | _ -> - let evi = nf_evar_info current_sigma (Evd.find_undefined current_sigma evk) in - error_unsolvable_implicit loc env current_sigma evi k None) pending + error_unsolvable_implicit loc env current_sigma evk None) pending let check_evars_are_solved env current_sigma pending = check_typeclasses_instances_are_solved env current_sigma pending; diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 9256e10d6..bb7a3f2e3 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -477,17 +477,16 @@ module New = struct Evd.fold_undefined (fun evk evi acc -> if is_undefined_up_to_restriction sigma evk && not (Evd.mem origsigma evk) then - evi::acc + (evk,evi)::acc else acc) extsigma [] in match rest with | [] -> () - | evi :: _ -> - let (loc,k) = evi.Evd.evar_source in - let evi = Evarutil.nf_evar_info sigma evi in - Pretype_errors.error_unsolvable_implicit loc env sigma evi k None + | (evk,evi) :: _ -> + let (loc,_) = evi.Evd.evar_source in + Pretype_errors.error_unsolvable_implicit loc env sigma evk None let tclWITHHOLES accept_unresolved_holes tac sigma x = tclEVARMAP >>= fun sigma_initial -> diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 3c52a6a31..d16029400 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -501,34 +501,47 @@ let pr_trailing_ne_context_of env sigma = then str "." else (str " in environment:"++ fnl () ++ pr_context_unlimited env sigma) -let rec explain_evar_kind env = function - | Evar_kinds.QuestionMark _ -> strbrk "this placeholder" - | Evar_kinds.CasesType -> +let rec explain_evar_kind env sigma evk ty = function + | Evar_kinds.QuestionMark _ -> + strbrk "this placeholder of type " ++ ty + | Evar_kinds.CasesType false -> strbrk "the type of this pattern-matching problem" + | Evar_kinds.CasesType true -> + strbrk "a subterm of type " ++ ty ++ + strbrk " in the type of this pattern-matching problem" | Evar_kinds.BinderType (Name id) -> strbrk "the type of " ++ Nameops.pr_id id | Evar_kinds.BinderType Anonymous -> strbrk "the type of this anonymous binder" | Evar_kinds.ImplicitArg (c,(n,ido),b) -> let id = Option.get ido in - strbrk "the implicit parameter " ++ - pr_id id ++ spc () ++ str "of" ++ - spc () ++ Nametab.pr_global_env Id.Set.empty c - | Evar_kinds.InternalHole -> strbrk "an internal placeholder" + strbrk "the implicit parameter " ++ pr_id id ++ spc () ++ str "of" ++ + spc () ++ Nametab.pr_global_env Id.Set.empty c ++ + strbrk " whose type is " ++ ty + | Evar_kinds.InternalHole -> strbrk "an internal placeholder of type " ++ ty | Evar_kinds.TomatchTypeParameter (tyi,n) -> strbrk "the " ++ pr_nth n ++ strbrk " argument of the inductive type (" ++ pr_inductive env tyi ++ strbrk ") of this term" | Evar_kinds.GoalEvar -> - strbrk "an existential variable" + strbrk "an existential variable of type " ++ ty | Evar_kinds.ImpossibleCase -> strbrk "the type of an impossible pattern-matching clause" | Evar_kinds.MatchingVar _ -> assert false | Evar_kinds.VarInstance id -> - strbrk "an instance for the variable " ++ pr_id id - | Evar_kinds.SubEvar c -> - strbrk "a subterm of " ++ explain_evar_kind env c + strbrk "an instance of type " ++ ty ++ + str " for the variable " ++ pr_id id + | Evar_kinds.SubEvar evk' -> + let evi = Evd.find sigma evk' in + let pc = match evi.evar_body with + | Evar_defined c -> pr_lconstr_env env sigma (Evarutil.nf_evar sigma c) + | Evar_empty -> assert false in + let ty' = Evarutil.nf_evar sigma evi.evar_concl in + pr_existential_key sigma evk ++ str " of type " ++ ty ++ + str " in the partial instance " ++ pc ++ + str " found for " ++ explain_evar_kind env sigma evk' + (pr_lconstr_env env sigma ty') (snd evi.evar_source) let explain_typeclass_resolution env sigma evi k = match Typeclasses.class_of_constr evi.evar_concl with @@ -542,18 +555,19 @@ let explain_typeclass_resolution env sigma evi k = let explain_placeholder_kind env sigma c e = match e with | Some (SeveralInstancesFound n) -> - strbrk " (several distinct possible instances found)" + strbrk " (several distinct possible type class instances found)" | None -> match Typeclasses.class_of_constr c with - | Some _ -> strbrk " (no instance found)" + | Some _ -> strbrk " (no type class instance found)" | _ -> mt () -let explain_unsolvable_implicit env sigma evi k explain = +let explain_unsolvable_implicit env sigma evk explain = + let evi = Evarutil.nf_evar_info sigma (Evd.find_undefined sigma evk) in let env = Evd.evar_filtered_env evi in let type_of_hole = pr_lconstr_env env sigma evi.evar_concl in let pe = pr_trailing_ne_context_of env sigma in - strbrk "Cannot infer " ++ explain_evar_kind env k ++ - strbrk " of type " ++ type_of_hole ++ + strbrk "Cannot infer " ++ + explain_evar_kind env sigma evk type_of_hole (snd evi.evar_source) ++ explain_placeholder_kind env sigma evi.evar_concl explain ++ pe let explain_var_not_found env id = @@ -757,7 +771,7 @@ let explain_pretype_error env sigma err = let j = {uj_val = c; uj_type = actty} in explain_actual_type env sigma j t (Some e) | UnifOccurCheck (ev,rhs) -> explain_occur_check env sigma ev rhs - | UnsolvableImplicit (evi,k,exp) -> explain_unsolvable_implicit env sigma evi k exp + | UnsolvableImplicit (evk,exp) -> explain_unsolvable_implicit env sigma evk exp | VarNotFound id -> explain_var_not_found env id | UnexpectedType (actual,expect) -> let env, actual, expect = contract2 env actual expect in diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index be5711820..d5073802d 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -39,8 +39,7 @@ let check_evars env evm = | Evar_kinds.QuestionMark _ | Evar_kinds.ImplicitArg (_,_,false) -> () | _ -> - Pretype_errors.error_unsolvable_implicit loc env - evm (Evarutil.nf_evar_info evm evi) k None) + Pretype_errors.error_unsolvable_implicit loc env evm key None) (Evd.undefined_map evm) type oblinfo = -- cgit v1.2.3