Make restrict_universe_context stronger.

This fixes BZ#5717.

Also add a test and fix a changed test.

4 files changed, 122 insertions, 59 deletions

diff --git a/engine/univops.ml b/engine/univops.ml
index d498b2e0d..9a9ae12ca 100644
--- a/engine/univops.ml
+++ b/engine/univops.ml
@@ -20,21 +20,79 @@ let universes_of_constr c =
     | _ -> Constr.fold aux s c
   in aux LSet.empty c
 
-let restrict_universe_context (univs,csts) s =
-  (* Universes that are not necessary to typecheck the term.
-     E.g. univs introduced by tactics and not used in the proof term. *)
-  let diff = LSet.diff univs s in
-  let rec aux diff candid univs ness = 
-    let (diff', candid', univs', ness') = 
-      Constraint.fold
-	(fun (l, d, r as c) (diff, candid, univs, csts) ->
-	  if not (LSet.mem l diff) then
-	    (LSet.remove r diff, candid, univs, Constraint.add c csts)
-	  else if not (LSet.mem r diff) then
-	    (LSet.remove l diff, candid, univs, Constraint.add c csts)
-	  else (diff, Constraint.add c candid, univs, csts))
-	candid (diff, Constraint.empty, univs, ness)
-    in
-      if ness' == ness then (LSet.diff univs diff', ness)
-      else aux diff' candid' univs' ness'
-  in aux diff csts univs Constraint.empty
+type graphnode = {
+  mutable up : constraint_type LMap.t;
+  mutable visited : bool
+}
+
+let merge_types d d0 =
+  match d, d0 with
+  | _, Lt | Lt, _ -> Lt
+  | Le, _ | _, Le -> Le
+  | Eq, Eq -> Eq
+
+let merge_up d b up =
+  let find = try Some (LMap.find b up) with Not_found -> None in
+  match find with
+  | Some d0 ->
+    let d = merge_types d d0 in
+    if d == d0 then up else LMap.add b d up
+  | None -> LMap.add b d up
+
+let add_up a d b graph =
+  let node, graph =
+    try LMap.find a graph, graph
+    with Not_found ->
+      let node = { up = LMap.empty; visited = false } in
+      node, LMap.add a node graph
+  in
+  node.up <- merge_up d b node.up;
+  graph
+
+(* for each node transitive close until you find a non removable, discard the rest *)
+let transitive_close removable graph =
+  let rec do_node a node =
+    if not node.visited
+    then
+      let keepup =
+        LMap.fold (fun b d keepup ->
+            if not (LSet.mem b removable)
+            then merge_up d b keepup
+            else
+              begin
+                match LMap.find b graph with
+                | bnode ->
+                  do_node b bnode;
+                  LMap.fold (fun k d' keepup ->
+                    merge_up (merge_types d d') k keepup)
+                    bnode.up keepup
+                | exception Not_found -> keepup
+              end
+          )
+          node.up LMap.empty
+      in
+      node.up <- keepup;
+      node.visited <- true
+  in
+  LMap.iter do_node graph
+
+let restrict_universe_context (univs,csts) keep =
+  let removable = LSet.diff univs keep in
+  let (csts, rem) =
+    Constraint.fold (fun (a,d,b as cst) (csts, rem) ->
+        if LSet.mem a removable || LSet.mem b removable
+        then (csts, add_up a d b rem)
+        else (Constraint.add cst csts, rem))
+      csts (Constraint.empty, LMap.empty)
+  in
+  transitive_close removable rem;
+  let csts =
+    LMap.fold (fun a node csts ->
+        if LSet.mem a removable
+        then csts
+        else
+          LMap.fold (fun b d csts -> Constraint.add (a,d,b) csts)
+            node.up csts)
+      rem csts
+  in
+  (LSet.inter univs keep, csts)
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index cf5dc95fe..aa5621770 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -346,9 +346,14 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
 	  if not (keep_body_ucst_separate || not (Safe_typing.empty_private_constants = eff)) then
 	    nf t
 	  else t
-	in
+        in
         let used_univs_body = Univops.universes_of_constr body in
         let used_univs_typ = Univops.universes_of_constr typ in
+        (* Universes for private constants are relevant to the body *)
+        let used_univs_body =
+          List.fold_left (fun acc (us,_) -> Univ.LSet.union acc us)
+            used_univs_body (Safe_typing.universes_of_private eff)
+        in
         if keep_body_ucst_separate ||
            not (Safe_typing.empty_private_constants = eff) then
           let initunivs = UState.const_univ_entry ~poly initial_euctx in
diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v
index fd9640b89..fa30132ab 100644
--- a/test-suite/bugs/closed/3690.v
+++ b/test-suite/bugs/closed/3690.v
@@ -3,49 +3,44 @@ Set Printing Universes.
 Set Universe Polymorphism.
 Definition foo (a := Type) (b := Type) (c := Type) := Type.
 Print foo.
-(* foo =
-let a := Type@{Top.1} in
-let b := Type@{Top.2} in let c := Type@{Top.3} in Type@{Top.4}
-     : Type@{Top.4+1}
-(* Top.1
-   Top.2
-   Top.3
-   Top.4 |=  *) *)
-Check @foo. (* foo@{Top.5 Top.6 Top.7
-Top.8}
-     : Type@{Top.8+1}
-(* Top.5
-   Top.6
-   Top.7
-   Top.8 |=  *) *)
+(* foo@{Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10} =
+let a := Type@{Top.2} in let b := Type@{Top.5} in let c := Type@{Top.8} in Type@{Top.10}
+     : Type@{Top.10+1}
+(* Top.2 Top.3 Top.5 Top.6 Top.8 Top.9 Top.10 |= Top.2 < Top.3
+                                                 Top.5 < Top.6
+                                                 Top.8 < Top.9
+                                                  *)
+ *)
+Check @foo. (* foo@{Top.11 Top.12 Top.13 Top.14 Top.15 Top.16
+Top.17}
+     : Type@{Top.17+1}
+(* Top.11 Top.12 Top.13 Top.14 Top.15 Top.16 Top.17 |= Top.11 < Top.12
+                                                       Top.13 < Top.14
+                                                       Top.15 < Top.16
+                                                        *)
+ *)
 Definition bar := ltac:(let t := eval compute in foo in exact t).
-Check @bar. (* bar@{Top.13 Top.14 Top.15
-Top.16}
-     : Type@{Top.16+1}
-(* Top.13
-   Top.14
-   Top.15
-   Top.16 |=  *) *)
-(* The following should fail, since [bar] should only need one universe. *)
-Check @bar@{i j}.
+Check @bar. (* bar@{Top.27}
+     : Type@{Top.27+1}
+(* Top.27 |=  *) *)
+
+Check @bar@{i}.
 Definition baz (a := Type) (b := Type : a) (c := Type : b) := a -> c.
 Definition qux := Eval compute in baz.
-Check @qux. (* qux@{Top.24 Top.25
-Top.26}
-     : Type@{max(Top.24+1, Top.26+1)}
-(* Top.24
-   Top.25
-   Top.26 |= Top.25 < Top.24
-              Top.26 < Top.25
-               *) *)
-Print qux. (* qux =
-Type@{Top.21} -> Type@{Top.23}
-     : Type@{max(Top.21+1, Top.23+1)}
-(* Top.21
-   Top.22
-   Top.23 |= Top.22 < Top.21
-              Top.23 < Top.22
-               *) *)
+Check @qux. (* qux@{Top.38 Top.39 Top.40
+Top.41}
+     : Type@{max(Top.38+1, Top.41+1)}
+(* Top.38 Top.39 Top.40 Top.41 |= Top.38 < Top.39
+                                  Top.40 < Top.38
+                                  Top.41 < Top.40
+                                   *) *)
+Print qux. (* qux@{Top.34 Top.35 Top.36 Top.37} =
+Type@{Top.34} -> Type@{Top.37}
+     : Type@{max(Top.34+1, Top.37+1)}
+(* Top.34 Top.35 Top.36 Top.37 |= Top.34 < Top.35
+                                  Top.36 < Top.34
+                                  Top.37 < Top.36
+                                   *) *)
 Fail Check @qux@{Set Set}.
 Check @qux@{Type Type Type Type}.
 (* [qux] should only need two universes *)
diff --git a/test-suite/bugs/closed/5717.v b/test-suite/bugs/closed/5717.v
new file mode 100644
index 000000000..1bfd917d2
--- /dev/null
+++ b/test-suite/bugs/closed/5717.v
@@ -0,0 +1,5 @@
+Definition foo@{i} (A : Type@{i}) (l : list A) :=
+  match l with
+  | nil => nil
+  | cons _ t => t
+  end.