Fixed bug #2930: folded let-in's were hiding a violation to the occur

check condition in pattern-unification, resulting in the instantiation
of evars by terms depending on themselves, henceforth leading
eventually to a stack overflow. Occur-check in the arguments of evars
was also missing.

[Also fixed what looked like a typo in the env passed to
project_evar_on_evar on line 1611.]

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

2 files changed, 39 insertions, 16 deletions

diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 37f698cbe7..4996f86c24 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -141,15 +141,21 @@ let whd_head_evar_stack sigma c =
 
 let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
 
-let noccur_evar evd evk c =
-  let rec occur_rec c = match kind_of_term c with
-  | Evar (evk',_ as ev') ->
+let noccur_evar env evd evk c =
+  let rec occur_rec k c = match kind_of_term c with
+  | Evar (evk',args' as ev') ->
       (match safe_evar_value evd ev' with
-       | Some c -> occur_rec c
-       | None -> if Int.equal evk evk' then raise Occur)
-  | _ -> iter_constr occur_rec c
+       | Some c -> occur_rec k c
+       | None ->
+           if Int.equal evk evk' then raise Occur
+           else Array.iter (occur_rec k) args')
+  | Rel i when i > k ->
+      (match pi2 (Environ.lookup_rel (i-k) env) with
+       | None -> ()
+       | Some b -> occur_rec k (lift i b))
+  | _ -> iter_constr_with_binders succ occur_rec k c
   in
-  try occur_rec c; true with Occur -> false
+  try occur_rec 0 c; true with Occur -> false
 
 let normalize_evar evd ev =
   match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -757,7 +763,8 @@ let is_unification_pattern_meta env nb m l t =
     None
 
 let is_unification_pattern_evar env evd (evk,args) l t =
-  if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then
+  if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
+  then
     let args = remove_instance_local_defs evd evk (Array.to_list args) in
     let n = List.length args in
     match find_unification_pattern_args env (args @ l) t with
@@ -1132,10 +1139,11 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
     | Not_found -> CannotInvert
     | NotUnique -> Invertible NoUniqueProjection
 
-let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
   let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
   match res with
-  | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
+  | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
+      ->
       CannotInvert
   | _ ->
       res
@@ -1161,10 +1169,11 @@ let extract_candidates sols =
   with Exit ->
     None
 
-let invert_invertible_arg evd aliases k (evk,argsv) args' =
+let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
   let evi = Evd.find_undefined evd evk in
   let subst,_ = make_projectable_subst aliases evd evi argsv in
-  let projs = Array.map_to_list (invert_arg evd aliases k evk subst) args' in
+  let projs =
+    Array.map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
   Array.of_list (extract_unique_projections projs)
 
 (* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -1377,12 +1386,14 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
 
 let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
   let filter1 =
-    restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
+    restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
+      (Array.to_list argsv1)
   in
   let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
   let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
   let filter2 =
-    restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
+    restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
+      (Array.to_list argsv2)
   in
   let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
   let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
@@ -1402,7 +1413,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2
     try
       let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
       let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
-      evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1)
+      evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
     with
     | EvarSolvedWhileRestricting (evd,ev1) ->
         raise (EvarSolvedOnTheFly (evd,ev1))
@@ -1600,7 +1611,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
         let aliases = lift_aliases k aliases in
         (try
           let ev = (evk,Array.map (lift k) argsv) in
-          let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev'  ev in
+          let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev'  ev in
 	  evdref := evd;
           body
         with
diff --git a/test-suite/bugs/closed/2930.v b/test-suite/bugs/closed/2930.v
new file mode 100644
index 0000000000..0994b6fb23
--- /dev/null
+++ b/test-suite/bugs/closed/2930.v
@@ -0,0 +1,12 @@
+(* Checking that let-in's hiding evars are expanded when enforcing
+   "occur-check" *)
+
+Require Import List.
+
+Definition foo x y :=
+let xy := (x, y) in
+let bar xys  :=
+      match xys with
+      | nil => xy :: nil
+      | xy' :: xys' => xy' :: xys'
+      end in bar (nil : list (nat * nat)).