diff options
| author | Pierre-Marie Pédrot | 2018-10-03 14:59:44 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-10-03 14:59:44 +0200 |
| commit | 10477a2b31e9cddc697b03f75adcc5e42acb0e85 (patch) | |
| tree | cd5cc8dd59215032ba4bcf83f3e5c71fbdc7ce9d | |
| parent | 920cc6ba6ee33bf34cd853f6a9a050ed7594e2ce (diff) | |
| parent | 58e1d0f2006f3243cbf7b57a9858f5119ffea666 (diff) | |
Merge PR #8563: Fix checker soundness bug with polymorphism capturing global univs
| -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 d3d114d7d7..8a5220c9ca 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 |