Permalink
Browse files

Continuation of r16346 on filtering local definitions. Refined

the "choose less dependent" constraint-solving heuristic so that
it is not disturbed by local definitions.

This is a quick fix. A deeper analysis of the structure of constraints
of the form ?x[args] = y, determining if variable y can itself be a
local def or not, and whether args can be let-ins aliasing other
variables, would allow to know if the fix needs to be refined further.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16376 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
herbelin
herbelin committed Mar 30, 2013
1 parent 13cab83 commit a9ecb7e57fed81f936045f30830322834f95a17e
Showing with 24 additions and 4 deletions.
  1. +4 −2 pretyping/evarconv.ml
  2. +3 −0 pretyping/evarsolve.mli
  3. +0 −2 pretyping/evarutil.mli
  4. +4 −0 test-suite/output/inference.out
  5. +13 −0 test-suite/output/inference.v
View
@@ -782,14 +782,16 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let app_empty = match l1, l2 with [], [] -> true | _ -> false in
match kind_of_term term1, kind_of_term term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
- && Array.for_all (fun a -> eq_constr a term2 || isEvar a) args1 ->
+ & List.for_all (fun a -> eq_constr a term2 or isEvar a)
+ (remove_instance_local_defs evd evk1 (Array.to_list args1)) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
(match choose_less_dependent_instance evk1 evd term2 args1 with
| Some evd -> Success evd
| None -> UnifFailure (evd, ConversionFailed (env,term1,term2)))
| (Rel _|Var _), Evar (evk2,args2) when app_empty
- & Array.for_all (fun a -> eq_constr a term1 or isEvar a) args2 ->
+ & List.for_all (fun a -> eq_constr a term1 or isEvar a)
+ (remove_instance_local_defs evd evk2 (Array.to_list args2)) ->
(* The typical kind of constraint coming from pattern-matching return
type inference *)
(match choose_less_dependent_instance evk2 evd term1 args2 with
View
@@ -59,3 +59,6 @@ exception IllTypedInstance of env * types * types
(* May raise IllTypedInstance if types are not convertible *)
val check_evar_instance :
evar_map -> existential_key -> constr -> conv_fun -> evar_map
+
+val remove_instance_local_defs :
+ evar_map -> existential_key -> constr list -> constr list
View
@@ -195,5 +195,3 @@ val push_rel_context_to_named_context : Environ.env -> types ->
named_context_val * types * constr list * constr list
val generalize_evar_over_rels : evar_map -> existential -> types * constr list
-
-
@@ -6,3 +6,7 @@ fun e : option L => match e with
: option L -> option L
fun (m n p : nat) (H : S m <= S n + p) => le_S_n m (n + p) H
: forall m n p : nat, S m <= S n + p -> m <= n + p
+fun n : nat => let x := A n in ?17 ?20:T n
+ : forall n : nat, T n
+fun n : nat => ?25 ?28:T n
+ : forall n : nat, T n
@@ -15,3 +15,16 @@ Print P.
(* Check that plus is folded even if reduction is involved *)
Check (fun m n p (H : S m <= (S n) + p) => le_S_n _ _ H).
+
+
+(* Check that the heuristic to solve constraints is not artificially
+ dependent on the presence of a let-in, and in particular that the
+ second [_] below is not inferred to be n, as if obtained by
+ first-order unification with [T n] of the conclusion [T _] of the
+ type of the first [_]. *)
+
+(* Note: exact numbers of evars are not important... *)
+
+Inductive T (n:nat) : Type := A : T n.
+Check fun n (x:=A n:T n) => _ _ : T n.
+Check fun n => _ _ : T n.

0 comments on commit a9ecb7e

Please sign in to comment.