5 files changed, 43 insertions, 0 deletions
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