Quickly fixing bug #2996: typing functions now check when referring to

a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.

Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.

It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.

Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)

or

Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True.  (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)

6 files changed, 62 insertions, 12 deletions

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 98c0dfc20..cd1f2c856 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -96,15 +96,22 @@ let judge_of_variable env id =
 (* Management of context of variables. *)
 
 (* Checks if a context of variables can be instantiated by the
-   variables of the current env *)
-(* TODO: check order? *)
+   variables of the current env.
+   Order does not have to be checked assuming that all names are distinct *)
 let check_hyps_inclusion env c sign =
   Context.fold_named_context
-    (fun (id,_,ty1) () ->
+    (fun (id,b1,ty1) () ->
       try
-        let ty2 = named_type id env in
-        if not (eq_constr ty2 ty1) then raise Exit
-      with Not_found | Exit ->
+        let (_,b2,ty2) = lookup_named id env in
+        conv env ty2 ty1;
+        (match b2,b1 with
+        | None, None -> ()
+        | None, Some _ ->
+            (* This is wrong, because we don't know if the body is
+               needed or not for typechecking: *) ()
+        | Some _, None -> raise NotConvertible
+        | Some b2, Some b1 -> conv env b2 b1);
+      with Not_found | NotConvertible | Option.Heterogeneous ->
         error_reference_variables env id c)
     sign
     ~init:()
@@ -145,9 +152,17 @@ let type_of_constant_type_knowing_parameters env t paramtyps =
       mkArity (List.rev ctx,s)
 
 let type_of_constant_knowing_parameters env cst paramtyps =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ty, cu = constant_type env cst in
     type_of_constant_type_knowing_parameters env ty paramtyps, cu
 
+let type_of_constant_knowing_parameters_in env cst paramtyps =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
+  let ty = constant_type_in env cst in
+    type_of_constant_type_knowing_parameters env ty paramtyps
+
 let type_of_constant_type env t =
   type_of_constant_type_knowing_parameters env t [||]
 
@@ -155,13 +170,13 @@ let type_of_constant env cst =
   type_of_constant_knowing_parameters env cst [||]
 
 let type_of_constant_in env cst =
+  let cb = lookup_constant (fst cst) env in
+  let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in
   let ar = constant_type_in env cst in
     type_of_constant_type_knowing_parameters env ar [||]
 
 let judge_of_constant_knowing_parameters env (kn,u as cst) args =
   let c = mkConstU cst in
-  let cb = lookup_constant kn env in
-  let _ = check_hyps_inclusion env c cb.const_hyps in
   let ty, cu = type_of_constant_knowing_parameters env cst args in
   let _ = Environ.check_constraints cu env in
     make_judge c ty
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index e6fdf3d6c..ad0634e6c 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -120,6 +120,12 @@ val type_of_constant_type_knowing_parameters :
 val type_of_constant_knowing_parameters :
   env -> pconstant -> types Lazy.t array -> types constrained
 
+val type_of_constant_knowing_parameters_in :
+  env -> pconstant -> types Lazy.t array -> types
+
 (** Make a type polymorphic if an arity *)
 val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment ->
   constant_type
+
+(** Check that hyps are included in env and fails with error otherwise *)
+val check_hyps_inclusion : env -> constr -> section_context -> unit
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 6d7403031..c8c1d0e21 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -311,7 +311,7 @@ let pretype_ref loc evdref env ref us =
   | ref ->
     let evd, c = pretype_global loc univ_flexible env !evdref ref us in
     let () = evdref := evd in
-    let ty = Retyping.get_type_of env evd c in
+    let ty = Typing.type_of env evd c in
       make_judge c ty
 
 let judge_of_Type evd s =
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index aa33c3286..c7bdabe93 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -183,8 +183,7 @@ let retype ?(polyprop=true) sigma =
 	       ~polyprop env (mip,snd ind) argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
     | Const cst ->
-      let t = constant_type_in env cst in
-	(try Typeops.type_of_constant_type_knowing_parameters env t argtyps
+	(try Typeops.type_of_constant_knowing_parameters_in env cst argtyps
 	 with Reduction.NotArity -> retype_error NotAnArity)
     | Var id -> type_of_var env id
     | Construct cstr -> type_of_constructor env cstr
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 92bdd35ec..669fbfb46 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -27,7 +27,7 @@ let meta_type evd mv =
 
 let constant_type_knowing_parameters env cst jl =
   let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in
-  type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp
+  type_of_constant_knowing_parameters_in env cst paramstyp
 
 let inductive_type_knowing_parameters env (ind,u) jl =
   let mspec = lookup_mind_specif env ind in
diff --git a/test-suite/bugs/closed/2996.v b/test-suite/bugs/closed/2996.v
new file mode 100644
index 000000000..440cda617
--- /dev/null
+++ b/test-suite/bugs/closed/2996.v
@@ -0,0 +1,30 @@
+(* Test on definitions referring to section variables that are not any
+   longer in the current context *)
+
+Section x.
+
+  Hypothesis h : forall(n : nat), n < S n.
+
+  Definition f(n m : nat)(less : n < m) : nat := n + m.
+
+  Lemma a : forall(n : nat), f n (S n) (h n) = 1 + 2 * n.
+  Proof.
+    (* XXX *) admit.
+  Qed.
+
+  Lemma b : forall(n : nat), n < 3 + n.
+  Proof.
+    clear.
+    intros n.
+    Fail assert (H := a n).
+  Abort.
+
+  Let T := True.
+  Definition p := I : T.
+
+  Lemma paradox : False.
+  Proof.
+    clear.
+    set (T := False).
+    Fail pose proof p as H.
+  Abort.