Fixing wrong environment for Meta's in pose_all_metas_as_evars (bug #3284).

4 files changed, 34 insertions, 2 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f4420c489d..5bd0edf696 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -152,6 +152,12 @@ let reset_with_named_context (ctxt,ctxtv) env =
 
 let reset_context = reset_with_named_context empty_named_context_val
 
+let pop_rel_context n env =
+  let ctxt = env.env_rel_context in
+  { env with
+    env_rel_context = List.firstn (List.length ctxt - n) ctxt;
+    env_nb_rel = env.env_nb_rel - n }
+
 let fold_named_context f env ~init =
   let rec fold_right env =
     match env.env_named_context with
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 61a4f7327d..1523f40d1f 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -115,6 +115,9 @@ val reset_context : env -> env
 (** This forgets rel context and sets a new named context *)
 val reset_with_named_context : named_context_val -> env -> env
 
+(** This removes the [n] last declarations from the rel context *)
+val pop_rel_context : int -> env -> env
+
 (** {5 Global constants }
   {6 Add entries to global environment } *)
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 574088f420..71b054cd6e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -122,6 +122,8 @@ let rec subst_meta_instances bl c =
       (try pi2 (List.find select bl) with Not_found -> c)
     | _ -> map_constr (subst_meta_instances bl) c
 
+(** [env] should be the context in which the metas live *)
+
 let pose_all_metas_as_evars env evd t =
   let evdref = ref evd in
   let rec aux t = match kind_of_term t with
@@ -143,14 +145,18 @@ let pose_all_metas_as_evars env evd t =
 let solve_pattern_eqn_array (env,nb) f l c (sigma,metasubst,evarsubst) =
   match kind_of_term f with
     | Meta k ->
-	let sigma,c = pose_all_metas_as_evars env sigma c in
+	(* We enforce that the Meta does not depend on the [nb]
+	   extra assumptions added by unification to the context *)
+        let env' = pop_rel_context nb env in
+	let sigma,c = pose_all_metas_as_evars env' sigma c in
 	let c = solve_pattern_eqn env l c in
 	let pb = (Conv,TypeNotProcessed) in
 	  if noccur_between 1 nb c then
             sigma,(k,lift (-nb) c,pb)::metasubst,evarsubst
 	  else error_cannot_unify_local env sigma (applist (f, l),c,c)
     | Evar ev ->
-	let sigma,c = pose_all_metas_as_evars env sigma c in
+        let env' = pop_rel_context nb env in
+	let sigma,c = pose_all_metas_as_evars env' sigma c in
 	sigma,metasubst,(env,ev,solve_pattern_eqn env l c)::evarsubst
     | _ -> assert false
 
diff --git a/test-suite/bugs/closed/3284.v b/test-suite/bugs/closed/3284.v
new file mode 100644
index 0000000000..a942887ee9
--- /dev/null
+++ b/test-suite/bugs/closed/3284.v
@@ -0,0 +1,17 @@
+(* Several bugs:
+- wrong env in pose_all_metas_as_evars leading to out of scope instance of evar
+- check that metas posed as evars in pose_all_metas_as_evars were
+  resolved was not done
+*)
+
+Axiom functional_extensionality_dep :
+  forall {A : Type} {B : A -> Type} (f g : forall x : A, B x),
+    (forall x : A, f x = g x) -> f = g.
+
+Goal forall A B C (f g : forall (x : A) (y : B x), C x y), forall x:A, (forall x y, f x y = g x y) -> True.
+Proof.
+  intros A B C f g x H.
+  Fail apply @functional_extensionality_dep in H.
+  Fail apply functional_extensionality_dep in H.
+  specialize (H x).
+  apply functional_extensionality_dep in H.