From a9ecb7e57fed81f936045f30830322834f95a17e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 30 Mar 2013 18:45:55 +0000
Subject: 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
---
 pretyping/evarconv.ml           |  6 ++++--
 pretyping/evarsolve.mli         |  3 +++
 pretyping/evarutil.mli          |  2 --
 test-suite/output/inference.out |  4 ++++
 test-suite/output/inference.v   | 13 +++++++++++++
 5 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2d21fb0e77..8da09d5c56 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -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
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3e769e02de..e81fe83d21 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -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
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 92e8193813..4db6fdd3e8 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -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
-
-
diff --git a/test-suite/output/inference.out b/test-suite/output/inference.out
index 16b23ed18d..e2a36cfe7c 100644
--- a/test-suite/output/inference.out
+++ b/test-suite/output/inference.out
@@ -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
diff --git a/test-suite/output/inference.v b/test-suite/output/inference.v
index fe537c59a7..cd9a4a12b2 100644
--- a/test-suite/output/inference.v
+++ b/test-suite/output/inference.v
@@ -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.
-- 
cgit v1.2.3