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 *)

1 files changed, 23 insertions, 8 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