Fixing incorrect change to pattern-unification over Meta's introduced

in r14199 (June 2011). Meta's implicitly depend on the context they are
defined in and this has to be taken into account for checking if
occurrences are distinct (in particular, no Var's are allowed as
arguments of a pattern-unifiable Meta). The example expected to be
accepted thanks to r14199 is not a pattern-unification problem (it has
more than one solution) and was anyway already accepted (strange).

Compared to before r14199, aliases expansion and restriction of
pattern unification check to variables occurring in the right-hand
side are however now taken into account.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14642 85f007b7-540e-0410-9357-904b9bb8a0f7

4 files changed, 37 insertions, 25 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 180aac590..236bc1b43 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -227,7 +227,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | Flexible ev1, MaybeFlexible flex2 ->
 	let f1 i =
-          match is_unification_pattern env term1 l1 (applist appr2) with
+          match is_unification_pattern_evar env ev1 l1 (applist appr2) with
           | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
@@ -260,7 +260,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 
     | MaybeFlexible flex1, Flexible ev2 ->
 	let f1 i =
-	  match is_unification_pattern env term2 l2 (applist appr1) with
+	  match is_unification_pattern_evar env ev2 l2 (applist appr1) with
           | Some l1' ->
 	    (* Miller-Pfenning's patterns unification *)
 	    (* Preserve generality (except that CCI has no eta-conversion) *)
@@ -358,7 +358,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	     evar_conv_x ts (push_rel (na,None,c) env) i CONV c'1 c'2)]
 
     | Flexible ev1, (Rigid _ | PseudoRigid _) ->
-	(match is_unification_pattern env term1 l1 (applist appr2) with
+	(match is_unification_pattern_evar env ev1 l1 (applist appr2) with
         | Some l1 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
@@ -372,7 +372,7 @@ and evar_eqappr_x ts env evd pbty (term1,l1 as appr1) (term2,l2 as appr2) =
 	  true)
 
     | (Rigid _ | PseudoRigid _), Flexible ev2 ->
-	(match is_unification_pattern env term2 l2 (applist appr1) with
+	(match is_unification_pattern_evar env ev2 l2 (applist appr1) with
         | Some l2 ->
 	  (* Miller-Pfenning's pattern unification *)
 	  (* Preserve generality thanks to eta-conversion) *)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6a622d9aa..af9db2cde 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -1335,30 +1335,39 @@ let get_actual_deps aliases l t =
 
 (* Check if an applied evar "?X[args] l" is a Miller's pattern *)
 
-let find_unification_pattern_args env args l t =
+let find_unification_pattern_args env l t =
   if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
     let aliases = make_alias_map env in
-    let l' = Array.to_list args @ l in
-    match (try Some (expand_and_check_vars aliases l') with Exit -> None) with
-    | Some l when constr_list_distinct (get_actual_deps aliases l t) ->
-        Some (list_skipn (Array.length args) l)
-    | _ ->
-      None
+    match (try Some (expand_and_check_vars aliases l) with Exit -> None) with
+    | Some l as x when constr_list_distinct (get_actual_deps aliases l t) -> x
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern_meta env nb m l t =
+  (* Variables from context and rels > nb are implicitly all there *)
+  (* so we need to be a rel <= nb *)
+  if List.for_all (fun x -> isRel x && destRel x <= nb) l then
+    match find_unification_pattern_args env l t with
+    | Some _ as x when not (dependent (mkMeta m) t) -> x
+    | _ -> None
   else
     None
 
-let is_unification_pattern env f l t =
+let is_unification_pattern_evar env (evk,args) l t =
+  if List.for_all (fun x -> isRel x || isVar x) l (* common failure case *) then
+    let n = Array.length args in
+    match find_unification_pattern_args env (Array.to_list args @ l) t with
+    | Some l when not (occur_evar evk t) -> Some (list_skipn n l)
+    | _ -> None
+  else
+    None
+
+let is_unification_pattern (env,nb) f l t =
   match kind_of_term f with
-    | Meta m ->
-        (match find_unification_pattern_args env [||] l t with
-        | Some _ as x when not (dependent f t) -> x
-        | _ -> None)
-    | Evar (evk,args) ->
-        (match find_unification_pattern_args env args l t with
-        | Some _ as x when not (occur_evar evk t) -> x
-        | _ -> None)
-    | _ ->
-	None
+  | Meta m -> is_unification_pattern_meta env nb m l t
+  | Evar ev -> is_unification_pattern_evar env ev l t
+  | _ -> None
 
 (* From a unification problem "?X l = c", build "\x1...xn.(term1 l2)"
    (pattern unification). It is assumed that l is made of rel's that
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 365276853..c0c4252e6 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -96,7 +96,10 @@ val define_evar_as_product : evar_map -> existential -> evar_map * types
 val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
 val define_evar_as_sort : evar_map -> existential -> evar_map * sorts
 
-val is_unification_pattern : env -> constr -> constr list ->
+val is_unification_pattern_evar : env -> existential -> constr list ->
+  constr -> constr list option
+
+val is_unification_pattern : env * int -> constr -> constr list ->
   constr -> constr list option
 
 val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 250d83cc4..6fff81cfe 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -437,13 +437,13 @@ let unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flag
 	| App (f1,l1), _ when
 	    (isMeta f1 && use_metas_pattern_unification flags nb l1
              || use_evars_pattern_unification flags && isAllowedEvar flags f1) &
-	    store whenmem (is_unification_pattern curenv f1 (Array.to_list l1) cN) ->
+	    store whenmem (is_unification_pattern curenvnb f1 (Array.to_list l1) cN) ->
 	      solve_pattern_eqn_array curenvnb f1 (restore whenmem) cN substn
 
 	| _, App (f2,l2) when
 	    (isMeta f2 && use_metas_pattern_unification flags nb l2
              || use_evars_pattern_unification flags && isAllowedEvar flags f2) &
-	    store whenmem (is_unification_pattern curenv f2 (Array.to_list l2) cM) ->
+	    store whenmem (is_unification_pattern curenvnb f2 (Array.to_list l2) cM) ->
 	      solve_pattern_eqn_array curenvnb f2 (restore whenmem) cM substn
 
 	| App (f1,l1), App (f2,l2) ->