Merge PR #891: Check universes are declared

10 files changed, 119 insertions, 9 deletions

diff --git a/engine/evd.ml b/engine/evd.ml
index d1c7fef738..9f976b57dd 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -774,7 +774,7 @@ let universe_subst evd =
   UState.subst evd.universes
 
 let merge_context_set ?loc ?(sideff=false) rigid evd ctx' =
-  {evd with universes = UState.merge ?loc sideff rigid evd.universes ctx'}
+  {evd with universes = UState.merge ?loc ~sideff ~extend:true rigid evd.universes ctx'}
 
 let merge_universe_subst evd subst = 
   {evd with universes = UState.merge_subst evd.universes subst }
diff --git a/engine/uState.ml b/engine/uState.ml
index 0791e4c277..29cb3c9bcc 100644
--- a/engine/uState.ml
+++ b/engine/uState.ml
@@ -430,10 +430,17 @@ let univ_rigid = UnivRigid
 let univ_flexible = UnivFlexible false
 let univ_flexible_alg = UnivFlexible true
 
-let merge ?loc sideff rigid uctx ctx' =
+(** ~sideff indicates that it is ok to redeclare a universe.
+    ~extend also merges the universe context in the local constraint structures
+    and not only in the graph. This depends if the
+    context we merge comes from a side effect that is already inlined
+    or defined separately. In the later case, there is no extension,
+    see [emit_side_effects] for example. *)
+let merge ?loc ~sideff ~extend rigid uctx ctx' =
   let open Univ in
   let levels = ContextSet.levels ctx' in
-  let uctx = if sideff then uctx else
+  let uctx =
+    if not extend then uctx else
     match rigid with
     | UnivRigid -> uctx
     | UnivFlexible b ->
@@ -448,9 +455,8 @@ let merge ?loc sideff rigid uctx ctx' =
         else { uctx with uctx_univ_variables = uvars' }
   in
   let uctx_local =
-    if sideff then uctx.uctx_local
-    else ContextSet.append ctx' uctx.uctx_local
-  in
+    if not extend then uctx.uctx_local
+    else ContextSet.append ctx' uctx.uctx_local in
   let declare g =
     LSet.fold (fun u g ->
                try UGraph.add_universe u false g
@@ -479,7 +485,7 @@ let merge_subst uctx s =
 
 let emit_side_effects eff u =
   let uctxs = Safe_typing.universes_of_private eff in
-  List.fold_left (merge true univ_rigid) u uctxs
+  List.fold_left (merge ~sideff:true ~extend:false univ_rigid) u uctxs
 
 let new_univ_variable ?loc rigid name
   ({ uctx_local = ctx; uctx_univ_variables = uvars; uctx_univ_algebraic = avars} as uctx) =
@@ -668,7 +674,7 @@ let update_sigma_env uctx env =
     { uctx with uctx_initial_universes = univs;
                          uctx_universes = univs }
   in
-  merge true univ_rigid eunivs eunivs.uctx_local
+  merge ~sideff:true ~extend:false univ_rigid eunivs eunivs.uctx_local
 
 let pr_weak prl {uctx_weak_constraints=weak} =
   let open Pp in
diff --git a/engine/uState.mli b/engine/uState.mli
index a59e61b894..f833508ebf 100644
--- a/engine/uState.mli
+++ b/engine/uState.mli
@@ -103,7 +103,7 @@ val univ_rigid : rigid
 val univ_flexible : rigid
 val univ_flexible_alg : rigid
 
-val merge : ?loc:Loc.t -> bool -> rigid -> t -> Univ.ContextSet.t -> t
+val merge : ?loc:Loc.t -> sideff:bool -> extend:bool -> rigid -> t -> Univ.ContextSet.t -> t
 val merge_subst : t -> UnivSubst.universe_opt_subst -> t
 val emit_side_effects : Safe_typing.private_constants -> t -> t
 
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 1c323e3ea2..60293fe864 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -62,6 +62,7 @@ type ('constr, 'types) ptype_error =
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.Constraint.t
+  | UndeclaredUniverse of Univ.Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -125,3 +126,6 @@ let error_elim_explain kp ki =
 
 let error_unsatisfied_constraints env c =
   raise (TypeError (env, UnsatisfiedConstraints c))
+
+let error_undeclared_universe env l =
+  raise (TypeError (env, UndeclaredUniverse l))
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 20bf300ac3..9c6ef64b50 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -63,6 +63,7 @@ type ('constr, 'types) ptype_error =
   | IllTypedRecBody of
       int * Name.t array * ('constr, 'types) punsafe_judgment array * 'types array
   | UnsatisfiedConstraints of Univ.Constraint.t
+  | UndeclaredUniverse of Univ.Level.t
 
 type type_error = (constr, types) ptype_error
 
@@ -108,3 +109,5 @@ val error_ill_typed_rec_body  :
 val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
 
 val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+
+val error_undeclared_universe : env -> Univ.Level.t -> 'a
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 7f36f3813f..25c1cbff3a 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -431,7 +431,28 @@ and execute_recdef env (names,lar,vdef) i =
 and execute_array env = Array.map (execute env)
 
 (* Derived functions *)
+
+let universe_levels_of_constr env c =
+  let rec aux s c =
+    match kind c with
+    | Const (c, u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Ind ((mind,_), u) | Construct (((mind,_),_), u) ->
+       LSet.fold LSet.add (Instance.levels u) s
+    | Sort u when not (Sorts.is_small u) ->
+      let u = Sorts.univ_of_sort u in
+      LSet.fold LSet.add (Universe.levels u) s
+    | _ -> Constr.fold aux s c
+  in aux LSet.empty c
+
+let check_wellformed_universes env c =
+  let univs = universe_levels_of_constr env c in
+  try UGraph.check_declared_universes (universes env) univs
+  with UGraph.UndeclaredLevel u ->
+    error_undeclared_universe env u
+
 let infer env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
     make_judge constr t
 
@@ -449,11 +470,13 @@ let type_judgment env {uj_val=c; uj_type=t} =
   {utj_val = c; utj_type = s }
 
 let infer_type env constr =
+  let () = check_wellformed_universes env constr in
   let t = execute env constr in
   let s = check_type env constr t in
   {utj_val = constr; utj_type = s}
 
 let infer_v env cv =
+  let () = Array.iter (check_wellformed_universes env) cv in
   let jv = execute_array env cv in
     make_judgev cv jv
 
@@ -461,9 +484,11 @@ let infer_v env cv =
 
 let infer_local_decl env id = function
   | Entries.LocalDefEntry c ->
+      let () = check_wellformed_universes env c in
       let t = execute env c in
       RelDecl.LocalDef (Name id, c, t)
   | Entries.LocalAssumEntry c ->
+      let () = check_wellformed_universes env c in
       let t = execute env c in
       RelDecl.LocalAssum (Name id, check_assumption env c t)
 
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index bc624ba56d..95d71965df 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -529,6 +529,11 @@ let add_universe vlev strict g =
 let add_universe_unconstrained vlev g =
   fst (add_universe_gen vlev g)
 
+exception UndeclaredLevel of Univ.Level.t
+let check_declared_universes g us =
+  let check l = if not (UMap.mem l g.entries) then raise (UndeclaredLevel l) in
+  Univ.LSet.iter check us
+
 exception Found_explanation of explanation
 
 let get_explanation strict u v g =
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index 8c2d877b0b..752bf76270 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -55,6 +55,12 @@ val add_universe : Level.t -> bool -> t -> t
 (** Add a universe without (Prop,Set) <= u *)
 val add_universe_unconstrained : Level.t -> t -> t
 
+(** Check that the universe levels are declared. Otherwise
+    @raise UndeclaredLevel l for the first undeclared level found. *)
+exception UndeclaredLevel of Univ.Level.t
+
+val check_declared_universes : t -> Univ.LSet.t -> unit
+
 (** {6 Pretty-printing of universes. } *)
 
 val pr_universes : (Level.t -> Pp.t) -> t -> Pp.t
diff --git a/test-suite/bugs/closed/7900.v b/test-suite/bugs/closed/7900.v
new file mode 100644
index 0000000000..583ef0ef3b
--- /dev/null
+++ b/test-suite/bugs/closed/7900.v
@@ -0,0 +1,53 @@
+Require Import Coq.Program.Program.
+(* Set Universe Polymorphism. *)
+Set Printing Universes.
+
+Axiom ALL : forall {T:Prop}, T.
+
+Inductive Expr : Set := E (a : Expr).
+
+Parameter Value : Set.
+
+Fixpoint eval (e: Expr): Value :=
+  match e with
+  | E a => eval a
+  end.
+
+Class Quote (n: Value) : Set :=
+  { quote: Expr
+    ; eval_quote: eval quote = n }.
+
+Program Definition quote_mult n
+        `{!Quote n} : Quote n :=
+  {| quote := E (quote (n:=n)) |}.
+
+Set Printing Universes.
+Next Obligation.
+Proof.
+  Show Universes.
+  destruct Quote0 as [q eq].
+  Show Universes.
+  rewrite <- eq.
+  clear n eq.
+  Show Universes.
+  apply ALL.
+  Show Universes.
+Qed.
+Print quote_mult_obligation_1.
+(* quote_mult_obligation_1@{} =
+let Top_internal_eq_rew_dep :=
+  fun (A : Type@{Coq.Init.Logic.8}) (x : A) (P : forall a : A, x = a -> Type@{Top.5} (* <- XXX *))
+    (f : P x eq_refl) (y : A) (e : x = y) =>
+  match e as e0 in (_ = y0) return (P y0 e0) with
+  | eq_refl => f
+  end in
+fun (n : Value) (Quote0 : Quote n) =>
+match Quote0 as q return (eval quote = n) with
+| {| quote := q; eval_quote := eq0 |} =>
+    Top_internal_eq_rew_dep Value (eval q) (fun (n0 : Value) (eq1 : eval q = n0) => eval quote = n0)
+      ALL n eq0
+end
+     : forall (n : Value) (Quote0 : Quote n), eval (E quote) = n
+
+quote_mult_obligation_1 is universe polymorphic
+*)
diff --git a/vernac/himsg.ml b/vernac/himsg.ml
index b9c47ff475..a4650cfd92 100644
--- a/vernac/himsg.ml
+++ b/vernac/himsg.ml
@@ -679,6 +679,11 @@ let explain_unsatisfied_constraints env sigma cst =
     Univ.pr_constraints (Termops.pr_evd_level sigma) cst ++ 
     spc () ++ str "(maybe a bugged tactic)."
 
+let explain_undeclared_universe env sigma l =
+  strbrk "Undeclared universe: " ++
+    Termops.pr_evd_level sigma l ++
+    spc () ++ str "(maybe a bugged tactic)."
+
 let explain_type_error env sigma err =
   let env = make_all_name_different env sigma in
   match err with
@@ -716,6 +721,8 @@ let explain_type_error env sigma err =
       explain_wrong_case_info env ind ci
   | UnsatisfiedConstraints cst ->
       explain_unsatisfied_constraints env sigma cst
+  | UndeclaredUniverse l ->
+     explain_undeclared_universe env sigma l
 
 let pr_position (cl,pos) =
   let clpos = match cl with
@@ -1299,6 +1306,7 @@ let map_ptype_error f = function
 | IllTypedRecBody (n, na, jv, t) ->
   IllTypedRecBody (n, na, Array.map (on_judgment f) jv, Array.map f t)
 | UnsatisfiedConstraints g -> UnsatisfiedConstraints g
+| UndeclaredUniverse l -> UndeclaredUniverse l
 
 let explain_reduction_tactic_error = function
   | Tacred.InvalidAbstraction (env,sigma,c,(env',e)) ->