diff options
| author | Gaëtan Gilbert | 2018-09-26 16:29:16 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-10-01 12:56:00 +0200 |
| commit | 58e1d0f2006f3243cbf7b57a9858f5119ffea666 (patch) | |
| tree | 8f3147b07daa3d93e0f31c268eb2be4c0bee76fc | |
| parent | 9134d94d42bafd38dfcc6a09a99edd554e636b55 (diff) | |
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.
| -rw-r--r-- | checker/checker.ml | 4 | ||||
| -rw-r--r-- | 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 |