From 59e1618ccda6bbc9c627df93db7aaa3ea5930ccf Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 12 Jun 2016 15:56:06 +0200 Subject: Protecting eta-expansion in evarconv.ml against ill-typed problems. This can happen with the "with" clause (see e.g. #4782), but also with recursive calls in first-order unification (e.g. "?n a a b = f a" when a matching between "b" and "a" is tried before expanding f). --- pretyping/evarconv.ml | 36 +++++++++++++++++++++--------------- 1 file changed, 21 insertions(+), 15 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index cc202d73c5..a39e374447 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -462,10 +462,11 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let flex_rigid on_left ev (termF, skF as apprF) (termR, skR as apprR) = let switch f a b = if on_left then f a b else f b a in let eta evd = - match kind_of_term termR with - | Lambda _ -> eta env evd false skR termR skF termF - | Construct u -> eta_constructor ts env evd skR u skF termF - | _ -> UnifFailure (evd,NotSameHead) + match kind_of_term termR with + | Lambda _ when (* if ever problem is ill-typed: *) List.is_empty skR -> + eta env evd false skR termR skF termF + | Construct u -> eta_constructor ts env evd skR u skF termF + | _ -> UnifFailure (evd,NotSameHead) in match Stack.list_of_app_stack skF with | None -> @@ -741,10 +742,10 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ise_try evd [f3; f4] (* Eta-expansion *) - | Rigid, _ when isLambda term1 -> + | Rigid, _ when isLambda term1 && (* if ever ill-typed: *) List.is_empty sk1 -> eta env evd true sk1 term1 sk2 term2 - | _, Rigid when isLambda term2 -> + | _, Rigid when isLambda term2 && (* if ever ill-typed: *) List.is_empty sk2 -> eta env evd false sk2 term2 sk1 term1 | Rigid, Rigid -> begin @@ -1094,7 +1095,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs = abstract_free_holes evd subst, true with TypingFailed evd -> evd, false -let second_order_matching_with_args ts env evd ev l t = +let second_order_matching_with_args ts env evd pbty ev l t = (* let evd,ev = evar_absorb_arguments env evd ev l in let argoccs = Array.map_to_list (fun _ -> None) (snd ev) in @@ -1102,8 +1103,9 @@ let second_order_matching_with_args ts env evd ev l t = if b then Success evd else UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) if b then Success evd else -*) - UnifFailure (evd, ConversionFailed (env,mkApp(mkEvar ev,l),t)) + *) + let pb = (pbty,env,mkApp(mkEvar ev,l),t) in + UnifFailure (evd, CannotSolveConstraint (pb,ProblemBeyondCapabilities)) let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = let t1 = apprec_nohdbeta ts env evd (whd_head_evar evd t1) in @@ -1119,7 +1121,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk1 evd term2 args1 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | (Rel _|Var _), Evar (evk2,args2) when app_empty && List.for_all (fun a -> Term.eq_constr a term1 || isEvar a) (remove_instance_local_defs evd evk2 args2) -> @@ -1127,7 +1131,9 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = type inference *) (match choose_less_dependent_instance evk2 evd term1 args2 with | Some evd -> Success evd - | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))) + | None -> + let reason = ProblemBeyondCapabilities in + UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason))) | Evar (evk1,args1), Evar (evk2,args2) when Evar.equal evk1 evk2 -> let f env evd pbty x y = is_trans_fconv pbty ts env evd x y in Success (solve_refl ~can_drop:true f env evd @@ -1142,20 +1148,20 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 = ise_try evd [(fun evd -> first_order_unification ts env evd (ev1,l1) appr2); (fun evd -> - second_order_matching_with_args ts env evd ev1 l1 t2)] + second_order_matching_with_args ts env evd pbty ev1 l1 t2)] | _,Evar ev2 when Array.length l2 <= Array.length l1 -> (* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *) (* and otherwise second-order matching *) ise_try evd [(fun evd -> first_order_unification ts env evd (ev2,l2) appr1); (fun evd -> - second_order_matching_with_args ts env evd ev2 l2 t1)] + second_order_matching_with_args ts env evd pbty ev2 l2 t1)] | Evar ev1,_ -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev1 l1 t2 + second_order_matching_with_args ts env evd pbty ev1 l1 t2 | _,Evar ev2 -> (* Try second-order pattern-matching *) - second_order_matching_with_args ts env evd ev2 l2 t1 + second_order_matching_with_args ts env evd pbty ev2 l2 t1 | _ -> (* Some head evar have been instantiated, or unknown kind of problem *) evar_conv_x ts env evd pbty t1 t2 -- cgit v1.2.3 From 1f772656fa4bb6899ffea84ad5483e9690bbdc08 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 12 Jun 2016 16:00:23 +0200 Subject: Reserve exception "ConversionFailed" in unification for failure of conversion on closed terms. This will be useful to discriminate problems involving the "with" clause and which fails by lack of information or for deeper reasons. --- pretyping/pretype_errors.ml | 5 +++-- pretyping/pretype_errors.mli | 1 + 2 files changed, 4 insertions(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index cf5b08c58f..b0715af734 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -14,15 +14,16 @@ open Type_errors type unification_error = | OccurCheck of existential_key * constr - | NotClean of existential * env * constr + | NotClean of existential * env * constr (* Constr is a variable not in scope *) | NotSameArgSize | NotSameHead | NoCanonicalStructure - | ConversionFailed of env * constr * constr + | ConversionFailed of env * constr * constr (* Non convertible closed terms *) | MetaOccurInBody of existential_key | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f617df9ee7..880f48e5f9 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,7 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency | CannotSolveConstraint of Evd.evar_constraint * unification_error + | ProblemBeyondCapabilities type position = (Id.t * Locus.hyp_location_flag) option -- cgit v1.2.3 From 19aa7231ec96dbbfdda7788679cf7ddf00bda7a5 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 12 Jun 2016 16:06:43 +0200 Subject: Minor simplification in evarconv. Function default_fail was always part of an ise_try. Its associated error message was anyway thrown away. It is then irrelevant and could be made simpler. --- pretyping/evarconv.ml | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index a39e374447..96c90e2fc0 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -362,8 +362,6 @@ let rec evar_conv_x ts env evd pbty term1 term2 = and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty ((term1,sk1 as appr1),csts1) ((term2,sk2 as appr2),csts2) = - let default_fail i = (* costly *) - UnifFailure (i,ConversionFailed (env, Stack.zip appr1, Stack.zip appr2)) in let quick_fail i = (* not costly, loses info *) UnifFailure (i, NotSameHead) in @@ -415,7 +413,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty let not_only_app = Stack.not_purely_applicative skM in let f1 i = match Stack.list_of_app_stack skF with - | None -> default_fail evd + | None -> quick_fail evd | Some lF -> let tM = Stack.zip apprM in miller_pfenning on_left -- cgit v1.2.3 From bb43103f7ecea16e634d448215f24d6d55d56eb1 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 13 Jun 2016 16:37:29 +0200 Subject: evar_conv: Refine occur_rigidly This avoids postponing constraints which will surely produce an occur-check and allow to backtrack on first-order unifications producing those constraints directly (e.g. to apply eta). (fixes HoTT/HoTT with 8.5). --- pretyping/evarconv.ml | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) (limited to 'pretyping') diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 96c90e2fc0..aead1cb35f 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -97,8 +97,7 @@ let position_problem l2r = function | CUMUL -> Some l2r let occur_rigidly ev evd t = - let (l, app) = decompose_app_vect t in - let rec aux t = + let rec aux t = match kind_of_term (whd_evar evd t) with | App (f, c) -> if aux f then Array.exists aux c else false | Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true @@ -110,7 +109,7 @@ let occur_rigidly ev evd t = | Prod (_, b, t) -> ignore(aux b || aux t); true | Rel _ | Var _ -> false | Case _ -> false - in Array.exists (fun t -> try ignore(aux t); false with Occur -> true) app + in try ignore(aux t); false with Occur -> true (* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose the problem (t1 stack1) = (t2 stack2) into a problem -- cgit v1.2.3