From 58e1d0f2006f3243cbf7b57a9858f5119ffea666 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 26 Sep 2018 16:29:16 +0200
Subject: Fix checker soundness bug with polymorphism capturing global univs

Followup for #8341.

Not making a test as that's too difficult with our current infrastructure.
---
 checker/checker.ml | 4 +++-
 checker/univ.ml    | 5 ++---
 2 files changed, 5 insertions(+), 4 deletions(-)

diff --git a/checker/checker.ml b/checker/checker.ml
index fd2725c859..d63575b34c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -243,7 +243,9 @@ let explain_exn = function
   | Invalid_argument s ->
       hov 0 (anomaly_string () ++ str "uncaught exception Invalid_argument " ++ guill s ++ report ())
   | Sys.Break ->
-      hov 0 (fnl () ++ str "User interrupt.")
+    hov 0 (fnl () ++ str "User interrupt.")
+  | Univ.AlreadyDeclared ->
+    hov 0 (str "Error: Multiply declared universe.")
   | Univ.UniverseInconsistency (o,u,v) ->
       let msg =
 	if !Flags.debug (*!Constrextern.print_universes*) then
diff --git a/checker/univ.ml b/checker/univ.ml
index e50e883adf..a0511ad21b 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1088,14 +1088,13 @@ let subst_univs_universe fn ul =
 
 let merge_context strict ctx g =
   let g = Array.fold_left
-   (* Be lenient, module typing reintroduces universes and 
-      constraints due to includes *)
-	    (fun g v -> try add_universe v strict g with AlreadyDeclared -> g)
+            (fun g v -> add_universe v strict g)
 	    g (UContext.instance ctx)
   in merge_constraints (UContext.constraints ctx) g
 
 let merge_context_set strict ctx g =
   let g = LSet.fold
+   (* Include and side effects still have double-declared universes *)
 	    (fun v g -> try add_universe v strict g with AlreadyDeclared -> g)
 	    (ContextSet.levels ctx) g
   in merge_constraints (ContextSet.constraints ctx) g
-- 
cgit v1.2.3